The Good Old Davis-Putnam Procedure Helps Counting Models

Abstract

As was shown recently, many important AI problems require counting the number of models of propositional formulas. The problem of counting models of such formulas is, according to present knowledge, computationally intractable in a worst case. Based on the Davis-Putnam procedure, we present an algorithm, CDP, that computes the exact number of models of a propositional CNF or DNF formula F. Let m and n be the number of clauses and variables of F, respectively, and let p denote the probability that a literal l of F occurs in a clause C of F, then the average running time of CDP is shown to be O(nm^d), where d=-1/log(1-p). The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.

Cited by in corpus (20)

• Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
• On the Relationship between Sum-Product Networks and Bayesian Networks
• The Language of Search
• Solving #SAT and Bayesian Inference with Backtracking Search
• Model Counting in Product Configuration
• Faster than Classical Quantum Algorithm for dense Formulas of Exact Satisfiability and Occupation Problems
• A Scalable Approximate Model Counter
• Sampling Techniques for Boolean Satisfiability
• Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
• Model Counting Modulo Theories
• Learning Branching Heuristics for Propositional Model Counting
• Conditioning Probabilistic Databases
• Probabilistic Databases with MarkoViews
• Bose-Einstein Condensation in Satisfiability Problems
• Bit-Vector Model Counting using Statistical Estimation
• Typical models: minimizing false beliefs
• A Graphical #SAT Algorithm for Formulae with Small Clause Density
• Counting Solutions of Constraint Satisfiability Problems:Exact Phase Transitions and Approximate Algorithm
• Phase Transitions in Knowledge Compilation: an Experimental Study
• High Dimensional Discrete Integration over the Hypergrid