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).
