Ces dernières années, de nombreux travaux se sont concentrés
sur le problème de décision SAT : un ensemble de clauses propositionnelles
est-il oui ou non consistant ? Clairement, dans beaucoup de domaines
applicatifs, une réponse négative à pareille question n’est pas très
informative. Plus intéressant est de déterminer pourquoi un ensemble de clauses est inconsistant. Plus précisément,
on souhaite souvent déterminer quels sont les plus petits ensembles de clauses
qui se contredisent.
Le calcul des plus petits ensembles de clauses
contradictoires, appelés noyaux, au sein d’un ensemble de clauses inconsistant
est un problème dont la complexité, dans le pire des cas, est élevée. Dans ce
travail de stage, nous allons étudier et essayer de trouver des heuristiques
qui permettent de calculer exactement ou d’approcher les noyaux dans des temps
de calcul raisonnables.
Une première partie du travail consistera à analyser et comprendre
des heuristiques existantes, et à les expérimenter sur des « benchmarks »
classiques pour SAT. Dans la seconde partie du travail, on visera à améliorer
ces heuristiques et à les incorporer dans des algorithmes complets pour la
détection de noyaux inconsistants.
Ce sujet est conçu de manière à pouvoir être poursuivi en
thèse.
Encadrement
B. Mazure & É. Grégoire – CRIL {mazure,gregoire}@cril.univ-artois.fr
Références