Cours

Informations pratiques

• Des exercices seront proposés pendant le cours Satisfaisabilité (SAT) et Satisfaisabilité Modulo Théories(SMT). Pour les faire, tout portable avec Python 3 installé convient.
• Pour le cours sur Sage, un portable est nécessaire si vous voulez suivre  les exemples. Vous pouvez aussi installer Sage en suivant les instructions ci-jointes.

************************************

Géométrie Numérique

Bruno Lévy (DR INRIA, LORIA), Dmitry Sokolov (MCF, LORIA), Nicolas Ray (CR INRIA, LORIA)

Ce cours traite de plusieurs manières pour représenter et manipuler des formes en 3D dans un ordinateur. Avec l'évolution des moyens d'acquisition, de fabrication et de calcul, la simulation numérique joue un rôle de plus en plus important dans les sciences et dans l'industrie, que ça soit pour simuler et comprendre des phénomènes physiques, ou encore pour concevoir et prédire le comportement d'un objet industriel. La représentation 3D sous-jacente est un point crucial de ces simulations numériques.

Nous aborderons dans ce cours les fondements géométriques utilisés par les maillages, l'une des représentations 3D la plus largement utilisée. Nous verrons ensuite un ensemble d'algorithmes permettant de construire, de transformer et d'optimiser ces maillages, tels que le lissage et la paramétrisation, fondés sur des méthodes numériques. En pratique, ceci revient à la fin à poser des problèmes de type moindres carrés et à résoudre de grands systèmes linéaires creux, pour lesquels nous présenterons plusieurs algorithmes classiques de résolution numérique. Enfin, nous présenterons une introduction au transport optimal permettant de mesurer des distances et d'interpoler dans une classe très générale d'objets (des mesures de probabilités), très bien adaptée à une représentation discrète sur ordinateur. Nous aborderons ensuite les avancées récentes dans les algorithmes numériques permettant de calculer le transport optimal, trouvant des applications en analyse des données, en modélisation 3D, en apprentissage machine et en simulation numérique.

L'ensemble des méthodes présentées dans le cours sera illustré par des logiciels et bibliothèques (la plupart en C++, quelques uns en Python), tous disponibles en open-soure.

---------------------------------------------------

Calcul mathématique avec Sage

Vincent Delecroix (CR CNRS, LABRI)

SageMath (ou Sage) est un logiciel de mathématiques générales. C'est un logiciel libre développé par plus d'une centaine de personnes autour de la planète. Après une brève présentation générale du projet et une prise en main sur machine nous proposerons des TPs en rapport avec les autres cours de l'école. Voir les TP's

 ---------------------------------------------------

Satisfaisabilité (SAT) et Satisfaisabilité Modulo Théories (SMT)

Pascal Fontaine (MCF, LORIA), Sylvain Conchon (PR, LRI), Laurent Simon (PR, LaBRI)

Le cours est en deux parties, la première étant axée sur les solveurs SAT (satisfaisabilité propositionnelle), la seconde sur les solveurs SMT (satisfaisabilité modulo théories).

Nous présenterons d'abord les éléments clés de ce qui compose les “Solveurs SAT Modernes”. Après une introduction historique sur la quête de la résolution pratique du problème NP-Complet canonique “SAT”, nous expliquerons, en nous appuyant sur une implantation en Python reprenant les caractéristiques algorithmiques et les structures de données des solveurs CDCL (Conflict Driven Clause Learning), les points essentiels devant être intégrés à ces solveurs. Des exercices illustrant leur fonctionnement seront mis en place autour de la résolution de problèmes de Sudoku. Pour aller plus loin, nous utiliserons l’API fournie par le programme Python pour créer un générateur de Sudoku. Comme nous le verrons, l’encodage SAT posera rapidement des problèmes de mémoire dès lors que l’on voudra augmenter la taille des puzzles considérés. En guise d’illustration et comme transition vers la deuxième partie sur SMT, nous présenterons une extension sous forme de SMT du programme SAT permettant de prendre en compte des contraintes natives.

À l'instar des solveurs SAT, les solveurs SMT sont de plus en plus utilisés, dans l’avionique, la biologie en passant par les réseaux, l’automobile ou le ferroviaire, par l’industrie du

hardware ou du software, à tel point que l’on parle aujourd’hui d’une révolution SMT. Bénéficiant des progrès extraordinaires réalisés ces dernières années par les solveurs SAT sur lesquels ils sont basés, les démonstrateurs SMT permettent de décider de la satisfaisabilité de formules logiques contenant des symboles de théories particulières. Nous tenterons dans cette seconde partie de faire découvrir les principaux concepts sous-jacents à la conception et l’implémentation de tels solveurs. Les trois thèmes/questions suivants seront abordés :

1. Quelles théories utilise-t-on en pratique et quelles sont les procédures de décision qui leur sont associées ?

2. Comment combiner ces théories (ou procédures) entre elles et avec un solveur SAT ?

3. Comment étendre cette technique à des formules avec quantificateurs ?

Nous conclurons le cours par des exemples d'application, nous verrons les défis attendant les communautés SAT et SMT dans les années à venir. Cela motivera les échanges questions-réponses qui termineront ce cours.

 ---------------------------------------------------

Analyses statiques des réseaux booléens pour la biologie systémique

Loïc Paulevé (CR CNRS, LRI), Adrien Richard (CR CNRS, I3S)

Un réseau booléen regroupe un ensemble fini de variables booléennes, associées à une fonction de transition. Ce formalisme est particulièrement utilisé pour modéliser la dynamique qualitative des réseaux biologiques, rendant compte des circuits d'influences positives ou négatives entre l'activité des gènes et des protéines.

Ce cours détaillera deux aspects de l'analyse statique des réseaux booléens :

• le lien entre les propriétés du /graphe d'influence/ d'un réseau booléen et son nombre de points fixes et cycles limites, et leur temps d'atteinte ;

• l'interprétation abstraite de la dynamique des réseaux booléens, et son application pour la prédiction de cibles pour le contrôle de propriétés d'accessibilité.

 ---------------------------------------------------

Couplage probabiliste et combinatoire

Philippe Chassaing (PR, IECL), Irène Marcovici (MCF, IECL)

Dans ce cours il s'agira, sur des exemples souvent issus de la combinatoire et de l'informatique, de passer en revue diverses méthodes de couplage probabiliste. On s'attardera en particulier sur quelques avancées des années 2000 ou plus récentes, concernant les arbres, graphes et permutations, où une approche probabiliste élémentaire éclaire des calculs combinatoires ardus, à travers une représentation probabiliste inattendue d'objets combinatoires pris dans la liste suivante : hachage et fonctions de parking, nombres d'Euler et permutations, arbre binaire de recherche et processus de branchements de Yule, arbre couvrant minimal et graphes aléatoires, factorisation des mots, automates cellulaires, permutations à motifs exclus.

---------------------------------------------------

Comment candidater aux postes académiques ?

Simon Perdrix (CR CNRS, LORIA)

Après une thèse, le monde académique offre plusieurs métiers : enseignant-chercheur, chercheur, mais aussi ingénieur de recherche, enseignement en lycée et collège, classes préparatoires, … Chacun de ces concours a son propre calendrier, ses spécificités, ses prérequis. L'exposé donnera quelques conseils aux futurs candidats, pour la rédaction du dossier, les auditions, le contact avec les postes visés. Il expliquera ce qui distingue les différents concours (CNRS, Inria, MdC). On discutera également de la question de la parité et de l'égalité des chances, et de comment valoriser un parcours atypique.