Document Open Access Logo

Proof Complexity of Propositional Model Counting

Authors Olaf Beyersdorff , Tim Hoffmann , Luc Nicolas Spachmann

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.2.pdf
  • Filesize: 0.74 MB
  • 18 pages

Document Identifiers

Author Details

Olaf Beyersdorff
  • Friedrich-Schiller-Universität Jena, Germany
Tim Hoffmann
  • Friedrich-Schiller-Universität Jena, Germany
Luc Nicolas Spachmann
  • Friedrich-Schiller-Universität Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1.
  • Hoffmann, Tim: Carl-Zeiss Foundation.

Cite AsGet BibTex

Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof Complexity of Propositional Model Counting. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.2

Abstract

Recently, the proof system MICE for the model counting problem #SAT was introduced by Fichte, Hecher and Roland (SAT'22). As demonstrated by Fichte et al., the system MICE can be used for proof logging for state-of-the-art #SAT solvers. We perform a proof-complexity study of MICE. For this we first simplify the rules of MICE and obtain a calculus MICE' that is polynomially equivalent to MICE. Our main result establishes an exponential lower bound for the number of proof steps in MICE' (and hence also in MICE) for a specific family of CNFs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • model counting
  • #SAT
  • proof complexity
  • proof systems
  • lower bounds

Metrics

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

References

  1. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res., 40:353-373, 2011. Google Scholar
  2. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #sat and bayesian inference. In 44th Symposium on Foundations of Computer Science (FOCS 2003), 11-14 October 2003, Cambridge, MA, USA, Proceedings, pages 340-351. IEEE Computer Society, 2003. Google Scholar
  3. Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In 43rd IEEE/ACM International Conference on Software Engineering, ICSE 2021, Madrid, Spain, 22-30 May 2021, pages 312-323. IEEE, 2021. Google Scholar
  4. Olaf Beyersdorff and Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), volume 185 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:20, 2021. Google Scholar
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  6. Benjamin Böhm and Olaf Beyersdorff. Lower bounds for QCDCL via formula gauge. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing (SAT), pages 47-63, Cham, 2021. Springer International Publishing. Google Scholar
  7. Benjamin Böhm, Tomás Peitl, and Olaf Beyersdorff. QCDCL with cube learning or pure literal elimination - What is best? In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI), pages 1781-1787. ijcai.org, 2022. Google Scholar
  8. Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Knowledge compilation meets communication complexity. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI), pages 1008-1014. IJCAI/AAAI Press, 2016. Google Scholar
  9. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 233-350. IOS Press, 2021. Google Scholar
  10. Sam Buss and Neil Thapen. DRAT proofs, propagation redundancy, and extended resolution. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing (SAT), volume 11628 of Lecture Notes in Computer Science, pages 71-89. Springer, 2019. Google Scholar
  11. Florent Capelli. Knowledge compilation languages as proof systems. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing (SAT), volume 11628 of Lecture Notes in Computer Science, pages 90-99. Springer, 2019. Google Scholar
  12. Florent Capelli, Jean-Marie Lagniez, and Pierre Marquis. Certifying top-down decision-dnnf compilers. In Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI) 2021, pages 6244-6253. AAAI Press, 2021. Google Scholar
  13. Leroy Chew and Marijn J. H. Heule. Relating existing powerful proof systems for QBF. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 236 of LIPIcs, pages 10:1-10:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  14. Stephen A. Cook. The complexity of theorem proving procedures. In Proc. 3rd Annual ACM Symposium on Theory of Computing, pages 151-158, 1971. Google Scholar
  15. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. Google Scholar
  16. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 4488-4494. AAAI Press, 2017. Google Scholar
  17. Johannes Klaus Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. ACM J. Exp. Algorithmics, 26:13:1-13:26, 2021. Google Scholar
  18. Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 30:1-30:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  19. 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, Practical Aspects of Declarative Languages - 22nd International Symposium, PADL 2020, New Orleans, LA, USA, January 20-21, 2020, Proceedings, volume 12007 of Lecture Notes in Computer Science, pages 151-167. Springer, 2020. Google Scholar
  20. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 993-1014. IOS Press, 2021. Google Scholar
  21. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  22. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, pages 345-359, 2013. Google Scholar
  23. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. J. Autom. Reason., 58(1):97-125, 2017. Google Scholar
  24. Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 667-673. ijcai.org, 2017. Google Scholar
  25. Anna L. D. Latour, Behrouz Babaki, Anton Dries, Angelika Kimmig, Guy Van den Broeck, and Siegfried Nijssen. Combining stochastic constraint optimization and probabilistic programming - From knowledge compilation to constraint solving. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10416 of Lecture Notes in Computer Science, pages 495-511. Springer, 2017. Google Scholar
  26. João P. Marques Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. Google Scholar
  27. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  28. 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 2020, Rhodes, Greece, September 12-18, 2020, pages 882-892, 2020. Google Scholar
  29. Marc Thurley. sharpSAT - Counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 424-429. Springer, 2006. Google Scholar
  30. Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput., 20(5):865-877, 1991. Google Scholar
  31. Moshe Y. Vardi. Boolean satisfiability: Theory and engineering. Commun. ACM, 57(3):5, 2014. Google Scholar
  32. Marc Vinyals. Hard examples for common variable decision heuristics. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI), 2020. Google Scholar
  33. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. Drat-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing (SAT, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014. Google Scholar
  34. 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, 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, February 25-27, 2020, pages 575-589. USENIX Association, 2020. 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