Lower bound techniques for QBF proof systems. (English) Zbl 07228393

Niedermeier, Rolf (ed.) et al., 35th symposium on theoretical aspects of computer science, STACS 2018, Caen, France, February 28 – March 3, 2018. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 96, Article 2, 8 p. (2018).
Summary: How do we prove that a false QBF is inded false? How big a proof is needed? The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended – in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent genuine QBF lower bounds based on a semantic cost measure.
This talk will provide a broad overview of some of these developments.
For the entire collection see [Zbl 1381.68010].


03F20 Complexity of proofs
03B35 Mechanization of proofs and logical operations
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)


CAQE; QuBE++; QUBE; Quaffle
Full Text: DOI


[1] Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. {\it J.} {\it Comput. Syst. Sci.}, 74(3):323-334, 2008. URL: https://doi.org/10.1016/j.jcss.2007. 06.025, doi:10.1016/j.jcss.2007.06.025.
[2] :7
[3] Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. {\it Formal Methods in System Design}, 41(1):45-65, 2012.
[4] :8
[5] Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In {\it Proceeding of the 17th International Conference on Theory and} {\it Applications of Satisfiability Testing (SAT)}, pages 154-169, 2014.
[6] Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. {\it Journal of the ACM}, 48(2):149-169, 2001.
[7] Olaf Beyersdorff and Joshua Blinkhorn. Genuine lower bounds for QBF expansion. In {\it Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS)}, page to appear, 2018.
[8] Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. In {\it Proceedings of the ACM Conference on Innovations} {\it in Theoretical Computer Science (ITCS)}, page to appear, 2018.
[9] Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In {\it Proceedings of the ACM Conference on Innovations in Theoretical Com-} {\it puter Science (ITCS)}, pages 249-260. ACM, 2016.
[10] Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In {\it Proceedings of 39th International Symposium on Mathematical Foundations of} {\it Computer Science MFCS, Proceedings Part II, LNCS 8635}, pages 81-93, 2014.
[11] Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. Proof complexity of resolution-based QBF calculi. In {\it Proceedings of the 32nd International Symposium on Theoretical Aspects} {\it of Computer Science (STACS)}, pages 76-89. LIPIcs, 2015.
[12] Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not so simple. {\it ACM Transactions on Computational Logic}, 19(1):1:1- 1:26, Dec 2017. (preliminary version in STACS 2016).
[13] Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible Interpolation for QBF Resolution Calculi. {\it Logical Methods in Computer Science}, Volume 13, Issue 2, 2017. (preliminary version in ICALP 2015).
[14] Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. {\it Electronic Colloquium on Computational Complexity (ECCC)}, 24:37, 2017. (preliminary version in FSTTCS 2016).
[15] Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. In {\it 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical} {\it Computer Science (FSTTCS 2016)}, pages 14:1-14:14, 2017.
[16] Olaf Beyersdorff and Ján Pich. Understanding Gentzen and Frege systems for QBF. In {\it Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science,} {\it LICS}, pages 146-155, 2016.
[17] Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate Quantified Boolean Formulae. In {\it Proceedings of the 15th National Conference on Artificial Intelligence} {\it and Tenth Innovative Applications of Artificial Intelligence Conference (AAAI)}, pages 262- 267, 1998.
[18] Marco Cadoli, Marco Schaerf, Andrea Giovanardi, and Massimo Giovanardi. An algorithm to evaluate Quantified Boolean Formulae and its experimental evaluation.{\it Journal of} {\it Automated Reasoning}, 28(2):101-142, 2002.
[19] Leroy Chew. {\it QBF Proof Complexity}. PhD thesis, University of Leeds, UK, 2017.
[20] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. {\it Journal of} {\it the ACM}, 50(5):752-794, 2003.
[21] Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In {\it 19th International Conference}
[22] Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. QuBE++: An efficient QBF solver. In {\it Formal Methods in Computer-Aided Design}, pages 201-213. Springer Berlin Heidelberg, 2004.
[23] Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In {\it Proceeding of the 15th International Con-} {\it ference on Theory and Applications of Satisfiability Testing (SAT)}, pages 114-128, 2012.
[24] Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. {\it Theoretical Computer Science}, 577:25-42, 2015.
[25] Hans Kleine Büning, Marek Karpinski, and Andreas Flögel.Resolution for quantified Boolean formulas. {\it Information and Computation}, 117(1):12-18, 1995.
[26] William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke. A non-prenex, nonclausal QBF solver with game-state learning. In {\it 13th International Conference on Theory} {\it and Applications of Satisfiability Testing (SAT)}, pages 128-142, 2010.
[27] Jan Krajíček. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. {\it The Journal of Symbolic Logic}, 62(2):457-486, 1997.
[28] Pavel Pudlák. Lower bounds for resolution and cutting planes proofs and monotone computations. {\it The Journal of Symbolic Logic}, 62(3):981-998, 1997.
[29] Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In {\it Formal Methods} {\it in Computer-Aided Design, (FMCAD)}, pages 136-143, 2015.
[30] Anil Shukla. {\it On Proof Complexity for Quantified Boolean Formulas}. PhD thesis, The Institute of Mathematical Sciences, HBNI, India, 2017.
[31] György Turán and Farrokh Vatan. Linear decision lists and partitioning algorithms for the construction of neural networks. In {\it Foundations of Computational Mathematics}. Springer, 1997.
[32] Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In {\it Proceedings of the 18th International Conference on Principles and Practice of} {\it Constraint Programming (CP)}, pages 647-663, 2012.
[33] Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In {\it International Conference on Computer Aided Design}, pages 442-449, 2002.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.