White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

QBF Proof Complexity

Chew, Leroy Nicholas (2017) QBF Proof Complexity. PhD thesis, University of Leeds.

Chew_LN_Computing_PhD_2017.pdf - Final eThesis - complete (pdf)
Available under License Creative Commons Attribution-Noncommercial-Share Alike 2.0 UK: England & Wales.

Download (1523Kb) | Preview


Quantified Boolean Formulas (QBF) and their proof complexity are not as well understood as propositional formulas, yet remain an area of interest due to their relation to QBF solving. Proof systems for QBF provide a theoretical underpinning for the performance of these solvers. We define a novel calculus IR-calc, which enables unification of the principal existing resolution-based QBF calculi and applies to the more powerful Dependency QBF (DQBF). We completely reveal the relative power of important QBF resolution systems, settling in particular the relationship between the two different types of resolution-based QBF calculi. The most challenging part of this comparison is to exhibit hard formulas that underlie the exponential separations of the proof systems. In contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. To this end we exhibit a new proof technique for showing lower bounds in QBF proof systems based on strategy extraction. We also find that the classical lower bound techniques of the prover-delayer game and feasible interpolation can be lifted to a QBF setting and provide new lower bounds. We investigate more powerful proof systems such as extended resolution and Frege systems. We define and investigate new QBF proof systems that mix propositional rules with a reduction rule, we find the strategy extraction technique also works and directly lifts lower bounds from circuit complexity. Such a direct transfer from circuit to proof complexity lower bounds has often been postulated, but had not been formally established for propositional proof systems prior to this work. This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC0[p] circuits. In contrast, any non-trivial lower bound for propositional AC0[p]-Frege constitutes a major open problem.

Item Type: Thesis (PhD)
Keywords: QBF Proof Complexity, Circuit Complexity, Lower Bounds DQBF Resolution
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.723199
Depositing User: Mr Leroy Chew
Date Deposited: 26 Sep 2017 11:30
Last Modified: 25 Jul 2018 09:55
URI: http://etheses.whiterose.ac.uk/id/eprint/18281

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)