Refinement-driven Transformation for Effective Automated Constraint Modelling

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

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.