The Satisfiability (SAT) Problem fulfills both criteria for being tackled using a Peer-to-Peer Desktop Grid (P2PDG) system: First, it exhibits a considerable degree of parallelism and scalability. Second, it allows for problem decomposition into loosely coupled, yet not independent, parallel tasks to be farmed out for computation. In contrast to many prominent P2PDG applications (like SETI(at)Home), SAT problem decomposition has to be done in a fully dynamic manner. Moreover, to scale to a large number of compute nodes, the centralized coordinator/worker execution model of these applications must be replaced with a fully decentralized one, that fully leverages the Peer-to-Peer interaction possibilities provided by the Cohesion platform.
As SAT is prototypical for many other Constraint Satisfaction Problems (CSP), we enable an important new class of applications for execution on Desktop Grids with Cohesion SAT^SE.

The long term goal of Cohesion SAT^SE is to provide a generic framework for robust scalable distributed SAT solving that decouples distributed execution from sequential solver implementations issues.
As a first step towards this framework, we have implented a distributed SAT solving engine based on a fully distributed task pool with dynamic on-line decomposition. We leverage MiniSat 1.14 as the solver core, as it is easy to modify, highly efficient and explicitely designed for integration. Load balancing is based on Random Stealing. Termination detection is done using the Fixed Energy protocol.