Search-based SAT using zero-suppressed BDDs

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