Synthesis of efficient constraint-satisfaction programs
Synthesis of efficient constraint-satisfaction programs
复制标题
有效约束满足程序的综合
DOI：
10.1017/s0269888901000029
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Douglas R. Smith
中科院分区：
文献类型：
--
作者：
S. Westfold;Douglas R. Smith
在本文中，我们描述了框架，我们已经开发的KIDS（Kestrel交互式开发系统）生成高效的约束满足程序。我们已经使用KIDS来合成全局搜索调度程序，这些程序已经被证明比运行相同数据的其他程序快得多。我们专注于导致这种效率的基本思想。的效率的关键是减少搜索空间的大小的一组可能的解决方案（解决方案空间），允许有效的约束传播和修剪的解决方案空间的水平的有效表示。移动到解决方案空间表示涉及问题重构。在找到重新表述的问题的解决方案之后，提取阶段提取原始问题的解决方案。我们展示了如何从原始问题的约束可以自动重新制定和专业化，以自动获得有效的传播代码。我们的解决方案的方法利用我们的解决方案空间的半格结构。
In this paper we describe the framework we have developed in KIDS (Kestrel Interactive Development System) for generating efficient constraint satisfaction programs. We have used KIDS to synthesise global search scheduling programs that have proved to be dramatically faster than other programs running the same data. We focus on the underlying ideas that lead to this efficiency. The key to the efficiency is the reduction of the size of the search space by an effective representation of sets of possible solutions (solution spaces) that allows efficient constraint propagation and pruning at the level of solution spaces. Moving to a solution space representation involves a problem reformulation. Having found a solution to the reformulated problem, an extraction phase extracts solutions to the original problem. We show how constraints from the original problem can be automatically reformulated and specialised in order to derive efficient propagation code automatically. Our solution methods exploit the semi-lattice structure of our solution spaces.