Abstract FR:

Dans cette thèse, nous modélisons la résolution de problèmes de satisfaction de contraintes (csps) comme un processus de déduction. Nous formalisons les techniques de résolution de csps sur des domaines finis en utilisant des règles de réécriture et des stratégies. Les règles expriment les transformations réalisées par ces techniques sur les contraintes et les stratégies contrôlent l'application de ces règles. Cette approche nous permet de vérifier facilement des propriétés telles que la correction, la complétude et la terminaison d'un solveur. L'utilisation d'un langage de stratégies puissant nous permet de décrire les heuristiques d'une manière très abstraite et flexible. En utilisant cette approche déductive, nous pouvons prouver l'existence ou l'inexistence d'une solution : il nous suffit de regarder le terme de preuve pour reconstruire exactement une preuve du calcul réalisé. Afin de valider notre approche, nous avons implanté le système colette dans le langage elan. Nous étudions tout d'abord le problème de la résolution d'un ensemble de contraintes élémentaires qui sont combinées par des operateurs de conjonction. Nous nous intéressons ensuite à la résolution de problèmes d'optimisation en utilisant des techniques de résolution de csps. Nous abordons l'extension du langage de contraintes afin de considérer la combinaison des contraintes élémentaires avec les connecteurs logiques de disjonction, d'implication et d'équivalence. Le traitement des contraintes disjonctives est décrit en détail. Finalement, nous étudions la coopération de solveurs. En utilisant les operateurs de stratégies concurrents du langage elan, nous décrivons d'une manière abstraite des schémas de coopération séquentiels et concurrents. Pour d'autres types de coopération, nous utilisons des primitives de bas niveau qui sont disponibles dans elan pour la communication entre processus.