Global difference constraint propagation for finite domain solvers

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Global difference constraint propagation for finite domain solvers

Full text

Pdf (354 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Valencia, Spain

SESSION: Constraints table of contents

Pages 226-235

Year of Publication: 2008

ISBN:978-1-60558-117-0

Authors

Thibaut Feydy	The University of Melbourne, Australia
Andreas Schutt	The University of Melbourne, Australia
Peter J. Stuckey	The University of Melbourne, Australia

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 29, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1389449.1389478 What is a DOI?

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

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Jan V. Leeuwen , Warwick , A. R. Meyer , M. Nival, Handbook of Theoretical Computer Science: Algorithms and Complexity, MIT Press, Cambridge, MA, 1990
	2	S. Brand, N. Narodytska, C.-G. Quimper, P. J. Stuckey, and T. Walsh. Encodings of the sequence constraint. In C. Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, volume 4741 of LNCS, pages 210--224. Springer-Verlag, 2007.
	3	Boris V. Cherkassky , Andrew V. Goldberg, Negative-Cycle Detection Algorithms, Proceedings of the Fourth Annual European Symposium on Algorithms, p.349-363, September 25-27, 1996
	4	S. Cotton and O. Maler. Fast and Flexible Difference Constraint Propagation for DPLL(T). In Theory and Applications of Satisfiability Testing - SAT 2006, volume 4121 of LNCS, pages 170--183. Springer-Verlag, 2006.
	5	CSP2SAT. http://bach.istc.kobe-u.ac.jp/csp2sat/. {Dec07}.
	6	Rina Dechter , Itay Meiri , Judea Pearl, Temporal constraint networks, Artificial Intelligence, v.49 n.1-3, p.61-95, May 1991 [doi>10.1016/0004-3702(91)90006-6]
	7	P. Laborie. Complete MCS-based search: Application to resource constrained project scheduling. In Proceedings IJCAI 2005, pages 181--186, 2005.
	8	M. Lagerkvist and C. Schulte. Advisors for incremental propagation. In C. Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming, volume 4741 of LNCS, pages 409--422. Springer-Verlag, 2007.
	9	R. Niewenhuis, A. Oliveras, and C. Tinelli. Abstract DPLL and Abstract DPLL Modulo Theories. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 3452 of LNAI, pages 36--50. Springer-Verlag, 2005.
	10	Robert Nieuwenhuis , Albert Oliveras , Cesare Tinelli, Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T), Journal of the ACM (JACM), v.53 n.6, p.937-977, November 2006 [doi>10.1145/1217856.1217859]
	11	P.J. Stuckey, M. G. de la Banda, M. Maher, K. Marriott, J. Slaney, Z. Somogyi, M. Wallace, and T. Walsh. The G12 project: Mapping solver independent models to efficient solutions. In P. V. Beek, editor, Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming, number 3709 in LNCS, pages 13--16. Springer-Verlag, 2005.
	12	G. Ramalingan, J. Song, L. Joskowicz, and R. Miller. Solving systems of difference constraints incrementally. Algorithmica, 23:261--275, 1999.
	13	Robert Shostak, Deciding Linear Inequalities by Computing Loop Residues, Journal of the ACM (JACM), v.28 n.4, p.769-779, Oct. 1981 [doi>10.1145/322276.322288]
	14	N. Tamura, A. Taga, S. Kitagawa, and M. Banbara. Compiling finite linear CSP to SAT. In Proceedings of CP-2006, volume 4204 of LNCS, pages 590--603. Springer-Verlag, 2006.
	15	W.-J. van Hoeve, G. Pesant, L.-M. Rousseau, and A. Sabharwal. Revisiting the sequence constraint. In Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP '06), 2006.
	16	C. Wang, F. Ivančić, M. Ganai, and A. Gupta. Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 3835 of LNCS, pages 322--336. Springer-Verlag, 2005.