Parallel SAT Solving using Bit-level Operations¹

Abstract

We show how to exploit the 32/64 bit architecture of modern computers to accelerate some of the algorithms used in satisfiability solving by modifying assignments to variables in parallel on a single processor. Techniques such as random sampling demonstrate that while using bit vectors instead of Boolean values solutions to satisfiable formulae can be obtained faster. Here, we reveal that more complex algorithms, like unit propagation and detection of autarkies, can be parallelized efficiently, as well.

We capitalize on the developed parallel algorithms by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. Experiments show that the parallel version performs much faster than the original implementation.