C.A. Micchelli, W.L. Miranker
Journal of the ACM
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.
C.A. Micchelli, W.L. Miranker
Journal of the ACM
Saurabh Paul, Christos Boutsidis, et al.
JMLR
Joxan Jaffar
Journal of the ACM
Kenneth L. Clarkson, Elad Hazan, et al.
Journal of the ACM