AI 中文总结
研究如何构建全局差异约束传播器，核心方法是将差异约束同时处理，主要贡献是能显著改进标准传播方法，还展示了如何在惰性子句生成求解器中使用并解释该传播器。
AI 中文摘要
形式为$x - y \leq d$的差异约束已得到充分研究，因其与最短路径的联系，有高效的满足和蕴含算法。然而，有限域传播算法通常不使用这些算法，将每个差异约束视为单独的传播器。传播虽能保证求解的完备性，但可能不必要地慢。本文描述了如何构建一个同时处理所有差异约束的（边界一致）全局传播器。SAT模理论求解器已有差异约束的理论求解器，但全局差异约束传播器的要求不同。关键是展示了如何通过全局差异约束传播器解释传播，以便在惰性子句生成求解器中使用。实验表明，全局处理差异约束可显著改进标准传播方法。
英文摘要
Difference constraints of the form $x - y \leq d$ are well studied, with efficient algorithms for satisfaction and implication, because of their connection to shortest paths. Finite domain propagation algorithms, however, typically do not make use of these algorithms, and treat each difference constraint as a separate propagator. Propagation does guarantee completeness of solving, but can be needlessly slow. In this paper we describe how to build a (bounds consistent) global propagator for difference constraints that treats them all simultaneously. SAT modulo theory solvers have included theory solvers for difference constraints for some time. While a theory solver for difference constraints gives the basis of a global difference constraint propagator, we show how the requirements on the propagator are quite different. Crucially, we show how to explain propagations by a global difference constraint propagator, in order to use it within a lazy clause generation solver. We give experiments showing that treating difference constraints globally can substantially improve on the standard propagation approach.
