A Constraint Solver Synthesiser

EPSRC EP/H004092/1

Constraints are a natural, powerful means of representing and reasoning about combinatorial problems that impact all of our lives. For example, in the production of a university timetable many constraints occur, such as: the maths lecture theatre has a capacity of 100 students; art history lectures require a venue with a slide projector; no student can attend two lectures at once. Constraint solving offers a means by which solutions to such problems can be found automatically. Its simplicity and generality are fundamental to its successful application in a wide variety of disciplines, such as: scheduling; industrial design; aviation; banking; combinatorial mathematics; and the petrochemical and steel industries.

Currently, applying constraint technology to a large, complex problem requires significant manual tuning by an expert. Such experts are rare. The central aim of this project is to improve dramatically the scalability of constraint technology, while simultaneously removing its reliance on manual tuning by an expert. We propose to achieve this by developing a constraint solver synthesiser, which generates a constraint solver specialised to a given problem. Synthesising a solver from scratch has two key benefits. First, it will enable a fine-grained optimisation not possible for a general solver, allowing the solution of much larger, more difficult problems. Second, it will open up many research possibilities: there are many techniques in the literature that, although effective in a limited number of cases, are not suitable for general use. Hence, they are omitted from current general solvers and remain relatively undeveloped. The synthesiser will, however, select such techniques as they are appropriate for an input problem, creating novel combinations to produce powerful new solvers. The result we hope for is a dramatic increase in the number of practical problems solvable without the input of a constraints expert.