Creating an effective parallel SAT solver is known to be a challenging task. At present, the most efficient implementations of parallel SAT solvers are portfolio solvers with some heuristics to share learnt clauses. In this paper, we propose a novel approach for solving SAT problems in parallel based on the combination of traditional CDCL with Staalmarck's method. In particular, we use a variant of Staalmarck's Dilemma Rule to partition the search space between solvers and merge their results.

The paper describes the design of a new distributed SAT solver, called Dissolve, and presents experiments that demonstrate the value of the Dilemma-rule-based approach. The experiments showed that running times decreased on average (geometric mean) by 25% and 17% for SAT and UNSAT examples, respectively.

(Click here to access the paper: PDF.)