Année 2019-2020

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

Nov. 12, 2019: Propositional logic
- Les transparents du cours
- Le sujet de TP
Nov. 26, 2019: SAT solver algorithms
- Les transparents transparents du cours
- Le sujet de TP sujet de TP
Dec. 10, 2019: First-order theories and SMT solver algorithms
- Les transparents
- Le sujet de TP
Dec. 17, 2019: Theory of uninterpreted functions
- Les transparents transparents du cours
- Le sujet de TP
Dec. 07, 2019: Theory of linear real expressions
- Les transparents transparents du cours
- Le sujet de TP
Jan. 07, 2020: Theory of nonlinear real expressions
- Les transparents
- Le sujet de TP
Jan. 07, 2020: Combination of theories
- Les transparents
- Le sujet de TP
Jan. 21, 2020: Exam

Evaluation du cours

Le cours sera évaluer par deux activités

Programmer un solveur SAT fondé sur la méthode DPLL
Lire, résumer et présenter un article scientifiques

Projet de programmation

Le texte du sujet

La date du rendu est fixée au mardi 17 décembre 2019 à 13h

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

Lecture d’articles scientifiques

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.

Le travail est à réaliser en binôme
La présentation durera 10 minutes et sera suivie de 5-8 minutes de questions.
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 17 décembre 2019

La date de présentation est fixée à la dernière séance de cours, c’est-à-dire le mardi 21 janvier 2020 matin.
Le résumé est à rendre avant le vendredi 17 janvier 2020 miniuit.

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:

Une ou deux pharses de résumé de l’article
Une description détaillée des points principaux développés dans l’article comme les hypothèses fixées, les arguments en faveur des idées développées, un regard critique sur les données expérimentales, les conclusions de l’article.
Une discussion sur les limites, ou les possibles extensions des idées développées dans l’article.
Un avis argumenté sur l’article, par exemple, la qualité des idées développées et les impacts de celles-ci dans le domaine concerné.

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: Liste des binômes et des articles

DHIF Mohamed et KAMMOUN Mohamed Ali : A-SAT-Based-Algorithm-for-Context-Matching.pdf
BENYOUSSEF Manel et IDOUDI Houssine : Checking-Safety-Properties-Using-Induction-and-a-SAT-Solver.pdf
KAMINSKYI Nazar-Mykola et MAVLIUTOV Yaroslav : Constrained-Image-Generation-Using-Binarized-Neural-Networks-with-Decision-Procedures.pdf
HICKSON Lorraine et MENTEC Inès : efficient-haplotype-inference-with-boolean-satisfiability.pdf
DAMPEYROU Charles et GORCE Valentin : Enhancing-SAT-Based-Planning-with-Landmark-Knowledge.pdf
SAINT MÉZARD Marine et TURC Etienne : incremental-task-and-motion-planning-a-constraint-based-pproach.pdf
QUEYRUT Simon et ZHOU Zhi : Mapping-Ontologies-using-SAT-Solvers.pdf
CHIHI Mohamed Amine et OUERTATANI Houssem : ReaS-Combining-Numerical-Optimization-with-SAT-Solving.pdf
BOETTO Christophe et CHEN Hao : reluplex-an-eefficient-smt-solver-for-verifying-deep-neural-networks.pdf
COLLERY Benjamin et FAUCHEREAU Clément : SATNet-bridging-deep-learning-and-logical-reasoning-using-a-differentiable-satisfiability-solver.pdf
BOUZAIENE Maha et SAFFAR Mohamed Sary : SMT-solvers-for-software-security.pdf
BALLESTEROS LOPEZ Mónica Belén et LOPEZ LOPEZ Camilo : planning-as-satisfability.pdf
JOURNÉ Arthur et RÉROLLE Pierre-Louis : Scalable-Motion-Planning-using-Lazy-SMT-Based
ORTEGON MEJIA Julio Andres Felipe : smt-based-architecture-modelling-for-safety-assessment.pdf
BAPTISTE Jahmal et SAY Bunthet : towards-CLIPS-based-Task-Execution-and-Monitoring-with-SMT-based-Planning-and-Optimization.pdf