Identifiant pérenne de la notice : 206250703
Notice de type
Notice de regroupement
Note publique d'information : Dans de nombreux domaines de l'informatique, la représentation des problèmes est tout
aussi cruciale que la méthode de résolution qui est ensuite utilisée. Le formalisme
considéré ici est la logique propositionnelle, laquelle permet souvent d'allier puissance
d'expression et efficacité en pratique. Cette thèse traite de l'amélioration des algorithmes
de résolution pour SAT (complets et incomplets) et de l'extension du formalisme propositionnel
en améliorant la puissance d'expression et en préservant l'efficacité des algorithmes
de résolution classiques. Nous proposons de nouvelles techniques pour les méthodes
complètes, basées sur la procédure de Davis, Logemann et Loveland ainsi que pour les
méthodes incomplètes basées sur la recherche locale. Nous présentons, en premier lieu,
deux heuristiques simples et efficaces pouvant se greffer simplement aux algorithmes
existants. Ces heuristiques sont de deux types : la première est basée sur l'exploitation
des échecs de l'arbre de démonstration, la seconde, sur la prise en compte de la structure
du problème pour améliorer les algorithmes de résolution. Ces heuristiques simples
diminuent la taille de l'arbre de recherche sur la plupart des classes d'instances
utilisées. En ce qui concerne les algorithmes incomplets pour SAT, notre contribution
porte sur le développement de deux stratégies de réparation pour les méthodes de recherche
locale. La première prend en compte la structure de la formule. Celle-ci utilisée
avec TSAT améliore nettement les performances de celui-ci et permet de régler plus
facilement la taille de la liste tabou associée. La seconde utilise différents schémas
de coopération entre différents algorithmes de recherche locale. Enfin, nous présentons
deux extensions aux techniques décrites précédemment. La première est une extension
du formalisme et des algorithmes utilisés en calcul propositionnel. La seconde traite
de l'utilisation des techniques de résolution du problème SAT au premier ordre fini.
paprika.idref.fr
data.idref.fr
Documentation
