Skip to main content

Reasoning on succinctly represented problems and applications

Funding
Funded
Study mode
Full-time
Apply by
Year round
Start date
Year round
Subject area
Computer Science
How to apply
Change country or region

We’re currently showing entry requirements and other information for applicants with qualifications from United Kingdom.

Please select from our list of commonly chosen countries below or choose your own.

If your country or region isn’t listed here, please contact us with any questions about studying with us.

Overview

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.

About this opportunity

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—

Back to top

Who is this for?

Candidates will have, or be due to obtain, a Master’s Degree or equivalent in a relevant subject. Exceptional candidates with a First Class Bachelor’s Degree in an appropriate field or significant relevant experience will also be considered.

Back to top

How to apply

  1. 1. Contact supervisors

    Candidates wishing to apply should complete the University of Liverpool application form to apply for a PhD in Computer Science (CSPR).

    Please review our guide on How to apply for a PhD | Postgraduate research | University of Liverpool carefully and complete the online postgraduate research application form to apply for this PhD project.

    Please ensure you include the project title and reference number CSPR003 when applying.

  2. 2. Prepare your application documents

    You may need the following documents to complete your online application:

    • A research proposal (this should cover the research you’d like to undertake)
    • University transcripts and degree certificates to date
    • Passport details (international applicants only)
    • English language certificates (international applicants only)
    • A personal statement
    • A curriculum vitae (CV)
    • Contact details for two proposed supervisors
    • Names and contact details of two referees.

  3. 3. Apply

    Finally, register and apply online. You'll receive an email acknowledgment once you've submitted your application. We'll be in touch with further details about what happens next.

Back to top

Funding your PhD

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.

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.

Back to top

Contact us

Have a question about this research opportunity or studying a PhD with us? Please get in touch with us, using the contact details below, and we’ll be happy to assist you.

Dr Tony Tan
Back to top