Établissement
INP - ENSEEIHT
Description
La matière gravite autour de plusieurs cours visant à introduire différentes techniques et outils formels pour la modélisation de problèmes (programmation
logique, réseaux de contraintes, problèmes SAT/SMT), ainsi que pour leur résolution automatique (système résolution + branch-and-bound/branch-and-prune,
arbres de décision, réduction de symétries...).
La théorie abordée en cours est mise en pratique au travers de divers TP, introduisant des technologies comme Prolog (programmation logique) et Z3
(solveur SAT/SMT), et amenant les étudiants à modéliser des problèmes divers (problèmes combinatoires, problèmes d'opitimization en variables entières,
résolution de sudoku, synthèse d'expressions arithmétiques...).
Les compétences relatives à cette matière sont validées par une bureau d'étude (TP noté) qui recouvre l'ensemble des connaissances et techniques abordées au
fil des cours et des TP.