Explaining alldifferent

Downing, N., Feydy, T. and Stuckey, P.J.

Lazy clause generation is a powerful approach to reducing search in constraint programming. For use in a lazy clause generation solver, global constraints must be extended to explain themselves. Alternatively they can be decomposed into simpler constraints which already have explanation capability. In this paper we examine different propagation mechanisms for the alldifferent constraint, and show how they can be extended to explain themselves. We compare the different explaining implementations of alldifferent on a variety of problems to determine how explanation changes the trade-offs for propagators. The combination of global alldifferent propagators with explanation leads to a state-of-the-art constraint programming solution to problems involving alldifferent.

Cite as: Downing, N., Feydy, T. and Stuckey, P.J. (2012). Explaining alldifferent. In Proc. Australasian Computer Science Conference (ACSC 2012) Melbourne, Australia. CRPIT, 122. Reynolds, M. and Thomas, B, Eds., ACS. 115-124

(from crpit.com) (local if available)