License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.30
URN: urn:nbn:de:0030-drops-167043
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16704/
Fichte, Johannes K. ;
Hecher, Markus ;
Roland, Valentin
Proofs for Propositional Model Counting
Abstract
Although propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed.
As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment.
BibTeX - Entry
@InProceedings{fichte_et_al:LIPIcs.SAT.2022.30,
author = {Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
title = {{Proofs for Propositional Model Counting}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {30:1--30:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16704},
URN = {urn:nbn:de:0030-drops-167043},
doi = {10.4230/LIPIcs.SAT.2022.30},
annote = {Keywords: Model Counting, Verification, Certified Counting}
}
