Document Open Access Logo

Extending Merge Resolution to a Family of QBF-Proof Systems

Authors Sravanthi Chede , Anil Shukla

PDF
Thumbnail PDF

File

LIPIcs.STACS.2023.21.pdf
  • Filesize: 1.23 MB
  • 20 pages

Document Identifiers

Author Details

Sravanthi Chede
  • Indian Institute of Technology Ropar, Rupnagar, India
Anil Shukla
  • Indian Institute of Technology Ropar, Rupnagar, India

Acknowledgements

We thank the anonymous reviewers who helped us substantially improve the motivation of this paper and also shorten the proofs. We also thank Gaurav Sood and Leroy Chew for important discussions, comments and suggestions regarding this paper.

Cite AsGet BibTex

Sravanthi Chede and Anil Shukla. Extending Merge Resolution to a Family of QBF-Proof Systems. In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.STACS.2023.21

Abstract

Merge Resolution (MRes [Olaf Beyersdorff et al., 2021]) is a recently introduced proof system for false QBFs. Unlike other known QBF proof systems, it builds winning strategies for the universal player (countermodels) within the proofs as merge maps. Merge maps are deterministic branching programs in which isomorphism checking is efficient, as a result MRes is a polynomial time verifiable proof system. In this paper, we introduce a family of proof systems MRes-ℛ in which the information of countermodels are stored in any pre-fixed complete representation ℛ. Hence, corresponding to each possible complete representation ℛ, we have a sound and refutationally complete QBF-proof system in MRes-ℛ. To handle these arbitrary representations, we introduce consistency checking rules in MRes-ℛ instead of the isomorphism checking in MRes. As a result these proof systems are not polynomial time verifiable (Non-P). Consequently, the paper shows that using merge maps is too restrictive and with a slight change in rules, it can be replaced with arbitrary representations leading to several interesting proof systems. We relate these new systems with the implicit proof system from the algorithm in [Joshua Blinkhorn et al., 2021], which was designed to solve DQBFs (Dependency QBFs) using clause-strategy pairs like MRes. We use the OBDD (Ordered Binary Decision Diagrams) representation suggested in [Joshua Blinkhorn et al., 2021] and deduce that "Ordered" versions of the proof systems in MRes-ℛ are indeed polynomial time verifiable. On the lower bound side, we lift the lower bound result of regular MRes ([Olaf Beyersdorff et al., 2020]) by showing that the completion principle formulas (CR_n) from [Mikolás Janota and João Marques-Silva, 2015] which are shown to be hard for regular MRes in [Olaf Beyersdorff et al., 2020], are also hard for any regular proof system in MRes-ℛ. Thereby, the paper lifts the lower bound of regular MRes to an entire class of proof systems, which use various complete representations, including those undiscovered, instead of only merge maps. Thereby proving that the hardness of CR_n formulas is intact even after changing the weak isomorphism checking in MRes to the stronger consistency checking in MRes-ℛ.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • QBFs
  • Merge Resolution
  • Simulation
  • Lower Bound

Metrics

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

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45-65, August 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Theory and Applications of Satisfiability Testing - SAT 2014, volume 8561 of LNCS, pages 154-169. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_12.
  4. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reason., 65(1):125-154, 2021. URL: https://doi.org/10.1007/s10817-020-09560-1.
  5. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, and Gaurav Sood. Hard QBFs for merge resolution. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, volume 182 of LIPIcs, pages 12:1-12:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.12.
  6. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof complexity of resolution-based QBF calculi. In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 76-89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.76.
  7. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. Inf. Comput., 262:141-161, 2018. URL: https://doi.org/10.1016/j.ic.2018.08.002.
  8. Joshua Blinkhorn, Tomás Peitl, and Friedrich Slivovsky. Davis and Putnam meet Henkin: Solving DQBF with resolution. In Theory and Applications of Satisfiability Testing - SAT 2021, volume 12831 of LNCS, pages 30-46. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_4.
  9. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  10. Leroy Chew. Hardness and optimality in QBF proof systems modulo NP. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 98-115. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_8.
  11. Leroy Chew and Friedrich Slivovsky. Towards uniform certification in QBF. In Petra Berenbrink and Benjamin Monmege, editors, 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, March 15-18, 2022, Marseille, France (Virtual Conference), volume 219 of LIPIcs, pages 22:1-22:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.STACS.2022.22.
  12. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  13. Adnan Darwiche and Pierre Marquis. A knowledge compilation map. J. Artif. Intell. Res., 17:229-264, 2002. URL: https://doi.org/10.1613/jair.989.
  14. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  15. Yuval Filmus, Pavel Hrubes, and Massimo Lauria. Semantic versus syntactic cutting planes. In 33rd Symposium on Theoretical Aspects of Computer Science, STACS, volume 47 of LIPIcs, pages 35:1-35:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.35.
  16. Gottlob Frege. Begriffsschrift. In Jean Van Heijenoort, editor, From Frege to Gödel, pages 1-83. Cambridge: Harvard University Press, 1967. translated from Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache der reinen Denkens, Halle 1879. Google Scholar
  17. Mikolás Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  18. Stasys Jukna. Exponential lower bounds for semantic resolution. In Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, volume 39, pages 163-172. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/10.
  19. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and Computation, 117(1):12-18, 1995. URL: https://doi.org/10.1006/inco.1995.1025.
  20. Meena Mahajan and Gaurav Sood. QBF merge resolution is powerful but unnatural. 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 22:1-22:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.22.
  21. G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers & Mathematics with Applications, 41(7):957-992, 2001. URL: https://doi.org/10.1016/S0898-1221(00)00333-3.
  22. John Alan Robinson. Theorem-proving on the computer. J. ACM, 10(2):163-174, 1963. URL: https://doi.org/10.1145/321160.321166.
  23. Nathan Segerlind. The complexity of propositional proofs. Bull. Symb. Log., 13(4):417-481, 2007. URL: https://doi.org/10.2178/bsl/1203350879.
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