Solving linear and non-linear constraints using logic-based methods

Primary supervisor

Additional information

Contact admissions office

Other projects with the same supervisor


  • Competition Funded Project (European/UK Students Only)
This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. The funding is available to citizens of a number of European countries (including the UK). In most cases this will include all EU nationals. However full funding may not be available to all applicants and you should read the full department and project details for further information.

Project description

Solving systems of linear inequalities and closely related optimisation problems are fundamental mathematical problems with a wide range of applications such verification, constraint solving, planning and scheduling. Recently we have been developing two novel algorithms for solving linear constraints: conflict resolution and bound propagation. These methods were inspired by techniques which made propositional satisfiability scalable to industrial-size problems: unit propagation, backjumping and learning.

There are three major research directions which follow from this research that are available as PhD projects:

1) Extending conflict resolution and bound propagation to solve systems of constraints over the integers. This is important for program verification, where verification conditions usually contain integer constraints.

2) Integrating arithmetical reasoning into first-order theorem provers. This is a long standing challenge, solving it would lead to a breakthrough in the area.

3) Solving non-linear arithmetical constraints.

Requirements: Candidates should have a strong interest in logic/math, willingness to program and experiment with new ideas.

▲ Up to the top