Analyzing Decision Heuristic Effectiveness in Boolean Satisfiability Solvers

Abstract

Boolean satisfiability (SAT) solvers have achieved impressive performance in practical settings. They are now heavily relied upon in formal verification and other industry applications. However, their degree of success not well understood, and it is not known how much room there is for improvement in performance through continued improvements in decision heuristics, whose development has been responsible for orders of magnitude of performance improvements in the past. In this report, we define a notion of dependency relations between events in solver execution that allows us to identify what portions of the work done by the solver on any given instance is required or could be avoided by changing the decision heuristic. We carry out experiments with practical application-focused benchmarks and find that most branches chosen by the decision heuristic are required, and a minority of work done by the solver is wasteful. This suggests limited improvements are still possible by improving decision heuristics alone if other aspects of SAT solvers are not improved.