Systematic Parameter Decision in Approximate Model Counting
Jinping Lei, Toru Takisaka, Junqiang Peng, Mingyu Xiao
TL;DR
The paper addresses the challenge of choosing internal parameters for the hashing-based approximate model counter ApproxMC to achieve PAC guarantees while minimizing runtime. It reframes parameter selection as an optimization problem: derive a soundness condition from the ApproxMC6 correctness proof and minimize an objective that proxies runtime, with a key reduction from an eight-dimensional search to a two-dimensional box. A central result is the formal separation of soundness and optimality, enabling a straightforward, finite search for optimal parameters under the soundness constraints, and the introduction of FlexMC, which uses optimal parameters to accelerate computation. Experimental results show FlexMC speeds up ApproxMC6 by roughly $1.65$ to $2.46\times$ across various $\varepsilon$ settings, with improved balancing of failure bounds $p_L$ and $p_U$ and tighter runtime behavior. The approach is general, robust to revisions of ApproxMC, and provides a principled framework for parameter decision in hashing-based counting and related algorithms.
Abstract
This paper proposes a novel approach to determining the internal parameters of the hashing-based approximate model counting algorithm $\mathsf{ApproxMC}$. In this problem, the chosen parameter values must ensure that $\mathsf{ApproxMC}$ 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 $\mathsf{ApproxMC}$'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 $\mathsf{ApproxMC}$ by a factor of 1.6 to 2.4, depending on the error tolerance.