Parallel SAT Solving on Peer-to-Peer Desktop Grids

Abstract Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domainspecific problems inherent to one of the most challenging environments for parallel computing -- Peer-toPeer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as nonuniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers. Keywords SAT Solving

• Type: Journal
• Year: 2010
• Where: GRID
• Authors: Sven Schulz, Wolfgang Blochinger
• Keywords: Desktop Grid, Distributed And Parallel Computing, Distributed Parallel Satisfiability, GRID 2010, Multi-stage Sat Formula