Abstract FR:

La programmation par contraintes sur domaines finis a montré son efficacité pour traiter les problèmes difficiles, tant au point de vue de leur modélisation que de leur résolution. Les solveurs utilisés pour obtenir leurs solutions mêlent des techniques de réduction de domaine à des techniques d'énumération et commencent à utiliser des notions d'explications. Cette thèse propose trois contributions au domaine de la programmation par contraintes. Tout d'abord la réduction de domaine est reformulée en terme ensembliste et vue comme un calcul de point fixe. Ensuite, ce cadre permet une définition naturelle et générale d'explication, appelée arbre explicatif. Ces arbres de preuve sont inductivement définis par des règles exprimant le retrait d'une valeur comme conséquence d'autres retraits. Enfin, la vision des arbres explicatifs en tant que trace déclarative du calcul permet de les utiliser pour adapter le diagnostic déclaratif de réponse manquante à la programmation par contraintes.