Techniques algorithmiques pour l'extraction de formules minimales inconsistantes
- Doctorant:
- Cédric Piette
- Directeur de thèse :
- Éric Grégoire
- Co-encadrant de thèse :
- Bertrand Mazure
- Thèse soutenue le :
- 21 nov. 2007 • Salle des thèses
Résumé
Les problèmes de satisfaisabilité d’une formule propositionnelle (SAT) et de satisfaction de contraintes (CSP) sont des domaines de recherche majeurs en intelligence artificielle, et pour lesquels de nombreuses approches sont proposées chaque année dans le but d’élargir la classe des instances traitables. Ces améliorations permettent aujourd’hui de résoudre certains problèmes possédant des milliers, voire des millions de variables, rendant solubles en quelques secondes des problèmes considérés hors de portée il y a peu.
Une conséquence naturelle de ces progrès incessants est la modélisation de problèmes de taille de plus en plus importante. Or, quand des formules de grande taille censées être satisfaisables sont prouvées incohérentes, il peut être extrêmement difficile de déterminer la cause du problème, dans l’espoir de le réparer. En effet, contrairement aux problèmes cohérents pour lesquels un modèle est généralement produit, une réponse négative au test de la consistance d’une formule n’apporte que peu d’informations. Il semble intéressant de déterminer pourquoi un problème est sans solution ; précisément, dans ce cas, on cherche à effectuer l’extraction des plus petits ensembles de contraintes contradictoires. Malheureusement, il s’agit d’un problème d’une complexité extrêmement élevée dans le pire des cas, pour lequel les approches complètes et exactes sont souvent inapplicables en pratique. Il semble alors naturel de se diriger vers des méthodes heuristiques.
Après une présentation générale de la thématique abordée (partie 1), la deuxième partie de cette thèse est consacrée à notre contribution au cadre clausal booléen. Dans un premier temps, nous présentons un algorithme basé sur un nouveau concept permettant de prendre en compte un voisinage partiel des interprétations parcourues par une recherche locale, dans le but de faire l’approximation voire le calcul exact d’un MUS. Ensuite, nous montrons comment l’hybridation d’une méthode incomplète à la meilleure approche connue pour le calcul exhaustif de tous les MUS peut permettre à cette dernière d’éviter des appels à des oracles NP et CoNP, lui faisant gagner un ordre de grandeur en temps de calcul. Cependant, même avec cette amélioration, le nombre de MUS au sein d’une CNF, exponentiel dans le pire cas, peut rendre ce calcul irréalisable en pratique. Aussi, plusieurs méthodes efficaces permettant l’approximation de cet ensemble sont introduites. Cette partie se termine par une mise en application des techniques présentées à la gestion de l’incohérence des bases de connaissances stratifiées.
La troisième partie porte sur le problème de satisfaction de contraintes (CSP). Dans une première contribution, nous revisitons le meilleur algorithme connu et proposons des améliorations qui accélèrent son calcul, et étendent en conséquence la classe des problèmes traitables. Ensuite, un nouveau concept qui raffine celui de MUC, défini classiquement par la communauté, est présenté. Celui-ci permet de prendre en considération les tuples du problème et non ses contraintes. La viabilité de ce concept est démontrée à travers des propriétés qui démontrent que le procédé mis au point permet de réparer un problème sans retrait de contraintes. Des résultats expérimentaux confirment l’intérêt de l’approche, d’un point de vue pratique.
Composition du jury
- Eric Grégoire (Université d’Artois) (directeur de thèse)
- Youssef Hamadi (Microsoft Research Cambridge)
- Pierre Marquis (Université d’Artois)
- Bertrand Mazure (Université d’Artois) (co-directeur de thèse)
- Lakhdar Sais (Université d’Artois)
- Thomas Schiex (INRA Toulouse)
- Laurent Simon (INRIA Futurs Orsay)
- Gérard Verfaillie (Office National d’Études et de Recherches Aérospatiales)