Document Open Access Logo

Reasons for Hardness in QBF Proof Systems

Authors Olaf Beyersdorff, Luke Hinde, Ján Pich

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.14.pdf
  • Filesize: 497 kB
  • 15 pages

Document Identifiers

Author Details

Olaf Beyersdorff
Luke Hinde
Ján Pich

Cite As Get BibTex

Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for Hardness in QBF Proof Systems. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.14

Abstract

We aim to understand inherent reasons for lower bounds for QBF proof systems, and revisit and compare two previous approaches in this direction. 

The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we show a refined version of strategy extraction and thereby for any QBF proof system obtain a trichotomy for  hardness: (1) via circuit lower bounds, (2) via propositional Resolution lower bounds, or (3) `genuine' QBF lower bounds.

The second approach tries to explain QBF lower bounds through quantifier alternations in a system called relaxing QU-Res (Chen, ICALP'16). We prove a strong lower bound for relaxing QU-Res, which also exhibits significant shortcomings of that model.  Prompted by this we propose an alternative, improved version, allowing more flexible oracle queries in proofs. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.

Subject Classification

Keywords
  • proof complexity
  • quantified Boolean formulas
  • resolution
  • lower bounds

Metrics

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

References

  1. 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: http://dx.doi.org/10.1007/978-3-319-09284-3_12.
  2. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In 37th Annual Symposium on Foundations of Computer Science, FOCS '96, Burlington, Vermont, USA, 14-16 October, 1996, pages 274-282. IEEE Computer Society, 1996. URL: http://dx.doi.org/10.1109/SFCS.1996.548486.
  3. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. JSAT, 5(1-4):133-191, 2008. Google Scholar
  4. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Madhu Sudan, editor, Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, Cambridge, MA, USA, January 14-16, 2016, pages 249-260. ACM, 2016. URL: http://dx.doi.org/10.1145/2840728.2840740.
  5. Olaf Beyersdorff, Leroy Chew, and Mikolas Janota. On unification of QBF resolution-based calculi. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, volume 8635 of Lecture Notes in Computer Science, pages 81-93. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44465-8_8.
  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 fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2015.76.
  7. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I, volume 9134 of Lecture Notes in Computer Science, pages 180-192. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47672-7_15.
  8. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for qbfs. In Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen, editors, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, 2016, Chennai, India, volume 65 of LIPIcs, pages 40:1-40:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.40.
  9. Olaf Beyersdorff and Ján Pich. Understanding gentzen and frege systems for QBF. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 146-155. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2933597.
  10. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput., 30(5):1462-1484, 2000. URL: http://dx.doi.org/10.1137/S0097539799352474.
  11. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. URL: http://dx.doi.org/10.1016/j.apal.2011.09.009.
  12. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 94:1-94:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.94.
  13. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  14. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: http://dx.doi.org/10.2307/2273702.
  15. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. In Gonzalo A. Aranda-Corral, Jacques Calmet, and Francisco J. Martín-Mateos, editors, Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Seville, Spain, December 11-13, 2014. Proceedings, volume 8884 of Lecture Notes in Computer Science, pages 120-131. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-13770-4_11.
  16. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. URL: http://dx.doi.org/10.1007/BF01744431.
  17. 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: http://dx.doi.org/10.1007/978-3-642-33558-7_47.
  18. Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 761-780. IOS Press, 2009. URL: http://dx.doi.org/10.3233/978-1-58603-929-5-761.
  19. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: http://dx.doi.org/10.1016/0304-3975(85)90144-6.
  20. Johan Håstad. Almost optimal lower bounds for small depth circuits. In S. Micali, editor, Randomness and Computation, Advances in Computing Reasearch, Vol 5, pages 143-170. JAI Press, 1989. Google Scholar
  21. Mikolás Janota, William Klieber, Joao Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. Artif. Intell., 234:1-25, 2016. URL: http://dx.doi.org/10.1016/j.artint.2016.01.004.
  22. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus q-resolution. Theor. Comput. Sci., 577:25-42, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.01.048.
  23. Emil Jerábek. Dual weak pigeonhole principle, boolean complexity, and derandomization. Ann. Pure Appl. Logic, 129(1-3):1-37, 2004. URL: http://dx.doi.org/10.1016/j.apal.2003.12.003.
  24. Hans Kleine B"uning, Marek Karpinski, and Andreas Flögel. Resolution for quantified boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1025.
  25. Jan Krajícek, Pavel Pudlák, and Alan R. Woods. An exponenetioal lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Struct. Algorithms, 7(1):15-40, 1995. URL: http://dx.doi.org/10.1002/rsa.3240070103.
  26. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995. Google Scholar
  27. Florian Lonsing and Uwe Egly. Evaluating QBF solvers: Quantifier alternations matter. CoRR, abs/1701.06612, 2017. Google Scholar
  28. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-resolution with generalized axioms. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 435-452. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40970-2_27.
  29. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long distance q-resolution with dependency schemes. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 500-518. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40970-2_31.
  30. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential lower bounds for the pigeonhole principle. Computational Complexity, 3:97-140, 1993. URL: http://dx.doi.org/10.1007/BF01200117.
  31. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, pages 1045-1050, 2007. Google Scholar
  32. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. Google Scholar
  33. Horst Samulowitz and Fahiem Bacchus. Using SAT in QBF. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer Science, pages 578-592. Springer, 2005. URL: http://dx.doi.org/10.1007/11564751_43.
  34. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  35. Friedrich Slivovsky and Stefan Szeider. Soundness of q-resolution with dependency schemes. Theor. Comput. Sci., 612:83-101, 2016. URL: http://dx.doi.org/10.1016/j.tcs.2015.10.020.
  36. 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: http://dx.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 About DROPS Imprint Privacy Contact