Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs
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.
quantified Boolean formulas
proof complexity
lower bounds
9:1-9:18
Regular Paper
Olaf
Beyersdorff
Olaf Beyersdorff
Joshua
Blinkhorn
Joshua Blinkhorn
Luke
Hinde
Luke Hinde
10.4230/LIPIcs.ITCS.2018.9
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.
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.
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.
Eli Ben-Sasson and Russell Impagliazzo. Random CNFs are hard for the polynomial calculus. Computational Complexity, 19(4):501-519, 2010.
Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001.
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.
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.
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.
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.
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.
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.
Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science, 13, 2017.
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.
Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A characterization of tree-like resolution size. Information Processing Letters, 113(18):666-671, 2013.
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.
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.
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.
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.
Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012.
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.
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.
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.
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.
Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, Cambridge, 2010.
Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979.
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.
Wenceslas Fernandez de la Vega. Random 2-SAT: results and problems. Theoretical Computer Science, 265(1-2):131-146, 2001.
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.
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.
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.
Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random CNFs are hard for cutting planes. Computing Research Repository, abs/1703.02469, 2017.
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.
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.
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.
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.
Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. Electronic Colloquium on Computational Complexity, 24:42, 2017.
Mikolás̆ Janota and João Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015.
Emil Jeřábek. Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005.
Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and Computation, 117(1):12-18, 1995.
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.
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.
Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995.
Sharad Malik and Lintao Zhang. Boolean satisfiability from theoretical hardness to practical success. Communications of the ACM, 52(8):76-82, 2009.
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.
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.
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.
Alexander A. Razborov. Lower bounds for the size of circuits of bounded depth with basis ∧,⊕. Mathematical Notes, 41(4):333-338, 1987.
Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In National Conference on Artificial Intelligence (AAAI), pages 1045-1050. AAAI Press, 2007.
Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007.
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.
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.
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.
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.
Moshe Y. Vardi. Boolean satisfiability: Theory and engineering. Communications of the ACM, 57(3):5, 2014.
Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer, 1999.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode