Research course

Solving and proof complexity of quantified Boolean formulas

University of Leeds · School of Computing

Entry requirements

Applicants must have a minimum of a UK upper second class honours degree (2.1), or equivalent, in computer science or artificial intelligence. If English is not your first language, you must provide evidence that you meet the University’s minimum English Language requirements.

Months of entry


Course content

QBF-solvers are powerful tools that efficiently tackle the classically hard problem of solving quantified Boolean formulas (QBF) for important industrial applications, including verification and planning. In this project we aim to advance the understanding of the power and limitations of QBF algorithms. The main theoretical approach for this is through proof complexity, as the complexity of proofs directly corresponds to the complexity of QBF-solvers. QBF proof complexity is a young field with an exciting development in recent years. However, major questions remain open, including designing proof systems for solvers, developing techniques for lower bounds and finding hard formulas.

Keywords: Theoretical Computer Science, Computational Logic, Proof Complexity, QBF solving

Fees and funding

This scholarship is part of Leeds Anniversary Research Scholarship scheme.

This scholarship is fully funded covering fees and a maintenance of £14,254 in 2016/17

Qualification and course duration


full time
48 months

Course contact details

Dr Olaf Beyersdorff