Refinement-driven Transformation for Effective Automated Constraint Modelling

约束规划在工业界和学术界已经成功地应用于解决各种各样的组合问题。然而，为了将约束编程应用于特定领域，必须将该问题建模为约束规划。由于约束提供了丰富的语言，因此通常有许多可能的模型，其中一些比另一些要有效得多。因此，构建一个有效的模型是一项具有挑战性的任务，只有很少的专家从业人员。这造成了建模瓶颈，阻碍了人们广泛使用约束技术的力量。最近的工作已经开始减少这一瓶颈，通过将建模转换为对抽象规范的模型进行细化，并使细化过程自动化。然而，有效的建模不仅仅涉及精细化。模型转换可以极大地提高性能，例如打破对称性、利用优势以及添加模型中其他人隐含的约束。这一建议解决了正在进行的减少建模瓶颈的努力中的一个主要挑战：自动生成有效的约束程序。这一目标将通过制定转换规则来实现，这些规则利用了我们自己的建模专长的两个方面。首先，某些细化通常会生成可以转换为更有效形式的约束表达式。其次，可以对某些约束表达式或这类表达式的集合进行转换，以便触发以前不适用的有用的细化。我们将把转换规则嵌入到现有的自动建模系统中。这将缩小自动化建模人员和人工专家建模人员之间的差距。因此，开发强大的约束解算器所需的专业知识将进一步减少，使约束技术更接近大多数人。

Constraint programming has been used with great success totackle a wide variety of combinatorial problems in industry andacademia. However, in order to apply constraint programming toa particular domain, the problem must be modelled as aconstraint program. Since constraints provide a rich language, thereare often many possible models, some of which are far more effectivethan others. Therefore, constructing an effective model is a challenging task with very few expert practitioners. This creates a modelling bottleneck, preventing widespread access to the power of constraint technology. Recent work has begun to reduce this bottleneck by casting modelling as the refinement of a model from an abstract specification and automating the refinement process. Effective modelling involves more than just refinement, however. Model transformations, such as breaking symmetries, exploiting dominances, and adding constraints implied by others in the model can greatly increase performance. This proposal addresses a major challenge in the ongoing effort to reduce the modelling bottleneck: to generate effective constraint programs automatically. This goal will be achieved through the formulation of transformation rules that exploit two facets of our own modelling expertise. First, that certain refinements typically produce constraint expressions that can be transformed into a more effective form. Second, that certain constraint expressions, or sets of such expressions, can be transformed in order to trigger a useful refinement that was previously inapplicable. We will embed the transformation rules in the existing automated modelling system, Conjure. This will close the gap between automated and human expert modellers. Hence, the amount of expertise required to exploit powerful constraint solvers will be further diminished, bringing constraint technology closer to the majority.