A Scalable Approximate Model Counter

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 reference implementation, that is the first scalable approximate model counter for CNF formulas. The algorithm works by issuing a polynomial number of calls to a SAT solver. Our tool, ApproxMC, scales to formulas with tens of thousands of variables. Careful experimental comparisons show that ApproxMC reports, with high confidence, bounds that are close to the exact count, and also succeeds in reporting bounds with small tolerance and high confidence in cases that are too large for computing exact model counts.

Conference version will appear in CP 2013

References in corpus (2)

• The Good Old Davis-Putnam Procedure Helps Counting Models
• Uniform Solution Sampling Using a Constraint Solver As an Oracle

Cited by in corpus (11)

• Balancing Scalability and Uniformity in SAT Witness Generator
• Constrained Sampling and Counting: Universal Hashing Meets SAT Solving
• Approximate Probabilistic Inference via Word-Level Counting
• Constrained Counting and Sampling: Bridging the Gap between Theory and Practice
• Combining the $k$-CNF and XOR Phase-Transitions
• Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
• Probabilistic Program Abstractions
• Bit-Vector Model Counting using Statistical Estimation
• Probabilistic Model Counting with Short XORs
• Approximate Model Counting, Sparse XOR Constraints and Minimum Distance
• A New Probabilistic Algorithm for Approximate Model Counting