# A Scalable Approximate Model Counter

arXiv: https://arxiv.org/abs/1306.5726 · HTML: https://mlsanity.com/paper/1306.5726/

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jun 2013.

## Built on by (most cited first, 20 of 20)

- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [Softened Symbol Grounding for Neuro-symbolic Systems](https://mlsanity.com/paper/2403.00323/) (2024)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [Fast Converging Anytime Model Counting](https://mlsanity.com/paper/2212.09390/) (2022)
- [Model Counting in the Wild](https://mlsanity.com/paper/2408.07059/) (2024)
- [CCDD: A Tractable Representation for Model Counting and Uniform Sampling](https://mlsanity.com/paper/2202.10025/) (2022)
- [IBIA: An Incremental Build-Infer-Approximate Framework for Approximate Inference of Partition Function](https://mlsanity.com/paper/2304.06366/) (2023)
- [PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas](https://mlsanity.com/paper/2312.15877/) (2023)
- [An ASP-Based Framework for MUSes](https://mlsanity.com/paper/2507.03929/) (2025)
- [QuantifyML: How Good is my Machine Learning Model?](https://mlsanity.com/paper/2110.12588/) (2021)
- [Answer Set Counting and its Applications](https://mlsanity.com/paper/2502.09231/) (2025)
- [Systematic Parameter Decision in Approximate Model Counting](https://mlsanity.com/paper/2504.05874/) (2025)
- [Efficient Certified Reasoning for Binarized Neural Networks](https://mlsanity.com/paper/2507.02916/) (2025)
- [Approximate SMT Counting Beyond Discrete Domains](https://mlsanity.com/paper/2507.18612/) (2025)
- [Structure-Preserving Margin Distribution Learning for High-Order Tensor Data with Low-Rank Decomposition](https://mlsanity.com/paper/2509.14577/) (2025)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)
- [A Fast Model Counting Algorithm for Two-Variable Logic with Counting and Modulo Counting Quantifiers](https://mlsanity.com/paper/2605.03391/) (2026)
- [CSB: A Counting and Sampling tool for Bit-vectors](https://mlsanity.com/paper/2607.04142/) (2026)

## Abstract (arXiv)

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.