Document Open Access Logo

Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness

Author Hubie Chen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2016.94.pdf
  • Filesize: 443 kB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • proof complexity
  • polynomial hierarchy
  • quantified propositional logic

Metrics

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

Abstract

We present and study a framework in which one can present alternation-based lower bounds on proof length in proof systems for quantified Boolean formulas. A key notion in this framework is that of proof system ensemble, which is (essentially) a sequence of proof systems where, for each, proof checking can be performed in the polynomial hierarchy. We introduce a proof system ensemble called relaxing QU-res which is based on the established proof system QU-resolution.

Our main results include an exponential separation of the tree-like and general versions of relaxing QU-res, and an exponential lower bound for relaxing QU-res; these are analogs of classical results in propositional proof complexity.

Cite As Get BibTex

Hubie Chen. Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 94:1-94:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.94

Author Details

Hubie Chen

References

  1. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR), 40:353-373, 2011. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Resolution proofs and skolem functions in QBF evaluation and applications. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, pages 149-164, 2011. Google Scholar
  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 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pages 154-169, 2014. Google Scholar
  4. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR), 22:319-351, 2004. Google Scholar
  5. Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present and future. Bulletin of the EATCS, 65:66-89, 1998. Google Scholar
  6. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Combinatorica, 24(4):585-603, 2004. Google Scholar
  7. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  8. Marco Benedetti. skizzo: A suite to evaluate and certify QBFs. In Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pages 369-376, 2005. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, and Mikolas Janota. On unification of QBF resolution-based calculi. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, pages 81-93, 2014. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof complexity of resolution-based QBF calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, pages 76-89, 2015. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like q-resolution size. Electronic Colloquium on Computational Complexity (ECCC), 2014. Google Scholar
  12. 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. Google Scholar
  13. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and Computation, 117(1):12-18, 1995. Google Scholar
  14. Hubie Chen. Beyond q-resolution and prenex form: A proof system for quantified constraint satisfaction. CoRR, abs/1403.0222, 2014. Google Scholar
  15. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. CoRR, abs/1410.5369, 2014. Google Scholar
  16. Stephen A. Cook and Robert A. Reckhow. On the lengths of proofs in the propositional calculus (preliminary version). In Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1974, Seattle, Washington, USA, pages 135-148, 1974. Google Scholar
  17. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, pages 291-308, 2013. Google Scholar
  18. Allen Van Gelder. Contributions to the theory of practical quantified boolean formula solving. In Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, pages 647-663, 2012. Google Scholar
  19. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 546-553, 2011. Google Scholar
  20. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  21. Marijn Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pages 91-106, 2014. Google Scholar
  22. Mikolás Janota, Radu Grigore, and João Marques-Silva. On QBF proofs and preprocessing. In Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, pages 473-489, 2013. Google Scholar
  23. Mikolás Janota and Joao Marques-Silva. On propositional QBF expansions and Q-resolution. In SAT, pages 67-82, 2013. Google Scholar
  24. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-sat (preliminary version). In Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9-11, 2000, San Francisco, CA, USA., pages 128-136, 2000. Google Scholar
  25. Horst Samulowitz and Fahiem Bacchus. Using SAT in QBF. In Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, pages 578-592, 2005. Google Scholar
  26. N. Segerlind. The complexity of propositional proofs. Bull. Symbolic Logic, 13:417-626, 2007. Google Scholar
  27. Yinlei Yu and Sharad Malik. Validating the result of a quantified boolean formula (QBF) solver: theory and practice. In Proceedings of the 2005 Conference on Asia South Pacific Design Automation, ASP-DAC 2005, Shanghai, China, January 18-21, 2005, pages 1047-1051, 2005. Google Scholar
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