v2.11.0 (5354)

Cours scientifiques - IA303 : Résolution efficace des modèles logiques

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

24 heures en présentiel

effectifs minimal / maximal:

10/30

Diplô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 20

Littérale/grade européen

Pour 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
L'UE est acquise si Note finale >= 10
  • Crédits ECTS acquis : 2 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

Mots clés

procédures de décision, SAT, SMT
Veuillez patienter