Document Open Access Logo

Certified Knowledge Compilation with Application to Verified Model Counting

Authors Randal E. Bryant , Wojciech Nawrocki , Jeremy Avigad , Marijn J. H. Heule

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.6.pdf
  • Filesize: 0.88 MB
  • 20 pages

Document Identifiers

Author Details

Randal E. Bryant
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Wojciech Nawrocki
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
Jeremy Avigad
  • Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Bryant, Randal E.: Supported by NSF grant CCF-2108521.
  • Nawrocki, Wojciech: Hoskinson Center for Formal Mathematics
  • Avigad, Jeremy: Hoskinson Center for Formal Mathematics
  • Heule, Marijn J. H.: Supported by NSF grant CCF-2108521.

Cite AsGet BibTex

Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified Knowledge Compilation with Application to Verified Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.6

Abstract

Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision-decomposable, negation normal form (dec-DNNF) . Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from dec-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Propositional model counting
  • Proof checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Armin Biere. CaDiCaL at the SAT Race 2019. In Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B, pages 8-9. University of Helsinki, 2019. Google Scholar
  2. Manuel Blum, Ashok K. Chandra, and Mark N. Wegman. Equivalence of free Boolean graphs can be decided probabilistically in polynomial time. Information Processing Letters, 10(2):80-82, 18 March 1980. Google Scholar
  3. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Supplement to certified knowledge compilation with application to verified model counting, May 2023. URL: https://doi.org/10.5281/zenodo.7966174.
  4. Florent Capelli. Knowledge compilation languages as proof systems. In Theory and Applications of Satisfiability Testing (SAT), volume 11628 of LNCS, pages 90-91, 2019. Google Scholar
  5. Florent Capelli, Jean-Marie Lagniez, and Pierre Marquis. Certifying top-down decision-DNNF compilers. In AAAI Conference on Artificial Intelligence (AAAI), 2021. Google Scholar
  6. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Conference on Automated Deduction (CADE), volume 10395 of LNCS, pages 220-236, 2017. Google Scholar
  7. Adnan Darwiche. A compiler for deterministic, decomposable negation normal form. In Association for the Advancement of Artificial Intelligence (AAAI), 2002. Google Scholar
  8. Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In European Conference on Artificial Intelligence, pages 328-332, 2004. Google Scholar
  9. Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In International Joint Conference on Artificial Intelligence, pages 819-826, 2011. Google Scholar
  10. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17, 2002. Google Scholar
  11. Leonardo de Moura and Sebastian Ulrich. The Lean 4 theorem prover and programming language. In Conference on Automated Deduction (CADE), volume 12699 of LNAI, pages 625-635, 2021. Google Scholar
  12. Johannes K Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022. Google Scholar
  13. Evgueni I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe (DATE), pages 886-891, 2003. Google Scholar
  14. Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Nathan D. Wetzler. Efficient, verified checking of propositional proofs. In Interactive Theorem Proving, volume 10499 of LNCS, pages 269-284, 2017. Google Scholar
  15. Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan D. Wetzler. Verifying refutations with extended resolution. In Conference on Automated Deduction (CADE), volume 7898 of LNCS, pages 345-359, 2013. Google Scholar
  16. Marijn J. H. Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In International Joint Conference on Automated Reasoning (IJCAR), volume 8562 of LNCS, pages 91-106, 2014. Google Scholar
  17. Jinbo Huang and Adnan Darwiche. The language of search. Journal of Artificial Intelligence Research, 22:191-219, 2007. Google Scholar
  18. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of LNCS, pages 355-370, 2012. Google Scholar
  19. Angelika Kimmig, Guy Van den Broeck, and Luc De Raedt. Algebraic model counting. Journal of Applied Logic, 22:46-62, July 2017. Google Scholar
  20. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In International Joint Conference on Artificial Intelligence, pages 667-673, 2017. Google Scholar
  21. Peter Lammich. Efficient verified (UN)SAT certificate checking. J. Autom. Reason., 64(3):513-532, 2020. URL: https://doi.org/10.1007/s10817-019-09525-z.
  22. Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for Lean. In Certified Programs and Proofs (CPP), pages 253-266. ACM, 2023. URL: https://doi.org/10.1145/3573105.3575671.
  23. Mikaël Monet and Dan Olteanu. Towards deterministic decomposable circuits for safe queries. In Alberto Mendelzon International Workshop on Foundations of Data Management (AMW), 2018. Google Scholar
  24. Umut Oztok and Adnan Darwiche. On compiling CNF into decision-DNNF. In Constraint Programming (CP), volume 8656 of LNCS, pages 42-57, 2014. Google Scholar
  25. John A. Robinson. A machine-oriented logic based on the resolution principle. J.ACM, 12(1):23-41, January 1965. Google Scholar
  26. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in CakeML. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II, volume 12652 of LNCS, pages 223-241, 2021. Google Scholar
  27. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 466-483. Springer, 1983. Google Scholar
  28. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM Journal of Computing, 8(3):410-421, 1979. Google Scholar
  29. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In Proc. of the 10th Int. Symposium on Artificial Intelligence and Mathematics (ISAIM 2008), 2008. Google Scholar
  30. Nathan D. Wetzler, Marijn J. H. Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Theory and Applications of Satisfiability Testing (SAT), volume 8561 of LNCS, pages 422-429, 2014. Google Scholar
  31. Lintao Zhang and Sharad Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Design, Automation and Test in Europe (DATE), pages 880-885, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact