Document Open Access Logo

Certifying Projected Knowledge Compilation

Authors Randal E. Bryant , Yong Kiam Tan , Marijn J. H. Heule

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.8.pdf
  • Filesize: 1.15 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.8.html

Document Identifiers

Subject Classification

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

Metrics

Abstract

Knowledge compilers convert Boolean formulas, given in conjunctive normal form (CNF), into representations that enable efficient evaluation of unweighted and weighted model counts, as well as a variety of other useful properties. With projected knowledge compilation, the generated representation describes the restriction of the formula to a designated set of data variables, with the remaining ones eliminated by existential quantification. Projected knowledge compilation has applications in a variety of domains, including formal verification and synthesis.
This paper describes a formally verified proof framework for certifying the output of a projected knowledge compiler. It builds on an earlier clausal proof framework for certifying the output of a standard knowledge compiler. Extending the framework to projected compilation requires a method to represent Skolem assignments, describing how the quantified variables can be assigned, given an assignment for the data variables. We do so by extending the representation generated by the knowledge compiler to also encode Skolem assignments. We also refine the earlier framework, moving beyond purely clausal proofs to enable scaling certification to larger formulas.
We present experimental results obtained by making small modifications to the D4 projected knowledge compiler and extensions of our earlier proof generator. We detail a soundness argument stating that a compiler output that passes our certifier is logically equivalent to the quantified input formula; the soundness argument has been formally validated using the HOL4 proof assistant. The checker also ensures that the compiler output satisfies the properties required for efficient unweighted and weighted model counting. We have developed two proof checkers for the certification framework: one written in C and designed for high performance and one written in CakeML and formally verified in HOL4.

Cite As Get BibTex

Randal E. Bryant, Yong Kiam Tan, and Marijn J. H. Heule. Certifying Projected Knowledge Compilation. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.8

Author Details

Randal E. Bryant
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Yong Kiam Tan
  • Institute for Infocomm Research (I²R), A*STAR, Singapore
  • Nanyang Technological University, Singapore
Marijn J. H. Heule
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Bryant, Randal E.: National Science Foundation, NSF grant CCF-2108521.
  • Tan, Yong Kiam: Singapore NRF Fellowship Programme NRF-NRFF16-2024-0002.
  • Heule, Marijn J. H.: National Science Foundation, NSF grant CCF-2108521.

Supplementary Materials

References

  1. Rehan Abdul Aziz, Geoffrey Chu, Christian Muise, and Peter Stuckey. #∃SAT: Projected model counting. In Theory and Applications of Satisfiability Testing (SAT), volume 9340 of LNCS, pages 121-137, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_10.
  2. Valeriy Balabanov and Jie-Hong Roland Jiang. Unified QBF certification and its applications. Formal Methods in Systems Design, 41:45-65, 2012. URL: https://doi.org/10.1007/S10703-012-0152-6.
  3. Marco Benedetti. Evaluating QBFs via symbolic Skolemization. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 3452 of LNCS, pages 285-300, 2005. URL: https://doi.org/10.1007/978-3-540-32275-7_20.
  4. Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kasche Kaspar. The relative strength of #SAT proof systems. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl, July 2024. Google Scholar
  5. Olaf Beyersdorff, Tim Hoffman, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl, July 2023. Google Scholar
  6. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to verified model counting. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl, July 2023. Google Scholar
  7. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to formally verified model counting. Journal of Artificial Intelligence Research, 82:2057-2099, 2025. URL: https://doi.org/10.1613/JAIR.1.15958.
  8. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 10^20 states and beyond. Information and Computation, 98(2):142-170, 1992. URL: https://doi.org/10.1016/0890-5401(92)90017-A.
  9. 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
  10. Florent Capelli, Jean-Marie Lagniez, and Pierre Marquis. Certifying top-down decision-DNNF compilers. In AAAI Conference on Artificial Intelligence, 2021. Google Scholar
  11. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172:772-799, 2008. URL: https://doi.org/10.1016/J.ARTINT.2007.11.002.
  12. Sravanthi Chede, Leroy N. Chew, and Anil Shukla. Circuits, proofs, and propositional model counting. In Foundations of Software Technology and Theoretical Computer Science (FTTCS), 2024. Google Scholar
  13. Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In Symposium on Logic in Computer Science (LICS), pages 353-362. IEEE, 1989. URL: https://doi.org/10.1109/LICS.1989.39190.
  14. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 2014. Google Scholar
  15. Adnan Darwiche. Decomposable negation normal form. Journal of the ACM, 48(4):608-647, 2001. URL: https://doi.org/10.1145/502090.502091.
  16. Adnan Darwiche. On the tractable counting of theory models and its application to truth maintenance and belief revision. Journal of Applications of Non Classical Logics, 11(1-2):11-34, 2001. URL: https://doi.org/10.3166/JANCL.11.11-34.
  17. Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In European Conference on Artificial Intelligence, pages 328-332, 2004. Google Scholar
  18. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17, 2002. URL: https://doi.org/10.1613/JAIR.989.
  19. 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. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  20. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. ProCount: Weighted projected model counting with graded project-join trees. In Theory and Applications of Satisfiability Testing (SAT), volume 12831 of LNCS, pages 152-170, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_11.
  21. Thomas Eiter and Gabriele Kern-Isberner. A brief survey of forgetting from a knowledge representation and reasoning perspective. Künstliche Intelligenz, 33:9-33, 2019. URL: https://doi.org/10.1007/S13218-018-0564-6.
  22. Johannes K. Fichte, Markus Hecher, Michael Morak, Patrick Thier, and Stefan Woltran. Solving projected model counting by utilizing treewidth and its limits. Artificial Intelligence, 314, 2023. URL: https://doi.org/10.1016/J.ARTINT.2022.103810.
  23. Johannes K Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Theory and Applications of Satisfiability Testing (SAT). Schloss Dagstuhl, 2022. Google Scholar
  24. Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-end verification for subgraph solving. In AAAI Conference on Artificial Intelligence, pages 8038-8047, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28642.
  25. 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
  26. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Handbook of Satisfiability, pages 633-654. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-633.
  27. Rafael Kiesel and Thomas Eiter. Knowledge compilation and more with SharpSAT-TD. In Principles of Knowledge Representation and Reasoning, pages 406-416, 2023. URL: https://doi.org/10.24963/KR.2023/40.
  28. Angelika Kimmig, Guy Van den Broeck, and Luc De Raedt. Algebraic model counting. Journal of Applied Logic, 22:46-62, July 2017. URL: https://doi.org/10.1016/J.JAL.2016.11.031.
  29. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, POPL, pages 179-192. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  30. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In International Joint Conference on Artificial Intelligence (IJCAI), pages 667-673, 2017. URL: https://doi.org/10.24963/IJCAI.2017/93.
  31. Jean-Marie Lagniez and Pierre Marquis. A recursive algorithm for projected model counting. In AAAI Conference on Artificial Intelligence, pages 1536-1543, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011536.
  32. Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic blocked clause elimination for projected model counting. In Theory and Applications of Satisfiability Testing (SAT), 2024. Google Scholar
  33. Fangzhen Lin and Ray Reiter. Forget it! In AAAI Fall Symposium on Relevance, pages 154-159, 1994. Google Scholar
  34. Pierre Marquis. Knowledge compilation using theory prime implicates. In International Joint Conference on Artificial Intelligence (IJCAI), pages 837-843, 1995. Google Scholar
  35. Sybylle Möhle and Armin Biere. Dualizing projected model counting. In IEEE Conference on Tools with Artificial Intelligence, pages 702-709, 2018. Google Scholar
  36. Christian Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric Hsu. DSHARP: Fast d-DNNF compilation with sharpSAT. In Canadian Conference on Artificial Intelligence, volume 7310 of LNCS, pages 356-361, 2012. URL: https://doi.org/10.1007/978-3-642-30353-1_36.
  37. David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293-304, 1986. URL: https://doi.org/10.1016/S0747-7171(86)80028-1.
  38. Steven Prestwich. CNF encodings. In Handbook of Satisfiability, pages 75-97. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-75.
  39. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In International Joint Conference on Artificial Intelligence (IJCAI), pages 1169-1176, 2019. URL: https://doi.org/10.24963/IJCAI.2019/163.
  40. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Theorem Proving in Higher Order Logics, volume 5170 of LNCS. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  41. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. Verified progagation redundancy and compositional UNSAT checking in CakeML. International Journal of Software Tools for Technology Transfer, 25:167-184, 2023. URL: https://doi.org/10.1007/S10009-022-00690-Y.
  42. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. J. Funct. Program., 29:e2, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  43. 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
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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