Solving linear and non-linear constraints using logic-based methods
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.