Document Open Access Logo

Circuits, Proofs and Propositional Model Counting

Authors Sravanthi Chede , Leroy Chew , Anil Shukla

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2024.18.pdf
  • Filesize: 0.96 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Propositional model counting
  • Boolean circuits
  • #SAT
  • Proof Systems
  • Certified Partition Operation Graph (CPOG)

Metrics

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

Abstract

In this paper we present a new proof system framework CLIP (Circuit Linear Induction Proposition) for propositional model counting (#SAT). A CLIP proof firstly involves a Boolean circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of the circuit. 
This concept is remarkably simple and CLIP is modular so it allows us to use existing checking formats from propositional logic, especially strong proof systems. CLIP has polynomial-size proofs for XOR-pairs which are known to require exponential-size proofs in MICE [Fichte et al., 2022]. The existence of a strong proof system that can tackle these hard problems was posed as an open problem in Beyersdorff et al. [Olaf Beyersdorff et al., 2023]. In addition, CLIP systems can p-simulate all other existing #SAT proofs systems (KCPS(#SAT) [Florent Capelli, 2019], CPOG [Bryant et al., 2023], MICE). Furthermore, CLIP has a theoretical advantage over the other #SAT proof systems in the sense that CLIP only has lower bounds from its propositional proof system or if 𝖯^#𝖯 is not contained in P/poly, which is a major open problem in circuit complexity. 
CLIP uses unrestricted circuits in its proof as compared to restricted structures used by the existing #SAT proof systems. In this way, CLIP avoids hardness or limitations due to circuit restrictions.

Cite As Get BibTex

Sravanthi Chede, Leroy Chew, and Anil Shukla. Circuits, Proofs and Propositional Model Counting. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSTTCS.2024.18

Author Details

Sravanthi Chede
  • Indian Institute of Technology Ropar, Rupnagar, India
Leroy Chew
  • TU Wien, Austria
Anil Shukla
  • Indian Institute of Technology Ropar, Rupnagar, India

Funding

  • Chew, Leroy: This work was supported by FWF ESPRIT grant no. ESP 197.

Acknowledgements

We thank Olaf Beyersdorff, Tim Hoffmann, Luc Nicolas Spachmann for useful discussions on this topic. We also thank the anonymous reviewers for helpful suggestions on the paper.

References

  1. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Ján Pich. Frege systems for quantified boolean logic. J. ACM, 67(2):9:1-9:36, 2020. URL: https://doi.org/10.1145/3381881.
  2. Olaf Beyersdorff, Johannes Klaus 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, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 5:1-5:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.SAT.2024.5.
  3. Olaf Beyersdorff, Tim Hoffmann, and Luc Nicolas Spachmann. Proof complexity of propositional model counting. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 2:1-2:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.2.
  4. 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), 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.6.
  5. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn J. H. Heule. Supplement to certified knowledge compilation with application to verified model counting, 2023. URL: https://zenodo.org/records/7966174.
  6. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Log. Methods Comput. Sci., 17(2), 2021. URL: https://lmcs.episciences.org/7400.
  7. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Log., 163(7):906-917, 2012. URL: https://doi.org/10.1016/J.APAL.2011.09.009.
  8. Florent Capelli. Knowledge compilation languages as proof systems. In Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 90-99. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_6.
  9. Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, and Stefan Szeider. Hardness of random reordered encodings of parity for resolution and CDCL. In Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, pages 7978-7986. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28635.
  10. Leroy Chew and Marijn J. H. Heule. Sorting parity encodings by reusing variables. In Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 1-10. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_1.
  11. Stephen A Cook. A short proof of the pigeon hole principle using extended resolution. Acm Sigact News, 8(4):28-32, 1976. URL: https://doi.org/10.1145/1008335.1008338.
  12. Stephen A Cook and Robert A Reckhow. The relative efficiency of propositional proof systems. In Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook, pages 173-192. ACM, 2023. URL: https://doi.org/10.1145/3588287.3588299.
  13. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discret. Appl. Math., 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  14. Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608-647, 2001. URL: https://doi.org/10.1145/502090.502091.
  15. Peter M. Fenwick. A new data structure for cumulative frequency tables. Softw. Pract. Exp., 24(3):327-336, 1994. URL: https://doi.org/10.1002/SPE.4380240306.
  16. 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), 2022. URL: https://doi.org/10.4230/LIPICS.SAT.2022.30.
  17. Gottlob Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache der reinen Denkens, Halle. Lubrecht & Cramer, 1879. English translation in: from Frege to Gödel, a source book in mathematical logic (J. van Heijenoord editor), Harvard University Press, Cambridge 1967. Google Scholar
  18. Joshua A. Grochow and Toniann Pitassi. Circuit complexity, proof complexity, and polynomial identity testing: The ideal proof system. J. ACM, 65(6), November 2018. URL: https://doi.org/10.1145/3230742.
  19. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  20. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, New York, NY, USA, 1995. Google Scholar
  21. Benjamin Kiesl, Adrián Rebola-Pardo, and Marijn JH Heule. Extended resolution simulates DRAT. In Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, pages 516-531. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_34.
  22. Jan Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log., 62(2):457-486, 1997. URL: https://doi.org/10.2307/2275541.
  23. Meena Mahajan and Gaurav Sood. QBF merge resolution is powerful but unnatural. In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 22:1-22:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.SAT.2022.22.
  24. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  25. John Alan Robinson. Theorem-proving on the computer. Journal of the ACM, 10(2):163-174, 1963. URL: https://doi.org/10.1145/321160.321166.
  26. Boris Ryabko. A fast on-line adaptive code. IEEE Trans. Inf. Theory, 38(4):1400-1404, 1992. URL: https://doi.org/10.1109/18.144725.
  27. 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.
  28. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In SAT 2014, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
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