Classified by Research TopicSorted by DateClassified by Publication Type

Formally Certified Approximate Model Counting

Formally Certified Approximate Model Counting.
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), July 2024.
Distinguished Paper Award

Download

[PDF] 

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. Nev- ertheless, 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 inter- actions 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 out- put approximation. Our approach combines: (i) a static, once-off, for- mal 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 gen- eral 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 solv- ing steps. Experimentally, we show that certificate generation adds little overhead to an approximate counter implementation, and that our cer- tificate checker is able to fully certify 84.7% of instances with generated certificates when given the same time and memory limits as the counter.

BibTeX

@inproceedings{tysmm24,
title={Formally Certified Approximate Model Counting},
author={Tan, Yong Kiam and 
              Yang, Jiong
              and Soos, Mate
              and Myreen, Magnus O. 
              and Meel, Kuldeep S.
              },
 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. Nev-
 ertheless, 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 inter-
 actions 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 out-
 put approximation. Our approach combines: (i) a static, once-off, for-
 mal 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 gen-
 eral 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 solv-
 ing steps. Experimentally, we show that certificate generation adds little
 overhead to an approximate counter implementation, and that our cer-
 tificate checker is able to fully certify 84.7% of instances with generated
 certificates when given the same time and memory limits as the counter.
},
month=jul,
year={2024},
booktitle=CAV,
note={Distinguished Paper Award},
bib2html_rescat={Counting},	
bib2html_pubtype={Refereed Conference,Award Winner},
bib2html_dl_pdf={https://arxiv.org/pdf/2406.11414},
}

Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Aug 22, 2024 18:37:34