2026-08-16T22:55:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16704 2024-03-06T10:58:06Z ddc:004 open_access

Proofs for Propositional Model Counting Fichte, Johannes K. Hecher, Markus Roland, Valentin Model Counting Verification Certified Counting 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Johannes K. Fichte and Markus Hecher and Valentin Roland 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.30 urn:nbn:de:0030-drops-167043 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.30 eng https://creativecommons.org/licenses/by/4.0/legalcode