A Constraint Solver Synthesiser

约束是对影响我们生活的组合问题进行表示和推理的一种自然而强大的方法。例如，在制作大学时间表时，会出现许多限制条件，例如：数学演讲厅可容纳100名学生；艺术史讲座需要有幻灯机的场地；没有学生能同时听两堂课。约束求解提供了一种自动找到这类问题的解决方案的方法。它的简单性和普遍性是其成功应用于各种学科的基础，例如：调度；工业设计;航空;银行;组合数学;石油化工和钢铁行业，仅举几个例子。目前，将约束技术应用于大型复杂问题需要专家进行大量的人工调优。这样的专家很少见。该项目的中心目标是显著提高约束技术的可扩展性，同时消除对专家手动调优的依赖。我们提出了一种新颖、优雅的方法来实现这一点：约束求解器合成器，它生成一个专门针对给定问题的约束求解器。针对单个问题的需求合成约束求解器是约束研究的一个突破性方向，它关注的是通用求解器的增量改进。从零开始合成求解器有两个关键的好处，这两个好处都将产生重大影响。首先，它将实现一般求解器无法实现的细粒度优化，从而允许解决更大、更困难的问题。其次，它将开辟许多令人兴奋的研究可能性。文献中有许多技术，虽然在有限的病例中有效，但不适合普遍使用。因此，它们在当前的一般求解器中被省略，并且相对来说还没有得到发展。然而，合成器将选择适合输入问题的技术，创造新的组合来产生强大的新求解器。结果将是在没有约束专家输入的情况下，可解决的实际问题的数量急剧增加。

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.