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, \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 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\times$ speedup over ApproxMC.

翻译：模型计数问题，也称为#SAT，是计算给定布尔公式$F$的模型数量或满足赋值数量的问题。模型计数是计算机科学中的一个基本问题，具有广泛的应用。近年来，基于哈希技术的近似模型计数方法日益受到关注，这类方法提供$(\varepsilon, \delta)$-保证：即返回的计数结果与精确计数的偏差在$(1+\varepsilon)$因子内，且置信度至少为$1-\delta$。尽管哈希技术对于足够大的$\delta$值具有良好的可扩展性，但当$\delta$值较小时，其可扩展性会受到严重影响，从而阻碍了其在需要高置信度估计的应用领域中的采用。本文的主要贡献在于解决哈希技术的这一关键弱点：我们提出了一种基于舍入的新方法，能够在较小的$\delta$值下实现运行时间的显著降低。由此产生的计数器称为RoundMC，它在运行时性能上相较于当前最先进的计数器ApproxMC取得了实质性提升。特别是，我们对由1890个实例组成的基准测试套件进行了广泛评估，结果表明RoundMC比ApproxMC多解决了204个实例，并且比ApproxMC实现了4倍的加速。