Value Removal Explanations in Constraint Programming and Application to Declarative Diagnosis
Constraint programming over finite domains his efficiency to deal with difficult problems, so to the view point of their modelling that of their resolution. The solvers used to obtain their solutions mix domain reduction to labeling methods and begin using notions of explanations.
This thesis proposes three contributions to the domain of constraint programming. First, domain reduction is revisited in a set theoretical framework and seen as a fix-point computation. Next, this framework allows a natural and general definition of explanation, called explanation tree. These proof trees are inductively defined by rules expressing the removal of a value as a consequence of other removals. At last, the vision of the explanation trees as a declarative trace of the computation allows using them to adapt the declarative diagnosis of missing answer to constraint programming.
