Formally Certified Approximate Model Counting

TL;DR

This work introduces the first certified framework for randomized approximate model counting, targeting ApproxMC by coupling a static PAC guarantee proven in Isabelle/HOL with per-run certificates for CNF-XOR solver calls. The approach balances theorem-proving with certificate checking: a formal abstract specification yields a PAC guarantee, which is then concretized into a verified CertCheck and an ApproxMCCert that can produce and verify partial certificates against an external CNF-XOR solver. The authors extend FRAT-XOR and related tooling, modify CryptoMiniSat, and implement a scalable certificate-checking pipeline that achieves full certification on a majority of instances and identifies practical bug fixes in real tooling. Experimental results show certificate generation incurs limited overhead and that CertCheck certifies a substantial fraction of instances within tight resource constraints, demonstrating practical viability for trusted probabilistic counting. The work lays a foundation for future enhancements (e.g., sparse hashing, rounding) and cross-theory certification, enabling broader trust in probabilistic model counting and its applications.

Abstract

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.

Figures (5)

• Figure 1: The certified approximate model counting workflow.
• Figure 2: An example pigeon-hole formula (2 pigeons, 5 holes, 180 solutions) in DIMACS format and a valid certificate for the checker at $\varepsilon=0.8$ and $\delta=0.2$ ($\emph{ 1000 1000 1000 1000 1000 1000 \small\normalfont\ttfamily\slshape thresh}=73, \emph{ 1000 1000 1000 1000 1000 1000 \small\normalfont\ttfamily\slshape t}=9$). The certificate is shown with colored comments and with redundant spaces added for clarity. In clauses, the negative (resp. positive) integers are negated (resp. positive) literals, with a 0 terminator; solutions are lists of literals assigned to true. Part of the certificate (marked with *) is checked with an external UNSAT proof checking pipeline.
• Figure 3: (top left) A sample input CNF-XOR formula where XOR lines start with x and indicate the literals that XOR to $1$, e.g., the line x 1 2 -3 represents the XOR constraint $x_1 \oplus x_2 \oplus \bar{x}_3 = 1$; (bottom left) a FRAT-XOR proof; (right) an XLRUP proof. The steps in bold indicate newly added XOR reasoning. Note that the XOR steps are (mostly) syntactically and semantically unchanged going from FRAT-XOR to XLRUP, so we focus on the latter here. The meaning of each XLRUP step (analogously for FRAT-XOR) is annotated in color-coded comments above the respective line.
• Figure 4: Per instance runtime (s) comparison for $\mathsf{ApproxMCCert}$ and $\mathsf{ApproxMC}$.
• Figure 5: (left) Runtime performance comparison between CNF-XOR unsatisfiability checkers. (right) Per instance CNF-XOR unsatisfiability proof size (bytes) comparison for $\mathsf{CMS}$+$\mathsf{frat}$-$\mathsf{xor}$ and $\mathsf{CMS}$+$\mathsf{tbuddy}$.

Theorems & Definitions (6)

• remark 1
• proof
• remark 2
• remark 3
• remark 4
• proof