Solving and proof complexity of quantified boolean formulas

Project description

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.

Entry requirements

We would normally expect applicants for postgraduate research to have achieved one of the following in a subject relevant to the proposed research:
• a minimum of a UK upper second class honours degree (2.1), or equivalent, or
• a good performance in a Masters level course.
We also recognise relevant industrial and academic experience and special circumstances in the consideration of applicants.

How to apply

Formal applications for research degree study should be made online through the university's website. Follow our step by step guide to apply for a Research Degree.

If you require any further information please contact the Graduate School Office
e: phd@engineering.leeds.ac.uk, t: +44 (0)113 343 8000.