Abstract FR:

La satisfaction de contraintes booléennes est un problème NP-Complet. Plusieurs systèmes existent pour résoudre un problème SAT. Ceux-ci varient selon les langages de programmation et les méthodes de résolution (inspirées d'algorithmes ou réunissant un ensemble de techniques). Nous proposons un langage en logique propositionnelle, pour une écriture naturelle du problème et un démonstrateur automatique pour satisfaire les contraintes. Le démonstrateur automatique choisi est une méthode basée sur la réécriture (méthode de Hsiang) que l'on peut paramétrer (heuristiques) pour la rendre plus ou moins complète. Il est également étendu pour connaitre le nombre de solutions ou obtenir un système équivalent selon l'option choisie. On trouvera dans cette thèse, d'une part un panorama des méthodes de résolution servant de référence, des techniques et langages existants a ce jour, d'autre part l'implantation d'un langage de programmation et d'une méthode de résolution avec des heuristiques.