Cédric Piette (CRIL - Université d'Artois)

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.

Cette présentation se focalise sur les aspects algorithmique et meta- heuristique de la localisation d’ensembles minimaux inconsistants de contraintes (MUS). Dans un premier temps, 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 d’un MUS sera proposé. Ensuite, un nouveau concept relatif au problème de satisfaction de contraintes (CSP) sera présenté. Celui-ci permet de prendre en considération les tuples du problème et non ses contraintes. La viabilité de ce concept sera 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 confirmant l’intérêt de ces approches d’un point de vue pratique seront également proposés.