Search-Based SAT Using Zero-Suppressed BDDs
Fadi Aloul, Maher N. Mneimneh, Karem A. Sakallah · 2002
We introduce a new approach to Boolean satisfiability (SAT) that combines backtrack search techniques and zero-suppressed binary decision diagrams (ZBDDs). This approach implicitly represents SAT instances using ZBDDs, and performs search using an efficient implementation of unit propagation on the ZBDD structure. The adaptation of backtrack search algorithms to such an implicit representation allows for a potential exponential increase in the size of problems that can be handled. Introduction. Many efficient enhancements to the Davis-Logemann-Loveland (DLL) backtrack-search procedure have been proposed. These enhancements extended the application of SAT solvers to large problem instances. Nevertheless, despite these advances, the tremendous growth in