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

Quantified Boolean Formulas: Proof Complexity and Models of Solving

Blinkhorn, Joshua Lewis (2019) Quantified Boolean Formulas: Proof Complexity and Models of Solving. PhD thesis, University of Leeds.

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

Download (701Kb) | Preview


Quantified Boolean formulas (QBF), which form the canonical PSPACE-complete decision problem, are a decidable fragment of first-order logic. Any problem that can be solved within a polynomial-size space can be encoded succinctly as a QBF, including many concrete problems in computer science from domains such as verification, synthesis and planning. Automated solvers for QBF are now reaching the point of industrial applicability. In this thesis, we focus on dependency awareness, a dedicated solving paradigm for QBF. We show that dependency schemes can be envisaged in terms of dependency quantified Boolean formulas (DQBF), exposing strong connections between these two previously disparate entities. By introducing new lower-bound techniques for QBF proof systems, we study the relative strengths of models of dependency-aware solving, including the proposal of new, stronger models. Proof Complexity: Using the strategy extraction paradigm, we introduce new lower-bound techniques that apply to resolution-based QBF proof systems. In particular, we use the technique to prove exponential lower bounds for a new family of QBFs called the equality formulas. Our technique also affords considerably simpler, more intuitive proofs of some existing QBF proof-size lower bounds. Models of Solving: We apply our lower bound techniques to show new separations for QBF proof systems parametrised by dependency schemes. We also propose new models of dynamic dependency-aware solving and prove that they are exponentially stronger than the existing static models. Finally, we introduce Merge Resolution, a proof system modelling CDCL-style solving for DQBF, which is the first of its kind.

Item Type: Thesis (PhD)
Keywords: proof complexity, QBF, DQBF, dependency schemes, solving
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.804553
Depositing User: Joshua Lewis Blinkhorn
Date Deposited: 30 Apr 2020 15:40
Last Modified: 11 May 2020 09:53
URI: http://etheses.whiterose.ac.uk/id/eprint/26508

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)