Abstract FR:

Le problème SAT qui consiste à montrer, étant donnée une formule du calcul propositionnel, qu'il existe une affectation des variables satisfaisant la formule, est un problème NP-complet (Cook 1971). Or, les problèmes de recherche se formulant en SAT recouvrent de nombreuses applications industrielles comme la vérification et conception de circuit, la planification etc. Pour pouvoir résoudre en pratique ces problèmes fortement combinatoires, plusieurs approches ont été récemment proposées : les méthodes de simplification, de recherche locale, recuit simulé, évolution artificielle, réseaux neuronaux, programmation linéaire en 0/1 etc. Parallèlement, d'autres recherches ont été développées pour essayer de mieux comprendre le fonctionnement de ces méthodes. Des progrès significatifs ont été accomplis dans ce sens. Cette thèse présente SCORE (FD/B), un environnement qui intègre un langage de programmation de haut niveau dédié aux problèmes SAT structurés, une méthode de résolution complète utilisant la recherche locale et un laboratoire de tests avec interface graphique. Les principaux traits de conception du langage SCORE (FD/B) sont : modularité, structures de tableaux, structures de contrôle et clauses de cardinalités. Ils favorisent une description déclarative et concise des problèmes. De plus, notre approche langage permet de détecter statiquement, a la traduction des programmes, des propriétés de symétrie qui seront exploitées plus tard par le solveur de SCORE (FD/B). La méthode de résolution que nous avons développée pour les problèmes SAT structurés et aléatoires, combine le retour arrière et la recherche locale. C'est une méthode complète. Nous proposons différentes options et heuristiques qui permettent de résoudre avec efficacité des problèmes réputés difficiles, notamment les problèmes insatisfiables. Enfin, pour pouvoir expérimenter, évaluer et comparer SCORE (FD/B), nous avons développé un environnement avec interface graphique.