Computing Explanations for the Unary Resource Constraint

Abstract. Integration of explanations into a CSP solver is a technique addressing difficult question “why my problem has no solution”. Moreover, explanations together with advanced search methods like directed backjumping can effectively cut off parts of the search tree and thus speed up the search. In order to use explanations, propagation algorithms must provide some sort of reasons (justifications) for their actions. For binary constraints it is mostly easy. In the case of global constraints computation of factual justifications can be tricky and/or computationally expensive. This paper shows how to effectively compute explanations for the unary resource constraint. The explanations are computed in a lazy way. The technique is experimentally demonstrated on job-shop benchmark problems. The following propagation algorithms are considered: edge-finding, not-first/not-last and detectable precedences. Speed of these filtering algorithms and speed of the explanation computation is the main interest.