# Systematic Parameter Decision in Approximate Model Counting

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 11 of its 29 references that are in the map.
- First posted on arXiv 8 Apr 2025.

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

- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [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)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [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)

## Abstract (arXiv)

This paper proposes a novel approach to determining the internal parameters of the hashing-based approximate model counting algorithm mathsfApproxMC. In this problem, the chosen parameter values must ensure that mathsfApproxMC is Probably Approximately Correct (PAC), while also making it as efficient as possible. The existing approach to this problem relies on heuristics; in this paper, we solve this problem by formulating it as an optimization problem that arises from generalizing mathsfApproxMC's correctness proof to arbitrary parameter values. Our approach separates the concerns of algorithm soundness and optimality, allowing us to address the former without the need for repetitive case-by-case argumentation, while establishing a clear framework for the latter. Furthermore, after reduction, the resulting optimization problem takes on an exceptionally simple form, enabling the use of a basic search algorithm and providing insight into how parameter values affect algorithm performance. Experimental results demonstrate that our optimized parameters improve the runtime performance of the latest mathsfApproxMC by a factor of 1.6 to 2.4, depending on the error tolerance.