Descriptif
L’objectif de cet enseignement est de présenter les algorithmes actuels de résolution (satisfiabilité ou non-satisfiabilité) de formules de logiques booléennes modélisant différents problèmes comme la planification de chemins, la planification de tâches, diagnostique. En particulier, l’algorithme DPLL, et son extension CDCL, seront présentés dans une première partie du cours pour résoudre des problèmes purement booléens. Ensuite, les extensions de formule de logiques avec des termes venant d’autres théories (expressions linéaires en nombres entiers, en nombres réels, ou expressions non-linéaires ou tableaux), qui sont à l’origine des techniques SMT (SAT Modulo Théories), seront présentées. Cette seconde partie permettra de faire le lien entre les algorithmes CDCL et les algorithmes classiques de programmation par contraintes ou de programmation mathématique. Cet enseignement permettra de montrer comment des problèmes de décision complexes peuvent être résolus efficacement avec des techniques exploratoires.
Objectifs pédagogiques
- Savoir modéliser des problèmes de décision à l’aide de formules logiques combinées avec d’autres théories.
- Connaître les algorithmes de résolution de problèmes SAT/SMT
effectifs minimal / maximal:
10/30Diplôme(s) concerné(s)
Pour les étudiants du diplôme Diplôme d'Ingénieur de l'Ecole Nationale Supérieure de Techniques Avancées
Aucun pré-requis
Format des notes
Numérique sur 20Littérale/grade européenPour les étudiants du diplôme Diplôme d'Ingénieur de l'Ecole Nationale Supérieure de Techniques Avancées
Vos modalités d'acquisition :
Présentation orale d'articles scientifiques
Le rattrapage est autorisé (Max entre les deux notes écrêté à une note seuil)- le rattrapage est obligatoire si :
- Note initiale < 6
- le rattrapage peut être demandé par l'étudiant si :
- 6 ≤ note initiale < 10
- Crédits ECTS acquis : 1.5 ECTS
Le coefficient de l'UE est : 1
La note obtenue rentre dans le calcul de votre GPA.
L'UE est évaluée par les étudiants.
Programme détaillé
Séance 1 : Logique propositionnelle et logique des prédicats
Séance 2 : Algorithmes de résolutions des problèmes SAT
Séance 3 : Théories du premier ordre et moteur SMT
Séance 4 : Théorie des fonctions non interprétées et de l'égalité
Séance 5 : Théorie des expressions linéaires réelles non quantifiées
Séance 6 : Théorie des expressions non-linéaires non quantifiées
Séance 7 : Combinaison de théorie
Séance 8 : examen