About the Project
The Boolean Satisfiability (SAT) problem is a cornerstone of computer science, with widespread applications across academia and industry. Leading global companies—including Arm, Cadence, Synopsys, Microsoft, and Amazon—rely on SAT technology to develop their core products and services. However, traditional SAT solvers are reaching their limits when faced with highly demanding, complex tasks. This project aims to extend SAT techniques to address advanced applications that inherently exceed the…
capabilities of standard SAT frameworks.
The Boolean Satisfiability (SAT) problem is a cornerstone of computer science. Although it is known to be theoretically intractable, the past few decades have seen remarkable progress in SAT solver development. This has led to transformative applications across computing technology, where SAT solvers now serve as the core engine for numerous automated reasoning tasks. However, these solvers are not effective for many emerging applications whose inherent complexity far exceeds that of SAT.
To illustrate this, consider the graph 3-colouring problem. The input is an undirected graph (provided as an adjacency matrix), and the goal is to determine whether the vertices can be coloured using three colours such that no adjacent vertices share the same colour. While this problem is NP-complete and easily handled by modern SAT solvers, it becomes NEXP-complete when the graph is represented succinctly—making it exponentially more complex. Encoding a succinct graph as a standard SAT instance incurs an exponential blow-up in size, rendering even the most advanced SAT solvers completely ineffective.
The goal of this project is to study and extend classical SAT techniques to succinctly represented problems. Specifically, we aim to identify which techniques can be successfully adapted to succinct problems and which ones cannot. Because succinctly represented problems occur naturally in high-impact domains—such as Electronic Design Automation (EDA), automated symbolic reasoning, and hardware/software verification—this project will also actively explore and evaluate these practical applications.
While UKRI funding will not cover international fees, a limited number of scholarships to meet the fee difference will be available to support outstanding international students. We want all of our Staff and Students to feel that Liverpool is an inclusive and welcoming environment that actively celebrates and encourages diversity. We are committed to working with students to make all reasonable project adaptations including supporting those with caring responsibilities, disabilities or other personal circumstances.
For example, If you have a disability you may be entitled to a Disabled Students Allowance on top of your studentship to help cover the costs of any additional support that a person studying for a doctorate might need as a result. We believe everyone deserves an excellent education and encourage students from all backgrounds and personal circumstances to apply.
Funding Notes
This is 100% faculty-funded studentship at home rate through cost centre ECG10008. This fund is available due to the success of the EPSRC NIA grant. This UKRI funded Studentship will cover full tuition fees (for 2025-26 this is £5,006 pa.) and pay a maintenance grant for 3.5 years, at the UKRI standard rates (for 2025-26 this is £20,780 pa.) The Studentship also comes with access to additional funding in the form of a Research Training Support Grant to fund consumables, conference attendance, etc. UKRI Studentships are available to any prospective student wishing to apply including both home and international students.