De la satisfaisabilité à la compilation de bases de connaissances propositionnelles / Bertrand Mazure ; directeur de thèse Eric Grégoire

Date :

Editeur / Publisher : [S.l.] : [s.n.] , 1999

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Intelligence artificielle

Représentation des connaissances

Calcul des propositions

Grégoire, Eric (Directeur de thèse / thesis advisor)

Université d'Artois (1991-....) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : La représentation des connaissances et les problèmes d'inférences associés demeurent une problématique riche et centrale en informatique et plus précisément en intelligence artificielle. Le formalisme considéré dans cette thèse est la logique propositionnelle. A moins que p = np, la déduction en logique propositionnelle n'admet pas de solutions à la fois générales et efficaces. Deux problèmes directement connectés à la déduction sont abordés : la satisfaisabilité et la compilation de bases de connaissances propositionnelles. Après une présentation de la thématique abordée, une étude des méthodes de résolution du problème SAT est réalisée. Un nouvel algorithme de recherche locale, basé sur la méthode tabou, est proposé. Un résultat empirique permet de régler la taille de la liste tabou en fonction du nombre de variables pour des instances KSAT aléatoires. En ce qui concerne les algorithmes complets, notre contribution porte sur une généralisation du théorème de partition du modèle et sur la proposition de plusieurs de schémas de coopération (extrêmement performants en pratique) entre méthodes complètes et incomplètes. La présentation de résultats empiriques, mettant en évidence un lien entre la probabilité de positiver un littéral et le pic de difficulté des instances aléatoires, conclue la partie dédiée à SAT. La dernière partie est consacrée au problème de la compilation logique de bases de connaissances. Nous proposons une nouvelle technique de compilation préservant l'équivalence, reposant sur l'idée de déterminer un ensemble de formules traitables, appelé couverture traitable, sémantiquement équivalent à la formule initiale. Ce type de couverture généralise la notion de couverture d'impliquants. Nous proposons trois cas particuliers de couvertures : modulo une théorie, de simplifications traitables et d'hyper-impliquants. Les résultats théoriques et pratiques obtenus montrent que ces approches améliorent nettement les approches existantes.