A Scalable Approximate Model Counter
Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi

TL;DR
This paper introduces ApproxMC, a scalable approximate model counter for CNF formulas that provides high-confidence bounds close to the exact count, handling large problem sizes efficiently.
Contribution
It presents the first scalable approximate model counting algorithm for CNF formulas, using a polynomial number of SAT solver calls.
Findings
ApproxMC scales to formulas with tens of thousands of variables.
It provides bounds close to the exact count with high confidence.
It succeeds in large cases where exact counting is infeasible.
Abstract
Propositional model counting} (#SAT), i.e., counting the number of satisfying assignments of a propositional formula, is a problem of significant theoretical and practical interest. Due to the inherent complexity of the problem, approximate model counting, which counts the number of satisfying assignments to within given tolerance and confidence level, was proposed as a practical alternative to exact model counting. Yet, approximate model counting has been studied essentially only theoretically. The only reported implementation of approximate model counting, due to Karp and Luby, worked only for DNF formulas. A few existing tools for CNF formulas are bounding model counters; they can handle realistic problem sizes, but fall short of providing counts within given tolerance and confidence, and, thus, are not approximate model counters. We present here a novel algorithm, as well as a…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBayesian Modeling and Causal Inference · Markov Chains and Monte Carlo Methods · Machine Learning and Algorithms
