Global difference constraint propagation for finite domain solvers

Thibaut Feydy, Andreas Schutt, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

12 Citations (Scopus)

Abstract

Difference constraints of the form x - y ≤ d are well studied, with efficient algorithms for satisfaction and implication, because of their connection to shortest paths. Finite domain propagation algorithms however do not make use of these algorithms, and typically 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. We give experiments showing that treating difference constraints globally can substantially improve on the standard propagation approach.

Original languageEnglish
Title of host publicationPPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
Pages226-235
Number of pages10
DOIs
Publication statusPublished - 17 Dec 2008
Externally publishedYes
EventPPDP 2008: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - Valencia, Spain
Duration: 15 Jul 200817 Jul 2008

Publication series

NamePPDP'08 - Proceedings of the 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming

Conference

ConferencePPDP 2008: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
CountrySpain
CityValencia
Period15/07/0817/07/08

Keywords

  • Difference logic
  • Global constraints
  • Propagation

Cite this