[M2R 2012-2013] Programmation linéaire modulo disjonctions

Laboratoire : Verimag (http://www-verimag.imag.fr/)

Équipe : SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE)

Encadrants : David Monniaux <David.Monniaux@imag.fr>, Claire Maïza <Claire.Maiza@imag.fr>.

 Contexte Scientifique

On connaît depuis les années 1950 la programmation linéaire, c’est-à-dire calculer le maximum d’une forme linéaire sur l’ensemble des solutions d’un système (conjonction) d’inégalités linéaires. Cependant, certains problèmes s’expriment naturellement par des formules avec non seulement des conjonctions, mais aussi des disjonctions. Il s’agit ici de concevoir des méthodes efficaces adaptées à ce cas de figure, en utilisant des techniques de SMT-solving.

 Sujet

Lire la bibliographie sur le SMT-solving et la programmation linéaire, développer une technique d’optimisation modulo SMT, l’implémenter.

 Compétences Attendues

  • De bonnes bases en algorithmique, logique et recherche opérationnelle
  • C++ ou Caml

 Contexte de Travail

Le stagiaire sera encadré par David Monniaux et Claire Maïza (permanents du laboratoire).