[M2R 2012-2013] Contraintes non linéaires

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

Encadrants: Pierre Corbineau <Pierre.Corbineau@imag.fr>, David Monniaux <David.Monniaux@imag.fr>

 Contexte Scientifique

Dans un contexte de calcul scientifique, de preuve automatique de théorèmes, ou d’analyse de programmes, on a parfois besoin de montrer qu’un système d’inégalités non linéaires n’a pas de solutions ou de calculer une borne sur ses solutions. On a même parfois besoin d’une preuve forte que cette absence de solution ou cette borne sont correctes.

Nous avons développé une technique qui produit en sortie non seulement la réponse (p.ex. "le système n’a pas d’équations") mais surtout des coefficients qui permettent une vérification facile que cette réponse est justifiée (Monniaux & Corbineau, ITP 2011).

 Sujet

Notre technique souffre d’inefficacités diverses ; par exemple, elle n’exploite pas les symétries des problèmes, ou très peu. Il s’agit donc de chercher des améliorations.

 Compétences Attendues

  • De bonnes bases en algorithmique et recherche opérationnelle
  • Connaissance souhaitable du langage Python

 Contexte de Travail

Le stagiaire sera encadré par Pierre Corbineau et David Monniaux (permanents du laboratoire).