Une approche déductive de la résolution de problèmes de satisfaction de contraintes

In this thesis, we model the resolution of constraint satisfaction problems (CSPs) as a deductive process. We formalise CSP solving techniques over finite domains using rewrite rules and strategies. The rules express the transformations over the set of constraints carried out by these techniques. The strategies control the application of these rules. This approach allows us to easily verify properties like correctness, completeness, and termination of a solver. The use of a powerful strategy language allows us to describe heuristics in an abstract and flexible way. Furthermore, using this deductive approach we can justify theexistence or absence of a solution: we just have to look at the proof term in order to reconstruct exactly a proof of the computation carried out. To validate our approach, we have implemented the system COLETTE using the ELAN language.Firstly, we study the resolution of a set of elementary constraints combined by conjunction operators. Next, we focus on the resolution of optimisation problems using CSP solving techniques. Then, we extend the constraint language in order to consider the combination of elementary constraints by the logical operators of disjunction, implication, and equivalence. The treatment of disjunctive constraintsis described in detail. Finally, we study the cooperation of solvers. Using the concurrent strategy operators of the ELAN language we describe in an abstract way some schemes of sequential and concurrent cooperation. For other types of cooperation, we use low-level primitives for process communicationavailable in ELAN.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 opérateurs 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 opérateurs 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