Tan, Y. K., Yang, J., Soos, M., Myreen, M. O., & Meel, K. S. (2024). Formally Certified Approximate Model Counting. In Computer Aided Verification (pp. 153–177). Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-65627-9_8
Abstract:
AbstractApproximate 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), $$\textsf{ApproxMC}$$
ApproxMC
, provides a scalable means of obtaining model counts with probably approximately correct (PAC)-style guarantees. Nevertheless, the validity of $$\textsf{ApproxMC}$$
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 $$\textsf{ApproxMC}$$
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 $$\textsf{ApproxMC}$$
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\%$$
84.7
%
of instances with generated certificates when given the same time and memory limits as the counter.
License type:
Attribution 4.0 International (CC BY 4.0)
Funding Info:
This research / project is supported by the National Research Foundation Singapore - NRF Fellowship Programme
Grant Reference no. : NRF-NRFFAI1-2019-0004
This research / project is supported by the Ministry of Education - Tier 2 Grant
Grant Reference no. : MOE-T2EP20121-0011
This research / project is supported by the Ministry of Education - Tier 1 Grant
Grant Reference no. : R-252-000-B59-114