DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.14

Reasons for Hardness in QBF Proof Systems

Authors: Olaf Beyersdorff, Luke Hinde, and Ján Pich

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.FSTTCS.2017.14,
  author =	{Beyersdorff, Olaf and Hinde, Luke and Pich, J\'{a}n},
  title =	{{Reasons for Hardness in QBF Proof Systems}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.14},
  URN =		{urn:nbn:de:0030-drops-83824},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.14},
  annote =	{Keywords: proof complexity, quantified Boolean formulas, resolution, lower bounds}
}

Document

DOI: 10.4230/LIPIcs.ITCS.2018.9

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

Authors: Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.ITCS.2018.9,
  author =	{Beyersdorff, Olaf and Blinkhorn, Joshua and Hinde, Luke},
  title =	{{Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.9},
  URN =		{urn:nbn:de:0030-drops-83228},
  doi =		{10.4230/LIPIcs.ITCS.2018.9},
  annote =	{Keywords: quantified Boolean formulas, proof complexity, lower bounds}
}

Search Results

Documents authored by Hinde, Luke

Reasons for Hardness in QBF Proof Systems

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message