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

Reasons for Hardness in QBF Proof Complexity

Hinde, Luke Peter Edward (2019) Reasons for Hardness in QBF Proof Complexity. PhD thesis, University of Leeds.

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

Download (904Kb) | Preview


Quantified Boolean Formulas (QBF) extend the canonical NP-complete satisfiability problem by including Boolean quantifiers. Determining the truth of a QBF is PSPACE-complete; this is expected to be a harder problem than satisfiability, and hence QBF solving has much wider applications in practice. QBF proof complexity forms the theoretical basis for understanding QBF solving, as well as providing insights into more general complexity theory, but is less well understood than propositional proof complexity. We begin this thesis by looking at the reasons underlying QBF hardness, and in particular when the hardness is propositional in nature, rather than arising due to the quantifiers. We introduce relaxing QU-Res, a previous model for identifying such propositional hardness, and construct an example where relaxing QU-Res is unsuccessful in this regard. We then provide a new model for identifying such hardness which we prove captures this concept. Now equipped with a means of identifying ‘genuine’ QBF hardness, we prove a new lower bound technique for tree-like QBF proof systems. Lower bounds using this technique allows us to show a new separation between tree-like and dag-like systems. We give a characterisation of lower bounds for a large class of tree-like proof systems, in which such lower bounds play a prominent role. Further to the tree-like bound, we provide a new lower bound technique for QBF proof systems in general. This technique has some similarities to the above technique for tree-like systems, but requires some refinement to provide bounds for dag-like systems. We give applications of this new technique by proving lower bounds across several systems. The first such lower bounds are for a very simple family of QBFs. We then provide a construction to combine false QBFs to give formulas for which we can show lower bounds in this way, allowing the generation of the first random QBF proof complexity lower bounds.

Item Type: Thesis (PhD)
Keywords: QBF proof complexity
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.800472
Depositing User: Luke Peter Edward Hinde
Date Deposited: 02 Mar 2020 10:30
Last Modified: 11 Apr 2020 09:53
URI: http://etheses.whiterose.ac.uk/id/eprint/25982

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)