Model Counting: A New Strategy for Obtaining Good Bounds

Model counting is the classical problem of computing the number of solutions of a given propositional formula. It vastly generalizes the NP-complete problem of propositional satisfiability, and hence is both highly useful and extremely expensive to solve in practice. We present a new approach to model counting that is based on adding a carefully chosen number of so-called streamlining constraints to the input formula in order to cut down the size of its solution space in a controlled manner. Each of the additional constraints is a randomly chosen XOR or parity constraint on the problem variables, represented either directly or in the standard CNF form. Inspired by a related yet quite different theoretical study of the properties of XOR constraints, we provide a formal proof that with high probability, the number of XOR constraints added in order to bring the formula to the boundary of being unsatisfiable determines with high precision its model count. Experimentally, we demonstrate th...

• Type: Conference
• Year: 2006
• Where: AAAI
• Authors: Carla P. Gomes, Ashish Sabharwal, Bart Selman
• Keywords: AAAI 2006, Intelligent Agents, Model Counting, So-called Streamlining Constraints, XOR Constraints