Dissolve: A Distributed SAT Solver Based on Stalmarck's Method

Abstract

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 Stålmarck’s method. In particular, we use a variant of Stålmarck’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.