Difference constraints of the form $x - y \leq d$ are well studied, with efficient algorithms for satisfaction and implication due to their connection to shortest paths. However, finite domain propagation algorithms typically do not leverage these algorithms and treat each difference constraint as a separate propagator.
While propagation guarantees completeness of solving, it can be unnecessarily slow. In this paper, we describe how to build a bounds consistent global propagator for difference constraints that treats them all simultaneously.
Although SAT modulo theory solvers have included theory solvers for difference constraints for some time, we show that the requirements on the propagator are quite different. Crucially, we demonstrate how to explain propagations by a global difference constraint propagator to use it within a lazy clause generation solver.
Our experiments show that treating difference constraints globally can significantly improve on the standard propagation approach.
Blogger's Review: The proposed global difference constraint propagation method significantly enhances the efficiency of constraint programming, especially demonstrating strong performance advantages when handling complex constraints. Viewing difference constraints as a whole rather than processing them separately effectively reduces computation time, bringing new insights and ideas to the field of constraint solving.