# Formally Certified Approximate Model Counting

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 61 references that are in the map.
- First posted on arXiv 17 Jun 2024.

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

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Distribution-Aware Sampling and Weighted Model Counting for SAT](https://mlsanity.com/paper/1404.2984/) (2014)
- [Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs](https://mlsanity.com/paper/2209.12185/) (2022)
- [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)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation](https://mlsanity.com/paper/2206.02775/) (2022)
- [A Verified Compiler for Probability Density Functions](https://mlsanity.com/paper/1707.06901/) (2017)
- [Certifying Certainty and Uncertainty in Approximate Membership Query Structures -- Extended Version](https://mlsanity.com/paper/2004.13312/) (2020)
- [A Flexible Proof Format for SAT Solver-Elaborator Communication](https://mlsanity.com/paper/2109.09665/) (2021)
- [Proof Generation for CDCL Solvers Using Gauss-Jordan Elimination](https://mlsanity.com/paper/2304.04292/) (2023)
- [CertiStr: A Certified String Solver (technical report)](https://mlsanity.com/paper/2112.06039/) (2021)
- [Auditable Algorithms for Approximate Model Counting](https://mlsanity.com/paper/2312.12362/) (2023)

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

- [Efficient Certified Reasoning for Binarized Neural Networks](https://mlsanity.com/paper/2507.02916/) (2025)

## Abstract (arXiv)

Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of ApproxMC's approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter's stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints. We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both ApproxMC and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify 84.7% of instances with generated certificates when given the same time and memory limits as the counter.