A Constraint Solver Synthesiser

点击翻译按钮获取中文摘要

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, to name but a few examples.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 a novel, elegant means to achieve this: a constraint solver synthesiser, which generates a constraint solver specialised to a given problem. Synthesising a constraint solver tailored to the needs of an individual problem is a groundbreaking direction for constraints research, which has focused on the incremental improvement of general-purpose solvers. Synthesising a solver from scratch has two key benefits, both of which will have a major impact. 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 exciting 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 will be a dramatic increase in the number of practical problems solvable without the input of a constraints expert.