A New Probabilistic Algorithm for Approximate Model Counting
This addresses a need in AI and software analysis for efficient model counting, but it appears incremental as it builds on existing hashing-based approaches.
The paper tackles the problem of approximate model counting for constraints by proposing a new probabilistic polynomial-time algorithm that uses only satisfiability queries, showing promising results on benchmarks for propositional logic and SMT(BV) formulas.
Constrained counting is important in domains ranging from artificial intelligence to software analysis. There are already a few approaches for counting models over various types of constraints. Recently, hashing-based approaches achieve both theoretical guarantees and scalability, but still rely on solution enumeration. In this paper, a new probabilistic polynomial time approximate model counter is proposed, which is also a hashing-based universal framework, but with only satisfiability queries. A variant with a dynamic stopping criterion is also presented. Empirical evaluation over benchmarks on propositional logic formulas and SMT(BV) formulas shows that the approach is promising.