Postgrad LIVE! Study Fairs


University of Leeds Featured PhD Programmes
Imperial College London Featured PhD Programmes
University of Kent Featured PhD Programmes
University of Huddersfield Featured PhD Programmes
University of Nottingham Featured PhD Programmes

Reinforcement learning for SAT encodings of constraint models (EPSRC DTA)

  • Full or part time
  • Application Deadline
    Monday, February 25, 2019
  • Competition Funded PhD Project (European/UK Students Only)
    Competition Funded PhD Project (European/UK Students Only)

Project Description

Constraint satisfaction and optimisation problems are an important class of problems in artificial intelligence, where a set of decisions need to be made together, so that some requirements are satisfied and perhaps also optimizing something. There are many examples in industry such as vehicle routing and scheduling. I am interested in automated modelling and solving of discrete optimization and constraint satisfaction problems. The ultimate goal is for the user to be able to
state the problem without considering how it will be solved, and for the modelling and solving tools to produce a solution efficiently. To do this, the tools have to make choices of formulation and solving strategy automatically, and this is itself an artificial intelligence problem.

SAT is a very simple constraint language where the variables are all boolean. Encoding to SAT and applying a SAT solver is a very effective way of solving various optimization and constraint satisfaction problems. Modern SAT solvers are extremely efficient, so encoding to SAT is the state-of-the-art method for some types of problems. However, there are often many sensible ways of encoding a given constraint and it is difficult to choose among them. Reinforcement learning systems are able to learn from experience. Over time, by making choices and observing the outcome, they can learn to make better choices. This project is to investigate reinforcement learning techniques applied to learning good choices of SAT encodings. Since the main focus of the project is selecting encodings, an existing SAT encoding tool can be used as a starting point (such as Savile Row for example -

Interested applicants are encouraged to contact the project supervisor Dr Peter Nightingale at for further information.

Funding Notes

Applicants must meet the entrance requirements for a PhD in Computer Science, be eligible to pay home/EU fees and meet EPSRC funding eligibility requirements.

Successful candidates will be supported for three years. Funding includes:
£14,777 (2018/19 rate) per year stipend,
Home/EU tuition fees.


To be considered for this competitive funding:
1. Apply online for a full-time PhD in Computer Science (select the October 2019 start date).
2. Quote the project title (Reinforcement learning for SAT encodings of constraint models) in your application.
3. Provide a personal statement of 500-1,000 words with your initial thoughts on the research topic. A formal research proposal is not required.

Related Subjects

How good is research at University of York in Computer Science and Informatics?

FTE Category A staff submitted: 34.80

Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities

Email Now

Insert previous message below for editing? 
You haven’t included a message. Providing a specific message means universities will take your enquiry more seriously and helps them provide the information you need.
Why not add a message here
* required field
Send a copy to me for my own records.

Your enquiry has been emailed successfully

FindAPhD. Copyright 2005-2019
All rights reserved.