Stage - Ingénieur Développeur Ocaml H/F Dassault Systèmes

Le solveur de contraintes actuellement mis en oeuvre dans Stimulus utilise une combinaison de BDDs (Binary Decision Diagrams) [3, 4] et de polyèdres convexes, manipulés à l'aide de l'algorithme de Chernikova [5, 6]. La complexité théorique de la résolution des contraintes considérées dans Stimulus est NP-complet ou exponentielle en le nombre de variable, dans le pire des cas. La complexité en pratique sur les exemples concrets est heureusement beaucoup plus favorable. Néanmoins, notamment dans le cas des polyèdres, le pire des cas est facile à produire...

Vos Missions

Objectif du stage : expérimenter d'autres solveurs de contraintes

L'objectif principal du stage est donc de remplacer la manipulation de polyèdres convexes fondée sur l'algorithme de Chernikova par un algorithme de programmation linéaire de type simplexe, implanté dans de nombreuses librairies OpenSource, pour pouvoir comparer les performances respectives des deux approches dans le cadre de Stimulus.

- Vous devrez d'abord identifier les bibliothèques de programmation linéaire existantes qui répondent aux besoins de Stimulus (arithmétique exacte, aspects incrémentaux, etc...) ;
- Ensuite, vous devrez proposer une architecture adéquate pour interfacer le solveur de Stimulus avec la bibliothèque de programmation linéaire sélectionnée, et la mettre en oeuvre ;
- Enfin, il s'agira d'expérimenter la solution sur les nombreux modèles Stimulus à disposition de l'équipe.

Si le temps le permet, vous aborderez l'étape suivante consistant à expérimenter l'usage d'un solveur « SMT » (Sat Modulo Theory) comme AltErgo [7], qui remplacerait à la fois les BDDs et les polyèdres convexes. Le défi est ici d'introduire de l'aléa dans le tirage des solutions fait par un tel solveur.

Qualifications

Etudiant(e) préparant un diplôme de niveau Bac +5, Ecole d'Ingénieur ou Master Universitaire, vous vous spécialisez en Informatique et recherchez un stage de fin d'études à compter de janvier 2026.

Vous êtes familier avec le langage OCaml.

Des connaissances en analyse de programme et en méthodes formelles seront appréciées.

On attend de vous de la curiosité, de la rigueur et une certaine autonomie.

Vous serez amené(e), au cours de votre mission, à collaborer avec l'ensemble des membres de l'équipe.

Les atouts en nous rejoignant

· Environnement collaboratif et innovant

· Collaboration internationale

· Diversité des technologies, produits et solutions

· Apprentissage au sein d'une équipe experte

· Engagement en faveur de la diversité et de l'inclusion