Année 2018-2019


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.

Enseignant

Alexandre Chapoutot


Supports de cours

  1. Nov. 13, 2018: Propositional logic
  2. Nov. 27, 2018: SAT solver algorithms
  3. Dec. 04, 2018: First-order theories and SMT solver algorithms
  4. Dec. 18, 2018: Theory of uninterpreted functions
  5. Jan. 08, 2019: Theory of linear real expressions
  6. Jan. 08, 2019: Theory of nonlinear real expressions
  7. Jan. 15, 2019: Combination of theories
  8. Jan. 22, 2019: Exam

Evaluation du cours

L’évaluation se fonde sur la rédaction d’un résumé et la présentation d’un article scientifique qui traite des algorithmes SAT/SMT ou de leurs applications dans des domaines variés.

  1. Le travail est à réaliser en binôme

  2. La présentation durera 10 minutes et sera suivie de 5-8 minutes de questions.

  3. Le résumé doit tenir sur une page au format A4 donné au format PDF (rédigé en LaTeX de préférence).

Date des livrables

Le binôme et le choix de l’article sont à définir pour la séance du 11 décembre 2018

Remarques

Un article ne sera attribué qu’une seule fois, c’est-à-dire que tous les binômes auront un article différent à présenter.

Pour le résumé, il est attendu:

Quelques éléments pour bien préparer la présentation

Quelques conseils sur comment lire un article de recherche sont données dans

Remarques pour la présentation: Pour la présentation, l’évaluation prendra en compte la clareté de l’exposé et les éléments montrant la compréhension du sujet. Une répartition équitable du temps de parole ches les binôme est également important!

Evaluation: ordre de passage pour la présentation des articles scientifiques