Document Open Access Logo

The Relative Strength of #SAT Proof Systems

Authors Olaf Beyersdorff , Johannes K. Fichte , Markus Hecher , Tim Hoffmann , Kaspar Kasche

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.5.pdf
  • Filesize: 0.94 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Model Counting
  • #SAT
  • Proof Complexity
  • Proof Systems
  • Lower Bounds
  • Knowledge Compilation

Metrics

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

Abstract

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps (knowledge compilation proof system), MICE (model counting induction by claim extension), and CPOG (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers.
Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.

Cite As Get BibTex

Olaf Beyersdorff, Johannes K. Fichte, Markus Hecher, Tim Hoffmann, and Kaspar Kasche. The Relative Strength of #SAT Proof Systems. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.5

Author Details

Olaf Beyersdorff
  • Friedrich Schiller University Jena, Germany
Johannes K. Fichte
  • Linköping University, Sweden
Markus Hecher
  • Massachusetts Institute of Technology, Cambridge, MA, USA
Tim Hoffmann
  • Friedrich Schiller University Jena, Germany
Kaspar Kasche
  • Friedrich Schiller University Jena, Germany

Funding

  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1
  • Fichte, Johannes K.: ELLIIT (Excellence Center at Linköping - Lund in Information Technology) funded by the Swedish government
  • Hecher, Markus: Austrian Science Fund (FWF) grant J4656, Vienna Science and Technology Fund (WWTF) grant ICT19-065, and Society for Research Funding Lower Austria (GFF) grant ExzF-0004
  • Hoffmann, Tim: Carl-Zeiss Foundation
  • Kasche, Kaspar: Carl-Zeiss Foundation

Acknowledgements

Parts of the work has been carried out while the first four authors were visiting the Simons Institute for Theory of Computation at UC Berkeley.

References

  1. Handbook of satisfiability, 2021. Google Scholar
  2. S. Akshay, Supratik Chakraborty, and Kuldeep S. Meel. Auditable Algorithms for Approximate Model Counting. In AAAI'24, 2024. Google Scholar
  3. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. Theory Comput., 3(1):81-102, 2007. URL: https://doi.org/10.4086/toc.2007.v003a005.
  4. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. JAIR, 40:353-373, 2011. URL: https://doi.org/10.1613/jair.3152.
  5. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #sat and bayesian inference. In FOCS'03, pages 340-351, 2003. URL: https://doi.org/10.1109/SFCS.2003.1238208.
  6. Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In ICSE'21, pages 312-323, 2021. URL: https://doi.org/10.1109/ICSE43902.2021.00039.
  7. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. JAIR, 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  8. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, 2004. URL: https://doi.org/10.1007/s00493-004-0036-5.
  9. Olaf Beyersdorff. Proof complexity of quantified Boolean logic - a survey. In Mathematics for Computation (M4C), pages 353-391. World Scientific Publishing Company, Singapore, 2022. Google Scholar
  10. Olaf Beyersdorff and Benjamin Böhm. Understanding the relative strength of QBF CDCL solvers and QBF resolution. LMCS, 19(2), 2023. URL: https://doi.org/10.46298/lmcs-19(2:2)2023.
  11. Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. In SAT'23, volume 271, pages 2:1-2:18, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.2.
  12. Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. ECCC, pages TR24-030, 2024. URL: https://eccc.weizmann.ac.il/report/2024/030.
  13. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified Boolean formulas. In Handbook of Satisfiability, pages 1177-1221. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201015.
  14. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. Exponential separations between restricted resolution and cutting planes proof systems. In FOCS'98, pages 638-647, 1998. URL: https://doi.org/10.1109/SFCS.1998.743514.
  15. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Certified knowledge compilation with application to verified model counting. In SAT'23, volume 271, pages 6:1-6:20, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.6.
  16. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Handbook of Satisfiability, pages 233-350. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200990.
  17. Florent Capelli. Understanding the complexity of #sat using knowledge compilation. In LICS'17, pages 1-10, 2017. URL: https://doi.org/10.1109/LICS.2017.8005121.
  18. Florent Capelli. Knowledge compilation languages as proof systems. In SAT'19, volume 11628, pages 90-99, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_6.
  19. Leroy Chew and Marijn J. H. Heule. Relating existing powerful proof systems for QBF. In SAT'22, volume 236, pages 10:1-10:22, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.10.
  20. Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook, volume 43, pages 143-152. ACM Books, 2023. URL: https://doi.org/10.1145/3588287.3588297.
  21. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. JSL, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  22. Adnan Darwiche. Compiling knowledge into decomposable negation normal form. In IJCAI'99, pages 284-289, 1999. URL: http://ijcai.org/Proceedings/99-1/Papers/042.pdf.
  23. Adnan Darwiche. On the tractable counting of theory models and its application to truth maintenance and belief revision. JANCL, 11(1-2):11-34, 2001. URL: https://doi.org/10.3166/jancl.11.11-34.
  24. Adnan Darwiche. A compiler for deterministic, decomposable negation normal form. In AAAI'02, pages 627-634, 2002. URL: http://www.aaai.org/Library/AAAI/2002/aaai02-094.php.
  25. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. JAIR, 17:229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  26. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In AAAI'17, pages 4488-4494, 2017. URL: https://doi.org/10.1609/aaai.v31i1.11178.
  27. Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. JEA, 26(1):1-26, 2021. URL: https://doi.org/10.1145/3459080.
  28. Johannes Klaus Fichte, Markus Hecher, and Valentin Roland. Proofs for propositional model counting. In SAT'22, volume 236, pages 30:1-30:24, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.30.
  29. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In ISAIM'08, 2008. Google Scholar
  30. Evguenii I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In DATE, pages 10886-10891, 2003. URL: https://doi.org/10.1109/DATE.2003.10008.
  31. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Model counting. In Handbook of Satisfiability, volume 336, pages 993-1014. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201009.
  32. Amin Haken. The intractability of resolution. TCS, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  33. Markus Hecher, Patrick Thier, and Stefan Woltran. Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology. In SAT'20, volume 12178, pages 343-360, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_25.
  34. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In CADE'13, pages 345-359, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  35. Marijn J. H. Heule, Martina Seidl, and Armin Biere. Solution validation and extraction for QBF preprocessing. JAR, 58(1):97-125, 2017. URL: https://doi.org/10.1007/s10817-016-9390-4.
  36. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. TCS, 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  37. Stasys Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
  38. Rafael Kiesel and Thomas Eiter. Knowledge Compilation and More with SharpSAT-TD. In KR'23, pages 406-416, 2023. URL: https://doi.org/10.24963/kr.2023/40.
  39. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn J. H. Heule. Extended resolution simulates DRAT. In IJCAR'18), volume 10900, pages 516-531, jul, 2018. Held as Part of the Federated Logic Conference (FloC'18). URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  40. Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, and Armin Biere. Simulating strong practical proof systems with extended resolution. JAR, 64(7):1247-1267, 2020. URL: https://doi.org/10.1007/s10817-020-09554-z.
  41. Hans Kleine Büning and Theodor Lettman. Propositional logic: deduction and algorithms. Cambridge University Press, New York, NY, USA, 1999. Google Scholar
  42. Tuukka Korhonen and Matti Järvisalo. Integrating tree decompositions into decision heuristics of propositional model counters (short paper). In CP'21, pages 8:1-8:11, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.8.
  43. Jan Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2019. Google Scholar
  44. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DDNF compiler. In IJCAI'17, pages 667-673, Melbourne, VIC, Australia, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  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 - from knowledge compilation to constraint solving. In CP'17, volume 10416, pages 495-511, 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 AI'12, volume 7310, pages 356-361. Springer Verlag, 2012. URL: https://doi.org/10.1007/978-3-642-30353-1_36.
  47. Tobias Philipp and Adrián Rebola-Pardo. DRAT proofs for XOR reasoning. In JELIA'16, pages 415-429, 2016. Google Scholar
  48. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence, 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  49. 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.
  50. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. URL: https://doi.org/10.2178/bsl/1203350879.
  51. Weijia Shi, Andy Shih, Adnan Darwiche, and Arthur Choi. On tractable representations of binary neural networks. In KR'20, pages 882-892, 2020. URL: https://doi.org/10.24963/kr.2020/91.
  52. Marc Thurley. sharpSAT - Counting Models with Advanced Component Caching and Implicit BCP. In SAT'06, pages 424-429, 2006. URL: https://doi.org/10.1007/11814948_38.
  53. Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM J. Comput., 20(5):865-877, 1991. URL: https://doi.org/10.1137/0220053.
  54. G. C. Tseitin. On the complexity of derivations in propositional calculus. In Studies in Mathematics and Mathematical Logic, Part II, pages 115-125. Springer, 1968. Google Scholar
  55. Leslie G. Valiant. The complexity of computing the permanent. TCS, 8(2):189-201, 1979. URL: https://doi.org/10.1016/0304-3975(79)90044-6.
  56. Marc Vinyals. Hard examples for common variable decision heuristics. In AAAI'20, 2020. Google Scholar
  57. Marc Vinyals, Jan Elffers, Jan Johannsen, and Jakob Nordström. Simplified and improved separations between regular and general resolution by lifting. In SAT'20, pages 182-200, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_14.
  58. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. Drat-trim: Efficient checking and trimming using expressive clausal proofs. In SAT'14, volume 8561, pages 422-429, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  59. 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 NSDI'20, pages 575-589, 2020. URL: https://www.usenix.org/conference/nsdi20/presentation/zhai.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact