Note publique d'information : 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.
paprika.idref.fr
data.idref.fr
Documentation
