A Fast SAT Solver Strategy Based on Negated Clauses

We propose a new algorithm for organizing the search in DPLL-based SAT solvers. Each negated clause is viewed as a cube in the n-dimensional Boolean search space denoting a sub-space where no satisfying assignments can be found. The algorithm systematically subtracts all clause-cubes from the universal cube that represents the entire n-dimensional Boolean search space. If the result is an empty cube then the problem is unsatisfiable; else the problem is satisfiable. We show that this algorithm can be implemented by modifying the decision engine of a DPLL-based SAT solver to use information extracted from the conflict analysis engine. Intuitively, this algorithm is more deterministic, exploits locality better and learns more useful clauses. We tested this idea in a basic DPLL SAT solver, in a DPLL solver featuring clause learning and in the well-known zChaff solver. The test suite includes 1075 problem instances from the DIMACs, IBM-CNF, BMC, and microprocessor formal verification benchmarks. Significant improvements in execution time and number of aborted instances have been observed in all cases. Given the breadth of the experimental evaluation, we claim that disjoint cube subtraction search is an effective algorithm for improving the performance of SAT solvers