Document Open Access Logo

Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs

Authors Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2018.9.pdf
  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Author Details

Olaf Beyersdorff
Joshua Blinkhorn
Luke Hinde

Cite AsGet BibTex

Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ITCS.2018.9

Abstract

As a natural extension of the SAT problem, an array of proof systems for quantified Boolean formulas (QBF) have been proposed, many of which extend a propositional proof system to handle universal quantification. By formalising the construction of the QBF proof system obtained from a propositional proof system by adding universal reduction (Beyersdorff, Bonacina & Chew, ITCS'16), we present a new technique for proving proof-size lower bounds in these systems. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. By examining the capacity of proofs in several QBF systems, we are able to use the technique to obtain lower bounds based on cost alone. As applications of the technique, we first prove exponential lower bounds for a new family of simple QBFs representing equality. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first 'genuine' lower bounds of this kind, which apply to the QBF analogues of resolution, Cutting Planes, and Polynomial Calculus. Finally, we employ the technique to give a simple proof of hardness for a prominent family of QBFs.
Keywords
  • quantified Boolean formulas
  • proof complexity
  • lower bounds

Metrics

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

References

  1. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. In Symposium on Foundations of Computer Science (FOCS), pages 190-199. IEEE Computer Society, 2001. Google Scholar
  2. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Carsten Sinz and Uwe Egly, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 8561 of Lecture Notes in Computer Science, pages 154-169. Springer, 2014. Google Scholar
  3. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In Symposium on Foundations of Computer Science (FOCS), pages 274-282. IEEE Computer Society, 1996. Google Scholar
  4. Eli Ben-Sasson and Russell Impagliazzo. Random CNFs are hard for the polynomial calculus. Computational Complexity, 19(4):501-519, 2010. Google Scholar
  5. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Google Scholar
  6. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 5(1-4):133-191, 2008. Google Scholar
  7. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Electronic Colloquium on Computational Complexity (ECCC), 24:35, 2017. Google Scholar
  8. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Madhu Sudan, editor, ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 249-260. ACM, 2016. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, and Mikolás̆ Janota. On unification of QBF resolution-based calculi. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8635 of Lecture Notes in Computer Science, pages 81-93. Springer, 2014. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, and Mikolás̆ Janota. Proof complexity of resolution-based QBF calculi. In Ernst W. Mayr and Nicolas Ollinger, editors, International Symposium on Theoretical Aspects of Computer Science (STACS), volume 30 of Leibniz International Proceedings in Informatics (LIPIcs), pages 76-89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not simple. In Symposium on Theoretical Aspects of Computer Science (STACS), pages 15:1-15:14, 2016. Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science, 13, 2017. Google Scholar
  13. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-resolution size. Journal of Computer and System Sciences, 2017. in press. Google Scholar
  14. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A characterization of tree-like resolution size. Information Processing Letters, 113(18):666-671, 2013. Google Scholar
  15. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. In Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2017. Google Scholar
  16. Olaf Beyersdorff and Ján Pich. Understanding Gentzen and Frege systems for QBF. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Symposium on Logic in Computer Science (LICS), pages 146-155. ACM, 2016. Google Scholar
  17. Roderick Bloem, Robert Könighofer, and Martina Seidl. SAT-based synthesis methods for safety specs. In Kenneth L. McMillan and Xavier Rival, editors, International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 8318 of Lecture Notes in Computer Science, pages 1-20. Springer, 2014. Google Scholar
  18. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, International Conference on Theory and Practice of Satisfiability Testing (SAT), volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. Google Scholar
  19. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  20. Michael Cashmore, Maria Fox, and Enrico Giunchiglia. Partially grounded planning as quantified Boolean formula. In Daniel Borrajo, Subbarao Kambhampati, Angelo Oddi, and Simone Fratini, editors, International Conference on Automated Planning and Scheduling (ICAPS). AAAI, 2013. Google Scholar
  21. Hubie Chen. Proof complexity modulo the polynomial hierarchy: Understanding alternation as a source of hardness. ACM Transactions on Computation Theory, 9(3):15:1-15:20, 2017. Google Scholar
  22. Hubie Chen and Yannet Interian. A model for generating random quantified Boolean formulas. In Leslie Pack Kaelbling and Alessandro Saffiotti, editors, International Joint Conference on Artificial Intelligence (IJCAI), pages 66-71. Professional Book Center, 2005. Google Scholar
  23. Vasek Chvátal and Bruce A. Reed. Mick gets some (the odds are on his side). In Symposium on Foundations of Computer Science (FOCS), pages 620-627. IEEE Computer Society, 1992. Google Scholar
  24. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge, 2010. Google Scholar
  25. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  26. Nadia Creignou, Hervé Daudé, Uwe Egly, and Raphaël Rossignol. Exact location of the phase transition for random (1, 2)-QSAT. RAIRO - Theoretical Informatics and Applications, 49(1):23-45, 2015. Google Scholar
  27. Wenceslas Fernandez de la Vega. Random 2-SAT: results and problems. Theoretical Computer Science, 265(1-2):131-146, 2001. Google Scholar
  28. Nachum Dershowitz, Ziyad Hanna, and Jacob Katz. Space-efficient bounded model checking. In Fahiem Bacchus and Toby Walsh, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 3569 of Lecture Notes in Computer Science, pages 502-518. Springer, 2005. Google Scholar
  29. Josep Díaz, Lefteris M. Kirousis, Dieter Mitsche, and Xavier Pérez-Giménez. A new upper bound for 3-SAT. In Ramesh Hariharan, Madhavan Mukund, and V. Vinay, editors, Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 2 of LIPIcs, pages 163-174. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2008. Google Scholar
  30. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. Annals of Mathematics and Artificial Intelligence, 80(1):21-45, 2017. Google Scholar
  31. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random CNFs are hard for cutting planes. Computing Research Repository, abs/1703.02469, 2017. Google Scholar
  32. John Franco and Marvin C. Paull. Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem. Discrete Applied Mathematics, 5(1):77-87, 1983. Google Scholar
  33. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Michela Milano, editor, International Conference on Principles and Practice of Constraint Programming (CP), volume 7514 of Lecture Notes in Computer Science, pages 647-663. Springer, 2012. Google Scholar
  34. 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. Google Scholar
  35. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Toby Walsh, editor, International Joint Conference on Artificial Intelligence (IJCAI), pages 546-553. IJCAI/AAAI, 2011. Google Scholar
  36. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. Electronic Colloquium on Computational Complexity, 24:42, 2017. Google Scholar
  37. Mikolás̆ Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015. Google Scholar
  38. Emil Jeřábek. Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005. Google Scholar
  39. 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
  40. Roman Kontchakov, Luca Pulina, Ulrike Sattler, Thomas Schneider, Petra Selmer, Frank Wolter, and Michael Zakharyaschev. Minimal module extraction from DL-lite ontologies using QBF solvers. In Craig Boutilier, editor, International Joint Conference on Artificial Intelligence (IJCAI), pages 836-841. AAAI Press, 2009. Google Scholar
  41. Jan Krají\ucek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  42. 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
  43. Sharad Malik and Lintao Zhang. Boolean satisfiability from theoretical hardness to practical success. Communications of the ACM, 52(8):76-82, 2009. Google Scholar
  44. Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, and Sharad Malik. Constrained sampling and counting: Universal hashing meets SAT solving. In Adnan Darwiche, editor, Beyond NP, volume WS-16-05 of AAAI Workshops. AAAI Press, 2016. Google Scholar
  45. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-SAT (preliminary version). In David B. Shmoys, editor, Symposium on Discrete Algorithms, pages 128-136. ACM/SIAM, 2000. Google Scholar
  46. Luca Pulina. The ninth QBF solvers evaluation - preliminary report. In Florian Lonsing and Martina Seidl, editors, International Workshop on Quantified Boolean Formulas (QBF), volume 1719 of CEUR Workshop Proceedings, pages 1-13. CEUR-WS.org, 2016. Google Scholar
  47. Alexander A. Razborov. Lower bounds for the size of circuits of bounded depth with basis ∧,⊕. Mathematical Notes, 41(4):333-338, 1987. Google Scholar
  48. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In National Conference on Artificial Intelligence (AAAI), pages 1045-1050. AAAI Press, 2007. Google Scholar
  49. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  50. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, International Conference on Computer-Aided Design (ICCAD), pages 220-227. IEEE Computer Society / ACM, 1996. Google Scholar
  51. R. Smolensky. Algebraic methods in the theory of lower bounds for Boolean circuit complexity. In Alfred V. Aho, editor, ACM Symposium on Theory of Computing (STOC), pages 77-82. ACM, 1987. Google Scholar
  52. Stefan Staber and Roderick Bloem. Fault localization and correction with QBF. In João Marques-Silva and Karem A. Sakallah, editors, International Conference on Theory and Applications of Satisfiability Testing (SAT), volume 4501 of Lecture Notes in Computer Science, pages 355-368. Springer, 2007. Google Scholar
  53. 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, ACM Symposium on Theory of Computing (STOC), pages 1-9. ACM, 1973. Google Scholar
  54. Moshe Y. Vardi. Boolean satisfiability: Theory and engineering. Communications of the ACM, 57(3):5, 2014. Google Scholar
  55. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer, 1999. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact