arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2008.01415cs.AI
收藏

基于抽象解释的模块化约束求解器协作

Modular Constraint Solver Cooperation via Abstract Interpretation

University of Angers(昂热大学);University of Nantes(南特大学)

Pierre Talbot, Éric Monfroy, Charlotte Truchet

摘要:

约束求解器之间的合作是困难的,因为不同的解决范式有不同的理论基础。最近的工作表明,抽象解释可以提供一个统一的理论,各种约束求解。特别是,它依赖于抽象域,将约束语言捕获为有序结构。本文的主要观点是将合作方案看作是抽象域的组合。我们提出了一个模块化的框架,求解器和合作计划可以无缝地添加和组合。这不同于诸如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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑