• Thèse soutenue le :
  • 2005-02-04

Résumé

Un domaine particulièrement fertile de la recherche en intelligence artificielle ces dix dernières années a concerné l’algorithmique pour SAT, c’est-à-dire l’algorithmique pour le problème de décision qui consiste à vérifier la consistance d’un ensemble fini de clauses propositionnelles. Ce problème revêt une importance considérable en informatique théorique et en intelligence artificielle. S’agissant du problème NP-complet de référence, c’est pour la communauté scientifique un défi important que de faire reculer les limites de taille des instances qui peuvent être résolues pratiquement, ainsi que de comprendre les difficultés inhérentes de ce problème. A cet égard, les progrès pratiques enregistrés sont impressionnants. Il est maintenant possible de résoudre de très grandes instances du problème SAT, instances pourtant réputées difficiles, en des temps de calcul très minimes. Sur le plan pratique, l’algorithmique pour SAT apparaît utile dans de nombreux domaines de l’informatique, et en particulier en intelligence artificielle. De fait, elle est utile pour la vérification de la cohérence de bases de connaissances propositionnelles, tout comme la vérification de circuits de type VLSI. Puisque la déduction peut s’effectuer par réfutation, c’est également un outil possible pour effectuer de la déduction. Beaucoup de formes de raisonnement non monotone reposent également sur des contraintes de consistance, ou peuvent être modélisées par celles-ci. Ainsi, c’est souvent en raison de l’absence d’informations contradictoires ou d’exceptions que nous pouvons effectuer des raisonnements au caractère plausible. Cette absence d’informations ou de contradictions se modélise naturellement, dans le cadre booléen, par un test de consistance logique. Des problèmes tels que la planification ont aussi trouvé une manière prometteuse de les résoudre par une codification à l’aide de SAT. D’autres domaines applicatifs, comme le diagnostic de pannes sont aussi des domaines ou l’algorithmique pour SAT peut s’avérer utile : l’apparition de pannes se traduisant par l’inconsistance d’une modélisation où l’on a supposé par défaut l’absence de pannes.

Cette thèse a été écrite dans ce contexte. Nous nous sommes intéressés à l’algorithmique pour SAT en vue de décrire des approches novatrices pour différents problèmes d’intelligence artificielle, dont la complexité dans le pire des cas se situe souvent plus haut que SAT dans la hiérarchie polynomiale. A cet égard, notre contribution est essentiellement conceptuelle. Nous avons abordé plusieurs questions, en essayant de dégager de nouvelles approches et algorithmes.

Notre contribution se décline selon quatre directions.

En tout premier lieu, nous nous sommes intéressés à une méta-heuristique décrite dans <>. Cette heuristique suggère que les contraintes les plus souvent falsifiées lors d’une recherche locale qui échoue dans un temps prédéterminé sont souvent les contraintes impossibles à résoudre si le problème n’admet pas de solution. Dans un contexte de résolution d’instances de SAT, cette heuristique suggère que les clauses les plus souvent falsifiées lors d’une recherche locale qui n’arrive pas à détecter un modèle dans un temps prédéterminé choisi suffisamment long, participent vraisemblablement à l’union des noyaux de l’instance, si celle-ci est réellement inconsistante. Un noyau est un ensemble minimal et inconsistant de clauses. Une recherche complète devrait se concentrer sur ces clauses pour démontrer l’inconsistance de l’instance le plus rapidement. Nous avons analysé cette heuristique et avons proposé une manière de l’améliorer. De fait, lors d’une recherche locale, toutes les clauses falsifiées n’appartiennent pas nécessairement à des noyaux mais se voient néanmoins comptabilisées. Nous proposons une caractérisation plus fine des clauses falsifiées qui doivent être comptabilisées, en écartant des classes de clauses falsifiées qui ne devraient pas être prises en considération.

Une seconde contribution repose dans la proposition d’un algorithme visant à calculer de la manière la plus efficace des modèles où certains marqueurs (propositions d’anormalité à la McCarthy) mis à vrai sont minimisés.

Notre troisième contribution s’inscrit dans l’étude de techniques de validation de base de connaissances, et plus particulièrement du test de consistance logique. Ce test est vital pour les bases de connaissances sur lesquelles on effectue de la déduction, car à partir d’un ensemble inconsistant d’informations, on peut déduire tout et son contraire. Nous nous sommes placés dans un contexte de construction incrémentale de bases de connaissances, où à chaque ajout d’informations nous vérifions si la consistance de l’ensemble est préservée, et, dans le cas contraire, il faut indiquer à l’utilisateur quelles sont les informations qu’il conviendrait d’extraire pour restaurer la consistance. Le cadre logique choisi est celui du premier ordre fini et où un pré-ordre de préférence entre clauses existe, indiquant quelles informations peuvent être prioritairement rejetées en cas de consistance à restaurer. Nous nous sommes intéressés à la manière selon laquelle nous pourrions effectuer les tests de consistance sur la base de connaissances instanciée dans le cadre propositionnel. Afin d’éviter une explosion combinatoire de la représentation, nous ne considérons qu’un schéma de vérification de consistance et d’inconsistance à profondeur de raisonnement limité, ainsi que proposé dans <>. Ce schéma explore l’interaction entre les informations ajoutées et le contenu actuel de la base de connaissances à différents niveaux successifs d’interaction. Il respecte le critère de préférence entre informations.

Enfin, notre quatrième contribution concerne le domaine du diagnostic de pannes par des techniques d’intelligence artificielle. Plus précisément, nous nous sommes intéressés au syndrome dit de l’arbre de Noël. Ce syndrome est celui décrit parfois par des pilotes de chasse lorsque des pannes majeures apparaissent en vol. Un grand nombre de voyants se mettent à clignoter sur le tableau de bord, comme un arbre de Noël dont les guirlandes clignotent, rendant difficile l’évaluation exacte et rapide de la situation et des causes réelles de dysfonctionnement. De fait, une panne peut en entraîner d’autres, prévues ou non par une modélisation a priori. C’est un problème classique dans de nombreux systèmes complexes critiques qui a été décrit également lors d’incidents majeurs dans les centrales nucléaires. Nous proposons une approche novatrice pour, face à ce syndrome, indiquer rapidement à l’opérateur quelle est la source la plus importance ou la plus grave de panne. L’approche repose sur une prioritisation a priori des causes possibles de dysfonctionnement et fait appel aux techniques avancées pour SAT pour indiquer la cause de panne à mettre en évidence en cas d’incident.