Rounding Meets Approximate Model Counting

Abstract The problem of model counting, also known as $\#\textsf{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 , \delta )$ -guarantees: i.e., the count returned is within a $(1+\varepsilon )$ -factor of the exact count with confidence at least $1-\delta$ . While hashing-based techniques attain reasonable scalability for large enough values of $\delta$ , their scalability is severely impacted for smaller values of $\delta$ , 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 $\delta$ . The resulting counter, called $\textsf{ApproxMC6}$ (The resulting tool $\textsf{ApproxMC6}$ is available open-source at https://github.com/meelgroup/approxmc ), achieves a substantial runtime performance improvement over the current state-of-the-art counter, $\textsf{ApproxMC}$ . In particular, our extensive evaluation over a benchmark suite consisting of 1890 instances shows $\textsf{ApproxMC6}$ solves 204 more instances than $\textsf{ApproxMC}$ , and achieves a $4\times$ speedup over $\textsf{ApproxMC}$ .