• Laure Brisoux Devendeville
    • Thèse soutenue le :
    • 2 déc. 1999

    Résumé

    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.