Explaining alldifferent

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 propagaton. The combination of global alldifferent propagators with explnation leads to a state-of-the-art constraint programming solution to problems involving alldifferent.