Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to
one of the most challenging environments for parallel computing—Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as
well as non-uniform 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 - Desktop Grid - Peer-to-Peer - Distributed systems