Chew, Leroy Nicholas (2017) QBF Proof Complexity. PhD thesis, University of Leeds.
Abstract
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.
Metadata
Supervisors: | Beyersdorff, Olaf and Vuskovic, Kristina |
---|---|
Keywords: | QBF Proof Complexity, Circuit Complexity, Lower Bounds DQBF Resolution |
Awarding institution: | University of Leeds |
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 |
Download
Final eThesis - complete (pdf)
Filename: Chew_LN_Computing_PhD_2017.pdf
Licence:
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 2.5 License
Export
Statistics
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.