| 9/09/2014 | Overview Problems in NP Example: tiling problem Algorithm of the form search/verify Abstraction of the "search" part: non-determinism NP Propositional logic Syntax Semantics Reduction to SAT |
| 16/09/2014 | TP1 : installer zchaff, étudier le parseur cnf fourni, programmer un sat solveur naif (avec récursivité), discussion sur la mise en place d?une procédure de test A faire pour la fois suivante : finir le solveur (chacun fait le sien), avancer sur la procédure de test (un binôme seulement), proposer un front-end de coloration de graphe (un binôme seulement) |
| 22/09/2014 |
Normal forms (presented by a student)
Tseitsin transformation (presented by a student)
DPLL algorithm
Recursive version
Backtracking made explicit
|
| 30/09/2014 | TP2 : discussions sur le code de chacun (besoin d?abstraire davantage), discussion sur l?avancement de la procédure de test et du front-end, programmer un sat solveur avec backtrack explicite et propagation unitaire A faire pour la fois suivante : finir la procédure de test et le front-end, terminer le nouveau sat solveur en tenant compte des conseils sur le style de programmation |
| 7/10/2014 | Backjumping and learning Demonstration of DPLL algorithm with backjumping and learning Proofs: soundness, completeness, terminaison |
| 14/10/2014 | TP3 : chacun présente son code au reste du groupe - discussion A faire pour la fois suivante : tester le sat solveur avec la nouvelle procédure de test - ajouter des optims (learning ou 2-watch literal) |
| 21/10/2014 |
DPLL modulo theory
Fourier Motzkin (presented by a student)
Omega test
Integer linear programming
Panorama about reasoning about numbers
DPLL(T): the global architecture
|
| 4/11/2014 | TP4 : le développement devient collaboratif uniquement - discussion sur l?architecture d?un petit SMT solveur (comment tester les sous-modules, répartition des charges, planning) |
| 18/11/2014 |
Uninterpreted functions and equality: congruence closure (presented by a student)
Combine theories
Discussion about theories
Craig's interpolation
Non-deterministic algorithm (Nelson-Oppen)
|
| 25/11/2014 | TP5 : discussion sur l'avancement du SMT |
| 2/12/2014 |
Proof of Nelson-Oppen, pinpointed that we assume theories to be stably infinite (presented by a student)
Deterministic algorithm for convex theories (Nelson-Oppen)
|
| 11/12/2014, 10h15, I51 | Examen sur table : sujet |
| 19/12/2014, 14h | TP6 : présentation oral du projet |