Counting Models Using Connected Components

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Constraint Satisfaction

Recent work by Birnbaum and 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 disconnected constraint-graph components, that substantially improves counting performance. Experiments are performed on random 3-SAT instances as well as instances from the SATLIB and Beijing benchmark suites. In addition, we show that from a structure-based perspective of worst-case complexity, counting models appears to be no harder than determining satisfiability.