Explaining the propagator.

The global constraint was proposed for modelling cumulative resources in scheduling problems for finite domain (FD) propagation. Since that time a great deal of research has investigated new stronger and faster filtering techniques for , but still most of these techniques only pay off in limited cases or are not scalable. Recently, the 'lazy clause generation' hybrid solving approach has been devised which allows a finite domain propagation engine possible to take advantage of advanced SAT technology, by 'lazily' creating a SAT model of an FD problem as computation progresses. This allows the solver to make use of SAT explanation and autonomous search capabilities. In this article we show how, once we use lazy clause generation, modelling the constraint by decomposition creates a highly competitive version of . Using decomposition into component parts automatically makes the propagator incremental and able to explain itself. We then show how, using the insights from the behaviour of the decomposition, we can create global constraints that explain their propagation. We compare these approaches to explaining the constraint on resource constrained project scheduling problems. All our methods are able to close a substantial number of open problems from the well-established PSPlib benchmark library of resource-constrained project scheduling problems. [ABSTRACT FROM AUTHOR]