A fast SAT solver algorithm best suited to reconfigurable hardware
Romanelli Zuim, José T. de Sousa, Claudionor N. Coelho · 2006
The majority of the existing reconfigurable hardware SAT solvers employ some variation of the Davis-Putnam algorithm; we propose a new algorithm for organizing the search in SAT Solvers best suited to reconfigurable architectures due to its vector-like operations. Its essence is to view each negated clause as a cube in the n-dimensional Boolean search space, and realizing that each of these clause-cubes denotes a sub-region of the search space where no satisfying assignments can be found. Starting from the universal cube, which represents the whole space, we systematically subtract all clause-cubes until we end up with a satisfying cube or an empty cube if the SAT formula is unsatisfiable. The algorithm for cube subtraction is the D-Sharp algorithm. We implemented this strategy in the well-known zChaff SAT solver. Improvements in execution time and number of aborted instances have been observed for the new algorithm. The test suite includes several instances from IBM-CNF BMC and Microprocessor's Formal Verification benchmarks. Given the breadth of the experimental software evaluation, we claim that D-Sharp subtraction search is an effective algorithm for improving the performance of SAT solvers and due to its data structure and bit-to-bit operations it is very well suited to reconfigurable hardware implementations. Design Automation (EDA).