Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR17-044 | 9th May 2017 13:13

Reasons for Hardness in QBF Proof Systems

RSS-Feed




Revision #1
Authors: Olaf Beyersdorff, Luke Hinde, Ján Pich
Accepted on: 9th May 2017 13:13
Downloads: 35
Keywords: 


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 at the same time exhibits significant shortcomings of that model. Prompted by this we propose an alternative, improved version, allowing fewer but more flexible oracle queries in proofs. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.



Changes to previous version:

We strengthen the definition of $\Sigma_k^p$-QU-Res; we remove the restrictions on oracle queries present in the previous version.


Paper:

TR17-044 | 21st February 2017 18:55

Reasons for Hardness in QBF Proof Systems





TR17-044
Authors: Olaf Beyersdorff, Luke Hinde, Ján Pich
Publication: 6th March 2017 16:27
Downloads: 110
Keywords: 


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 at the same time exhibits significant shortcomings of that model. Prompted by this we propose an alternative, improved version, allowing fewer but more flexible oracle queries in proofs. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.



ISSN 1433-8092 | Imprint