Document Open Access Logo

Proofs for Propositional Model Counting

Authors Johannes K. Fichte , Markus Hecher , Valentin Roland

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.30.pdf
  • Filesize: 0.91 MB
  • 24 pages

Document Identifiers

Author Details

Johannes K. Fichte
  • TU Wien, Austria
Markus Hecher
  • TU Wien, Austria
Valentin Roland
  • secunet Security Networks AG, Essen, Germany

Funding

Vienna Science and Technology Fund (WWTF) grant ICT19-065, the Austrian Science Fund (FWF) grants P32830 and Y698. Work has partially been carried out while Johannes Fichte and Markus Hecher were visiting the Simons Institute for the Theory of Computing at UC Berkeley.

Acknowledgements

Authors are stated in alphabetic order, gratefully acknowledge the valuable and extensive feedback by the anonymous reviewers, and discussions with Tobias Philipp (secunet).

Cite AsGet BibTex

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Proofs for Propositional Model Counting. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.30

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Mathematics of computing → Combinatorics
  • Software and its engineering → Formal software verification
Keywords
  • Model Counting
  • Verification
  • Certified Counting

Metrics

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

Supplementary Materials

References

  1. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and bayesian inference. In Proceedings of the 44th Symposium on Foundations of Computer Science, FOCS'03, pages 340-351, Cambridge, MA, USA, 2003. IEEE Computer Soc. URL: https://doi.org/10.1109/SFCS.2003.1238208.
  2. Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In Proceedings of the 43rd IEEE/ACM International Conference on Software Engineering, ICSE'21, pages 312-323, Madrid, 2021. IEEE Computer Soc. URL: https://doi.org/10.1109/ICSE43902.2021.00039.
  3. Pierre Bourhis, Laurence Duchien, Jérémie Dusart, Emmanuel Lonca, Pierre Marquis, and Clément Quinton. Pseudo polynomial-time top-k algorithms for d-DNNF circuits, 2022. URL: http://arxiv.org/abs/2202.05938.
  4. Robert Brummayer and Armin Biere. Fuzzing and delta-debugging SMT solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT'09, pages 1-5, Montreal, Canada, 2009. Association for Computing Machinery, New York. URL: https://doi.org/10.1145/1670412.1670413.
  5. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of sat and qbf solvers. In Ofer Strichman and Stefan Szeider, editors, Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT'10), volume 6175 of Lecture Notes in Computer Science, pages 44-57, Edinburgh, UK, July 2010. Springer Verlag. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  6. Florent Capelli. Knowledge compilation languages as proof systems. In Mikolás Janota and Inês Lynce, editors, Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing, volume 11628 of Lecture Notes in Computer Science, pages 90-99, Lisbon, 2019. Springer Verlag. URL: https://doi.org/10.1007/978-3-030-24258-9_6.
  7. Florent Capelli, Jean-Marie Lagniez, and Pierre Marquis. Certifying top-down decision-dnnf compilers. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI'21), pages 6244-6253, Virtual Event, 2021. The AAAI Press. Google Scholar
  8. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Improving approximate counting for probabilistic inference: From linear to logarithmic SAT solver calls. In Subbarao Kambhampati, editor, Proceedings of 25th International Joint Conference on Artificial Intelligence (IJCAI'16), pages 3569-3576, New York City, NY, USA, July 2016. The AAAI Press. Google Scholar
  9. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  10. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Proceedings of the 26th International Conference on Automated Deduction (CADE'17), volume 10395 of Lecture Notes in Computer Science, pages 220-236, Gothenburg, Sweden, 2017. Springer Verlag. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  11. Adnan Darwiche. Three modern roles for logic in AI. In Proceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS'20), pages 229-243, New York, NY, USA, 2020. Association for Computing Machinery, New York. URL: https://doi.org/10.1145/3375395.3389131.
  12. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. Journal of Artificial Intelligence Research, 17:229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  13. Emmanuelle Dietz, Johannes K. Fichte, and Florim Hamiti. A quantitative symbolic approach to individual human reasoning. In Proceedings of the 44th Annual Meeting of the Cognitive Science Society (CogSci'22), 2022. Google Scholar
  14. Jeffrey M. Dudek, Vu Phan, and Moshe Y. Vardi. ADDMC: weighted model counting with algebraic decision diagrams. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI'20), pages 1468-1476, New York, 2020. The AAAI Press. Google Scholar
  15. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. Dpmc: Weighted model counting by dynamic programming on project-join trees. In Helmut Simonis, editor, Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP'20), pages 211-230, Louvain-la-Neuve, Belgium, September 2020. Springer Verlag. Google Scholar
  16. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. Procount: Weighted projected model counting with graded project-join trees. In Chu-Min Li and Felip Manyà, editors, Proceedings of the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT'21), pages 152-170. Springer Verlag, 2021. Google Scholar
  17. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Satinder P. Singh and Shaul Markovitch, editors, Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI'17), pages 4488-4494, San Francisco, California, USA, 2017. The AAAI Press. Google Scholar
  18. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, volume 2919 of Lecture Notes in Computer Science, pages 502-518, Santa Margherita Ligure, Italy, 2003. Springer Verlag. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  19. Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying all differences using pseudo-boolean reasoning. Proceedings of the AAAI Conference on Artificial Intelligence, 34(02):1486-1494, April 2020. URL: https://doi.org/10.1609/aaai.v34i02.5507.
  20. Johannes K Fichte, Sarah Alice Gaggl, and Dominik Rusovac. Rushing and strolling among answer sets - navigation made easy. In AAAI'2022, 2022. Google Scholar
  21. Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. ACM Journal of Experimental Algorithmics, 26(13), December 2021. URL: https://doi.org/10.1145/3459080.
  22. Johannes K. Fichte, Markus Hecher, and Arne Meier. Knowledge-base degrees of inconsistency: Complexity and counting. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI'21), pages 6349-6357, 2021. Google Scholar
  23. Johannes K. Fichte, Markus Hecher, and Valentin Roland. GPUSAT3 benchmark data and source code, 2021. URL: https://doi.org/10.5281/zenodo.5159903.
  24. Johannes K. Fichte, Markus Hecher, and Valentin Roland. Parallel model counting with cuda: Algorithm engineering for efficient hardware utilization. In CP'21, 2021. Google Scholar
  25. Johannes Klaus Fichte, Markus Hecher, Ciaran McCreesh, and Anas Shahab. Complications for computational experiments from modern processors. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 25:1-25:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.25.
  26. Johannes Klaus Fichte, Markus Hecher, Patrick Thier, and Stefan Woltran. Exploiting database management systems and treewidth for counting. In Ekaterina Komendantskaya and Yanhong Annie Liu, editors, Proceedings of the 22nd International Symposium on Practical Aspects of Declarative Languages, volume 12007 of Lecture Notes in Computer Science, pages 151-167, New Orleans, LA, USA, 2020. Springer Verlag. URL: https://doi.org/10.1007/978-3-030-39197-3_10.
  27. Johannes Klaus Fichte, Norbert Manthey, Julian Stecklina, and André Schidler. Towards faster reasoners by using transparent huge pages. In Procs. of the 26th International Conference Principles and Practice of Constraint Programming (CP'20), volume 12333 of Lecture Notes in Computer Science, pages 267-285. Springer Verlag, September 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_18.
  28. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT competition 2020. Artificial Intelligence, 301:103572, 2021. URL: https://doi.org/10.1016/j.artint.2021.103572.
  29. Daniel E. Geer Jr. Complexity is the enemy. IEEE Security Privacy, 6(6):88-88, 2008. URL: https://doi.org/10.1109/MSP.2008.139.
  30. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In Proceedings of the International Symposium on Artificial Intelligence and Mathematics 2009, ISAIM'08, Fort Lauderdale, Florida, USA, 2008. Google Scholar
  31. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-boolean proofs. In Kevin Leyton-Brown and Mausam, editors, Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI'21), pages 3768-3777, 2021. Google Scholar
  32. Evguenii I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Proceedings of the Design, Automation and Test in Europe Conference and Exposition (DATE'03), pages 10886-10891, Munich, Germany, 2003. IEEE Computer Soc. URL: https://doi.org/10.1109/DATE.2003.10008.
  33. Ronald Lewis Graham, Martin Grötschel, and László Lovász. Handbook of combinatorics, volume I. Elsevier Science Publishers, North-Holland, 1995. Google Scholar
  34. Markus Hecher, Patrick Thier, and Stefan Woltran. Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology. In SAT'20, pages 343-360. Springer Verlag, 2020. Google Scholar
  35. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Maria Paola Bonacina, editor, Proceedings of the 24th International Conference on Automated Deduction (CADE'24), volume 7898 of Lecture Notes in Computer Science, pages 345-359, Lake Placid, NY, USA, 2013. Springer Verlag. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  36. Marijn J. H. Heule, Warren A. Hunt, and Nathan Wetzler. Expressing symmetry breaking in DRAT proofs. In Amy P. Felty and Aart Middeldorp, editors, Proceedings of the 25th International Conference on Automated Deduction Automated Deduction (CADE'25), pages 591-606. Springer Verlag, 2015. Google Scholar
  37. Jinbo Huang and Adnan Darwiche. DPLL with a trace: From SAT to knowledge compilation. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI'05), pages 156-162, Edinburgh, Scotland, UK, 2005. Professional Book Center. Google Scholar
  38. Matti Järvisalo, Marijn Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), volume 7364 of Lecture Notes in Computer Science, pages 355-370, Manchester, UK, June 2012. Springer Verlag. URL: https://doi.org/10.1007/978-3-642-31365-3_28.
  39. Matti Järvisalo, Marijn J. H. Heule, and Armin Biere. Inprocessing rules. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), pages 355-370. Springer Verlag, 2012. Google Scholar
  40. Mohimenul Kabir, Flavio Everardo, Ankit Shukla, Johannes K. Fichte, Markus Hecher, and Kuldeep Meel. ApproxASP - a scalable approximate answer set counter. In AAAI'2022, 2022. Google Scholar
  41. Hans Kleine Büning and Theodor Lettman. Propositional Logic: Deduction and Algorithms, volume 48 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1999. Google Scholar
  42. Tuukka Korhonen and Matti Järvisalo. Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming (CP'21), volume 210 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:11, Dagstuhl, Germany, 2021. Dagstuhl Publishing. URL: https://doi.org/10.4230/LIPIcs.CP.2021.8.
  43. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving model counting by leveraging definability. In Subbarao Kambhampati, editor, Proceedings of 25th International Joint Conference on Artificial Intelligence (IJCAI'16), pages 751-757, New York City, NY, USA, July 2016. The AAAI Press. Google Scholar
  44. Jean-Marie Lagniez and Pierre Marquis. An improved Decision-DDNF compiler. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI'17), pages 667-673, Melbourne, VIC, Australia, 2017. The AAAI Press. Google Scholar
  45. Anna L. D. Latour, Behrouz Babaki, Anton Dries, Angelika Kimmig, Guy Van den Broeck, and Siegfried Nijssen. Combining stochastic constraint optimization and probabilistic programming. In J. Christopher Beck, editor, Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP'17), pages 495-511. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_32.
  46. Christian J. Muise, Sheila A. McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-DNNF compilation with sharpSAT. In Leila Kosseim and Diana Inkpen, editors, Proceedings of the 25th Canadian Conference on Artificial Intelligence, volume 7310 of Lecture Notes in Computer Science, pages 356-361, Toronto, ON, Canada, 2012. Springer Verlag. URL: https://doi.org/10.1007/978-3-642-30353-1_36.
  47. Mohamed A. Nadeem, Johannes K. Fichte, and Markus Hecher. Plausibility reasoning via projected answer set counting - a hybrid approach. In IJCAI'22, 2022. To appear. Google Scholar
  48. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15), pages 3141-3148, Buenos Aires, Argentina, 2015. The AAAI Press. Google Scholar
  49. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  50. Tobias Philipp and Adrián Rebola-Pardo. DRAT proofs for XOR reasoning. In Loizos Michael and Antonis Kakas, editors, Proceedings of 15th European Conference on Logics in Artificial Intelligence (JELIA'16), pages 415-429. Springer Verlag, 2016. URL: https://doi.org/10.1007/978-3-319-48758-8_27.
  51. John Alan Robinson. A machine-oriented logic based on the resolution principle. Association for Computing Machinery, New York, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  52. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1-2):273-302, 1996. URL: https://doi.org/10.1016/0004-3702(94)00092-1.
  53. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), volume 4790 of Lecture Notes in Computer Science, pages 484-498, Yerevan, Armenia, 2007. Springer Verlag. URL: https://doi.org/10.1007/978-3-540-75560-9_35.
  54. Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), Vancouver, BC, Canada, 2004. Google Scholar
  55. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI'19), pages 1169-1176, Macao, China, 2019. IJCAI. Google Scholar
  56. Weijia Shi, Andy Shih, Adnan Darwiche, and Arthur Choi. On tractable representations of binary neural networks. In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR'20), pages 882-892, Rhodes, Greece, 2020. URL: https://doi.org/10.24963/kr.2020/91.
  57. Chico Sundermann, Thomas Thüm, and Ina Schaefer. Evaluating #SAT solvers on industrial feature models. In Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VAMOS '20), New York, NY, USA, 2020. Association for Computing Machinery, New York. URL: https://doi.org/10.1145/3377024.3377025.
  58. Marc Thurley. sharpSAT - counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes, editors, Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT'06), volume 4121 of Lecture Notes in Computer Science, pages 424-429, Seattle, WA, USA, 2006. Springer Verlag. URL: https://doi.org/10.1007/11814948_38.
  59. Leslie G. Valiant. The complexity of computing the permanent. Theoretical Computer Science, 8:189-201, 1979. URL: https://doi.org/10.1016/0304-3975(79)90044-6.
  60. Erik van der Kouwe, Dennis Andriesse, Herbert Bos, Cristiano Giuffrida, and Gernot Heiser. Benchmarking crimes: An emerging threat in systems security. CoRR, abs/1801.02381, 2018. URL: http://arxiv.org/abs/1801.02381.
  61. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Proceedings of the 17th International Conference Theory and Applications of Satisfiability Testing (SAT'14), pages 422-429, Vienna, Austria, July 2014. Springer Verlag. Held as Part of the Vienna Summer of Logic, VSL 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  62. Ennan Zhai, Ang Chen, Ruzica Piskac, Mahesh Balakrishnan, Bingchuan Tian, Bo Song, and Haoliang Zhang. Check before you change: Preventing correlated failures in service updates. In Ranjita Bhagwan and George Porter, editors, Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI'20), pages 575-589, Santa Clara, CA, USA, 2020. USENIX Association. 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