# Rounding Meets Approximate Model Counting

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 28 references that are in the map.
- First posted on arXiv 16 May 2023.

## Builds on (most cited first, 11 of 11)

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [The Model Counting Competition 2020](https://mlsanity.com/paper/2012.01323/) (2020)
- [A Scalable Approximate Model Counter](https://mlsanity.com/paper/1306.5726/) (2013)
- [Distribution-Aware Sampling and Weighted Model Counting for SAT](https://mlsanity.com/paper/1404.2984/) (2014)
- [Taming the Curse of Dimensionality: Discrete Integration by Hashing and Optimization](https://mlsanity.com/paper/1302.6677/) (2013)
- [Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling](https://mlsanity.com/paper/2110.09026/) (2021)
- [Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice](https://mlsanity.com/paper/2004.14692/) (2020)
- [Constrained Sampling and Counting: Universal Hashing Meets SAT Solving](https://mlsanity.com/paper/1512.06633/) (2015)
- [Approximate Probabilistic Inference via Word-Level Counting](https://mlsanity.com/paper/1511.07663/) (2015)
- [Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation](https://mlsanity.com/paper/2206.02775/) (2022)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)

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

- [Locally-Minimal Probabilistic Explanations](https://mlsanity.com/paper/2312.11831/) (2023)
- [Formally Certified Approximate Model Counting](https://mlsanity.com/paper/2406.11414/) (2024)
- [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)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)

## Abstract (arXiv)

The problem of model counting, also known as #SAT, is to compute the number of models or satisfying assignments of a given Boolean formula F. Model counting is a fundamental problem in computer science with a wide range of applications. In recent years, there has been a growing interest in using hashing-based techniques for approximate model counting that provide (varepsilon, δ)-guarantees: i.e., the count returned is within a (1+varepsilon)-factor of the exact count with confidence at least 1-δ. While hashing-based techniques attain reasonable scalability for large enough values of δ, their scalability is severely impacted for smaller values of δ, thereby preventing their adoption in application domains that require estimates with high confidence. The primary contribution of this paper is to address the Achilles heel of hashing-based techniques: we propose a novel approach based on rounding that allows us to achieve a significant reduction in runtime for smaller values of δ. The resulting counter, called RoundMC, achieves a substantial runtime performance improvement over the current state-of-the-art counter, ApproxMC. In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows that RoundMC solves 204 more instances than ApproxMC, and achieves a 4× speedup over ApproxMC.
