Roberto J. Bayardo Jr., IBM Almaden Research Center; J. D. Pehoushek, M.U.S.T. Centre
Recent work by Birnbaum and Lozinskii  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.