Search papers, labs, and topics across Lattice.
This paper introduces a global propagator for difference constraints that simultaneously processes multiple constraints, enhancing efficiency over traditional methods that treat each constraint separately. By leveraging the connection between difference constraints and shortest paths, the authors demonstrate that their approach can significantly reduce the time required for constraint satisfaction. Experimental results reveal that this global method outperforms standard finite domain propagation algorithms, providing a more effective solution for constraint programming tasks.
Treating difference constraints globally can lead to substantial efficiency gains in constraint satisfaction, outperforming traditional methods by a significant margin.
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.
