Stage Master 2 ou Ecole d'ingénieur

Contexte

Le problème SAT, qui consiste à déterminer la satisfiabilité d’un ensemble de clauses en logique propositionnelle, apparaît comme un problème de première importance aussi bien d’un point de vue pratique que théorique (premier problème démontré NP-complet); ses applications sont nombreuses et variées (vérification, planification, …).

Toutefois, le pouvoir d'expression du formalisme clausal reste limité, en particulier lorsqu'on cherche à encoder des problèmes combinatoire classiques, qui se formalisent naturellement dans le cadre des problèmes de satisfaction de contraintes (CSP). Dans ce contexte, la prise en compte de variables à valeurs discrètes induit un codage quadratique en nombre de clauses. De plus, le cadre des CSP offre à l'utilisateur un enrichissement du langage initial au travers de contraintes globales qui peuvent elles aussi s'avérer complexes à traiter lors de la transformation en formules booléennes.

Il est alors possible de considérer une variante du problème initial en considérant la notion de Xclause. Le problème XSAT (pour eXact Satisfiability) est en fait une restriction de SAT dans laquelle chaque clause doit être satisfaite par exactement un littéral. Les Xclauses se révèlent alors très utiles pour encoder de manière naturelle des problèmes de satisfaction de contraintes sur les domaines finis.

Du point de vue de la résolution, alors que le problème SAT bénéficie du développement de techniques très sophistiquées, donnant naissance à des solveurs extrêmement peformants, le problème XSAT n'a été que peu abordé dans la littérature et, le plus souvent, au travers d'algorithmes ad-hoc (prenant par exemple en compte des contraintes de cardinalité sur les clauses). Dans contexte, nous pensons qu'il est préférable de profiter du travail important effectué pour la résolution du problème SAT en vue de d'adapter les meilleurs solveurs à la variante XSAT.

Déroulement du stage

L'objectif de ce projet sera donc d'étudier comment les spécificités induites par la notion de Xclause peuvent être intégrées à un solveur SAT actuel. Dans un second temps, il conviendra également d'aborder la résolution de problèmes mixtes SAT/XSAT et de proposer une approche générale pour faciliter l'utilisation des Xclauses, qui peuvent être vues comme une forme de contraintes globales pour SAT.

Le travail d'implémentation et d'expérimentation s'appuiera sur le solveur MiniSAT, reconnu actuellement comme étant le plus performant du domaine.

Responsables du stage: Lucas Bordeaux, Youssef Hamadi, Microsoft Research, Cambridge, et Frédéric Lardeux, Frédéric Saubion, LERIA, Université d’Angers
Lieu du stage: Laboratoire commun Microsoft-INRIA, Saclay
Rémunération: indemnités de stage au tarif syndical suivant ressources (entre 350 et 600 euros par mois)