舍入遇见近似模型计数

模型计数问题，亦称 #SAT，是计算给定布尔公式 $F$ 的模型数或满足赋值数。模型计数是计算机科学中的基本问题，具有广泛应用。近年来，基于哈希的近似模型计数技术日益受到关注，其提供 $(\varepsilon, \delta)$-保证：即返回计数在精确计数的 $(1+\varepsilon)$ 倍内，且置信度至少 $1-\delta$。虽然基于哈希的技术对足够大的 $\delta$ 值具备合理可扩展性，但其可扩展性在较小 $\delta$ 值时严重受限，从而阻碍了其在需要高置信度估计的应用领域的采用。本文的主要贡献是解决基于哈希技术的阿喀琉斯之踵：我们提出一种基于舍入的新方法，使得在较小 $\delta$ 值下运行时长显著减少。所得计数器称为 RoundMC，相较当前最先进计数器 ApproxMC 实现了大幅运行时性能提升。特别地，我们在由 1890 个实例组成的基准套件上的广泛评估表明，RoundMC 比 ApproxMC 多求解 204 个实例，并达到相对于 ApproxMC 的 $4\times$ 加速。