Counting Models Using Connected Components

Roberto J. Bayardo Jr., IBM Almaden Research Center; J. D. Pehoushek, M.U.S.T. Centre

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.