论文标题
通过抽象解释的模块化约束求解器合作
Modular Constraint Solver Cooperation via Abstract Interpretation
论文作者
论文摘要
约束求解器之间的合作很困难，因为不同的解决范式具有不同的理论基础。最近的作品表明，抽象解释可以为各种约束求解器提供统一的理论。特别是，它依赖于抽象域，这些域将约束语言捕获为有序结构。本文的关键见解是将合作计划视为抽象领域组合。我们提出了一个模块化框架，可以无缝地添加和组合求解器和合作方案。这不同于现有方法（例如，合作方案通常是固定的SMT）（例如，纳尔逊·奥普彭（Nelson-Oppen））。我们为两个新的合作方案做出了贡献：（i）间隔传播器完成，允许抽象域交换界限约束，以及（ii）延迟的产品，这些产品交换了两个抽象域之间约束过度的限制。此外，延迟产品基于逻辑编程的延迟目标，它表明抽象域也可以捕获约束解决的控制方面。最后，为了实现模块化，我们提出共享产品以结合抽象领域和合作方案。我们的方法已经完全实施，我们提供了有关灵活的车间调度问题的各种示例。正在考虑在TPLP中接受。
Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT where the cooperation scheme is usually fixed (e.g., Nelson-Oppen). We contribute to two new cooperation schemes: (i) interval propagators completion that allows abstract domains to exchange bound constraints, and (ii) delayed product which exchanges over-approximations of constraints between two abstract domains. Moreover, the delayed product is based on delayed goal of logic programming, and it shows that abstract domains can also capture control aspects of constraint solving. Finally, to achieve modularity, we propose the shared product to combine abstract domains and cooperation schemes. Our approach has been fully implemented, and we provide various examples on the flexible job shop scheduling problem. Under consideration for acceptance in TPLP.
