| 8 septembre 2015 |
Classes de complexitéNP Example: tiling problem Algorithm of the form search/verify Abstraction of the "search" part: non-determinism NP tiling problem is NP-hard Comment encoder l'exécution d'une machine de Turing comme le pavage d'un rectangle SAT Réduction à SAT Théorème de Cook Rappel des formes normales PSPACE Définition de PSPACE et NPSPACE Example: corridor tiling problem corridor tiling problem is NPSPACE-dur |
| 15 septembre 2015 | TP : 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 septembre 2015 | PSPACE (suite) Quantified binary formula (QBF) QBF is in PSPACE QBF is NPSPACE-dur Théorème de Savitch : PSPACE = NPSPACE Pourquoi on peut se restreindre aux CNF: Tseitin transformation (presented by a student) Document pour préparer la présentation |
| 29 septembre 2015 | DPLL, backtracking et backjumping Recursive version Backtracking made explicit Version avec backjumping Demonstration of DPLL algorithm with backjumping and learning Proofs: soundness, completeness Terminaison (non faite) Document qui donne la preuve de terminaison |
| 6 octobre 2015 | TP : Discussion sur l'architecture |
| 13 octobre 2015 |
Rappel sur la logique du premier ordre
Arithmétique linéaire sur les réels
Fourier Motzkin
Combiner SAT et Fourier Motzkin
Panorama about reasoning about numbers
Théorie des réels
|
| 20 octobre 2015 | 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) |
| VACANCES (pas de séances le 27 octobre) | |
| 3 novembre 2015 |
Uninterpreted functions and equality: congruence closure (presented by a student)
Combine theories
Discussion about theories
Craig's interpolation
Non-deterministic algorithm (Nelson-Oppen)
|
| mardi 10 novembre 2015 |
Proof of Nelson-Oppen, pinpointed that we assume theories to be stably infinite (presented by a student)
Deterministic algorithm for convex theories (Nelson-Oppen)
|
| mardi 17 novembre 2015 | 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) |
| mardi 24 novembre 2015 | TP5 : discussion sur l'avancement du SMT |
| mardi 1 décembre 2015 | TP6 : présentation oral du projet |
| mardi 8 décembre 2015 | Examen sur table |