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/
Go to the corresponding LIPIcs Volume Portal


Fichte, Johannes K. ; Hecher, Markus ; Roland, Valentin

Proofs for Propositional Model Counting

pdf-format:
LIPIcs-SAT-2022-30.pdf (0.9 MB)


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}
}

Keywords: Model Counting, Verification, Certified Counting
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Source Code): https://github.com/vroland/sharptrace archived at: https://archive.softwareheritage.org/swh:1:dir:d945be2a2c32e1d5ab01d3fcf5042dec3c0b1839
Software (Source Code): https://github.com/vroland/sharpSAT/tree/proof-trace archived at: https://archive.softwareheritage.org/swh:1:dir:39ad2d798055b5632bf812a21f89131c364dabad
Software (Source Code): https://github.com/vroland/dp_on_dbs/tree/sharpsat_proof archived at: https://archive.softwareheritage.org/swh:1:dir:7d4d67c950dc9625c4adbebc6a1468cef16a5369
Software (Source Code): https://github.com/vroland/nnf2trace archived at: https://archive.softwareheritage.org/swh:1:dir:fcabb95ecc52d4dcd2a629da9022a4f5da9db0d7


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI