Counting Models using Connected Components

Recent work by Birnbaum & Lozinskii [1999] demonstrated that a clever yet simple extension of the well-known Davis-Putnam procedure for solving instances of propositional satisfiability yields an efficient scheme for counting the number of satisfying assignments (models). We present a new extension, based on recursively identifying connected constraint-graph components, that substantially improves counting performance on random 3-SAT instances as well as benchmark instances from the SATLIB and Beijing suites. In addition, from a structure-based perspective of worst-case complexity, while polynomial time satisfiability checking is known to require only a backtrack search algorithm enhanced with nogood learning, we show that polynomial time counting using backtrack search requires an additional enhancement: good learning.