Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of ApproxMC's approximation relies on a careful theoretical analysis of its randomized algorithm and the correctness of its highly optimized implementation, especially the latter's stateful interactions with an incremental CNF satisfiability solver capable of natively handling parity (XOR) constraints. We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates. We detail our general approach to establish a rigorous connection between these two parts of the verification, including our blueprint for turning the formalized, randomized algorithm into a verified proof checker, and our design of proof certificates for both ApproxMC and its internal CNF-XOR solving steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our certificate checker is able to fully certify $84.7\%$ of instances with generated certificates when given the same time and memory limits as the counter.

翻译：近似模型计数旨在估算输入布尔公式的解的数量。针对合取范式（CNF）公式的先进近似模型计数器ApproxMC，提供了一种可扩展的方法来获取具有概率近似正确（PAC）式保证的模型计数。然而，ApproxMC近似结果的有效性依赖于对其随机算法的严谨理论分析及其高度优化实现的正确性，尤其是后者与能够原生处理奇偶校验（XOR）约束的增量式CNF可满足性求解器之间的状态交互。我们提出了首个具有形式化验证输出近似质量保证的近似模型计数认证框架。我们的方法结合了：（i）在Isabelle/HOL证明助手中对算法PAC保证进行的静态一次性形式化证明；以及（ii）利用证明证书对ApproxMC调用外部CNF-XOR求解器进行动态逐轮验证。我们详述了建立这两部分验证之间严格联系的一般方法，包括将形式化的随机算法转化为可验证证明检查器的实施方案，以及为ApproxMC及其内部CNF-XOR求解步骤设计的证明证书结构。实验表明，证书生成对近似计数器实现带来的开销极小，且我们的证书检查器在获得与计数器相同的时间和内存限制时，能够对生成证书的实例实现$84.7\%$的完全认证。