Generating Propagators for Finite Set Constraints
Generating Propagators for Finite Set Constraints
复制标题
生成有限集约束的传播器
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
G. Smolka
中科院分区：
文献类型：
--
作者：
Guido Tack;Christian Schulte;G. Smolka
理想情况下，将传播器编程为约束的实现应该是针对一大类约束的完全声明性规范过程：高级声明性规范会自动转换为高效的传播器。本文介绍了使用存在一元二阶逻辑作为有限集传播器的声明性规范语言。论文中采用的方法是自动导出投影传播器（仅涉及单个变量），实现公式描述的约束。通过这种方式，本文将索引的思想转移到有限集约束，同时大大提高了索引可用的抽象水平。该论文证明了派生传播器的健全性和完整性，并提出了运行时分析，包括针对 n 元约束有效执行投影仪的技术。
Ideally, programming propagators as implementations of constraints should be an entirely declarative specification process for a large class of constraints: a high-level declarative specification is automatically translated into an efficient propagator. This paper introduces the use of existential monadic second-order logic as declarative specification language for finite set propagators. The approach taken in the paper is to automatically derive projection propagators (involving a single variable only) implementing constraints described by formulas. By this, the paper transfers the ideas of indexicals to finite set constraints while considerably increasing the level of abstraction available with indexicals. The paper proves soundness and completeness of the derived propagators and presents a run-time analysis, including techniques for efficiently executing projectors for n-ary constraints.