A new approach to parallel SAT solvers; New parallel approach to the Boolean satisfiabilityproblem (SAT); New approach to parallel Boolean satisfiability problemsolvers
Max Nelson · 2013
We present a novel approach to solving SAT problems in parallel by partitioning the entire set of problem clauses into smaller pieces that can be solved by individual threads. We examine the complications that arise with this partitioning, including the idea of global variables, broadcasting global conflict clauses, and a protocol to ensure correctness. Along with this algorithm description, we provide the details of a C++ implementation, ParallelSAT, with a few specific optimizations. Finally, we demonstrate that this approach provides a significant speedup on a set of SAT problems related to program analysis.