Document Open Access Logo

QBF Merge Resolution Is Powerful but Unnatural

Authors Meena Mahajan , Gaurav Sood

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.22.pdf
  • Filesize: 0.76 MB
  • 19 pages

Document Identifiers

Author Details

Meena Mahajan
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India
Gaurav Sood
  • The Institute of Mathematical Sciences, Chennai, India
  • Homi Bhabha National Institute, Training School Complex, Anushaktinagar, Mumbai, India

Acknowledgements

We thank Olaf Beyersdorff, Joshua Blinkhorn and Tomáš Peitl for interesting discussions about the power of M-Res. Part of this work was done at Schloss Dagstuhl Leibniz Centre for Informatics (seminar 20061).

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.22

Abstract

The Merge Resolution proof system (M-Res) for QBFs, proposed by Beyersdorff et al. in 2019, explicitly builds partial strategies inside refutations. The original motivation for this approach was to overcome the limitations encountered in long-distance Q-Resolution proof system (LD-Q-Res), where the syntactic side-conditions, while prohibiting all unsound resolutions, also end up prohibiting some sound resolutions. However, while the advantage of M-Res over many other resolution-based QBF proof systems was already demonstrated, a comparison with LD-Q-Res itself had remained open. In this paper, we settle this question. We show that M-Res has an exponential advantage over not only LD-Q-Res, but even over LQU^+-Res and IRM, the most powerful among currently known resolution-based QBF proof systems. Combining this with results from Beyersdorff et al. 2020, we conclude that M-Res is incomparable with LQU-Res and LQU^+-Res. Our proof method reveals two additional and curious features about MRes: (i) M-Res is not closed under restrictions, and is hence not a natural proof system, and (ii) weakening axiom clauses with existential variables provably yields an exponential advantage over MRes without weakening. We further show that in the context of regular derivations, weakening axiom clauses with universal variables provably yields an exponential advantage over M-Res without weakening. These results suggest that M-Res is better used with weakening, though whether M-Res with weakening is closed under restrictions remains open. We note that even with weakening, M-Res continues to be simulated by eFrege+∀red (the simulation of ordinary M-Res was shown recently by Chew and Slivovsky).

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • proof complexity
  • resolution
  • weakening
  • restrictions

Metrics

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

References

  1. Albert Atserias. On sufficient conditions for unsatisfiability of random formulas. J. ACM, 51(2):281-311, 2004. URL: https://doi.org/10.1145/972639.972645.
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods Syst. Des., 41(1):45-65, 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 Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 154-169. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_12.
  4. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res., 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  5. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reason., 65(1):125-154, 2021. Preliminary version in the proceedings of the 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). URL: https://doi.org/10.1007/s10817-020-09560-1.
  7. Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, and Gaurav Sood. Hard QBFs for merge resolution. In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, December 14-18, 2020, BITS Pilani, K K Birla Goa Campus, Goa, India (Virtual Conference), 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.
  8. 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.
  9. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory, 11(4):26:1-26:42, 2019. URL: https://doi.org/10.1145/3352155.
  10. 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.
  11. Archie Blake. Canonical expressions in Boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  12. Joshua Blinkhorn, Tomás Peitl, and Friedrich Slivovsky. Davis and Putnam meet Henkin: Solving DQBF with resolution. 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 30-46. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_4.
  13. 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, pages 233-350. IOS Press, Netherlands, 2nd edition, May 2021. URL: https://doi.org/10.3233/FAIA200990.
  14. 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.
  15. 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.
  16. Leroy Nicholas Chew. QBF proof complexity. PhD thesis, University of Leeds, 2017. URL: https://etheses.whiterose.ac.uk/18281/.
  17. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. URL: https://doi.org/10.1145/368273.368557.
  18. 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.
  19. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, volume 8312 of Lecture Notes in Computer Science, pages 291-308. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_21.
  20. Allen Van Gelder. Contributions to the theory of practical quantified boolean formula solving. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 647-663. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_47.
  21. Marijn J. H. Heule and Oliver Kullmann. The science of brute force. Commun. ACM, 60(8):70-79, 2017. URL: https://doi.org/10.1145/3107239.
  22. 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.
  23. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: https://doi.org/10.1006/inco.1995.1025.
  24. Joao Marques-Silva, Ines 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, pages 133-182. IOS Press, Netherlands, 2nd edition, May 2021. URL: https://doi.org/10.3233/FAIA200987.
  25. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  26. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. URL: https://doi.org/10.1145/321250.321253.
  27. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, Portland, OR, USA, November 4-6, 2019, pages 78-84. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00020.
  28. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  29. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report. In Alfred V. Aho, Allan Borodin, Robert L. Constable, Robert W. Floyd, Michael A. Harrison, Richard M. Karp, and H. Raymond Strong, editors, Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin, Texas, USA, pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  30. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  31. Moshe Y. Vardi. Boolean satisfiability: theory and engineering. Commun. ACM, 57(3):5, 2014. URL: https://doi.org/10.1145/2578043.
  32. Ingo Wegener. Branching Programs and Binary Decision Diagrams. Society for Industrial and Applied Mathematics, 2000. URL: https://doi.org/10.1137/1.9780898719789.
  33. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In Lawrence T. Pileggi and Andreas Kuehlmann, editors, Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, San Jose, California, USA, November 10-14, 2002, pages 442-449. ACM / IEEE Computer Society, 2002. URL: https://doi.org/10.1145/774572.774637.
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