Abstract FR:

En théorie, la résolution de CSPs est un problème NP-complet. L'élimination de la symétrie permet de diminuer cette complexité dans la pratique. Dans le cadre de cette thèse, nous avons étudié en première partie la symétrie locale ainsi que la dominance dans les CSPs à contraintes de différence. Nous avons donné une condition suffisante pour tester la symétrie et la dominance entre deux valeurs d'un même domaine. En deuxième partie, nous nous sommes intéressés au cas plus général des CSPs binaires quelconques, en proposant la méthode de résolution LSBDS qui exploite la symétrie locale détecté par SAUCY. En troisième et dernière partie de cette thèse, nous avons proposé une nouvelle approche incomplète pour le test d'inconsistance de CSP binaire. Cette approche est basée sur les notions de la dominance et de la coloration de la microstructure. Cette technique est aussi une contribution pour un challenge encore très peu étudié : preuve d'inconsistance par des méthodes incomplètes