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.