Pages

Main page

PhD topics

Topics for prospective PhD students

• Scaling up automated debugging based on constraint models. Suppose we have a program and a failing test case. The problem of diagnosing the bug in the program can be thought of as finding a minimal set of lines (or assignments) that must be changed to correct the output for the test case. This problem can be modelled as a constrained optimization problem, and solved with a constraint solver such as Minion. This approach was taken by Wotawa et al in a recent paper. In general, debugging is a hard problem and so it only works for very small programs at the moment. The PhD topic here is to investigate ways of scaling up this approach to automatic debugging so that it works on much larger programs, and is therefore more likely to be useful in a real setting.
• Reinforcement learning for selecting SAT encodings. SAT is a very simple constraint language where the variables are all boolean and constraints are all of one type. Encoding to SAT and applying a SAT solver is a popular 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. This project is to apply reinforcement learning to learn good encodings online, using Savile Row's SAT encodings as a basis.