Chaff: Engineering an Efficient SAT Solver

Overview

The study discussed in this paper has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. This paper describes the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean Constraint Propagation (BCP) and a novel low overhead decision strategy.