Solving and proof complexity of quantified boolean formulas
- Self-funded PhD students only
- Number of awards: 1
- Deadline: Ongoing.
- Supervisors: Contact Dr Olaf Beyersdorff to discuss this project further informally.
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.
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
If you require any further information please contact the Graduate School Office
e: firstname.lastname@example.org, t: +44 (0)113 343 8000.