Satisfiabilité booléenne
De la logique propositionnelle aux solveurs CDCL : modéliser un problème en clauses, et comprendre comment une machine le résout.
10 chapitres
Parcours pas encore commencé.
- 1.Logique propositionnelle et satisfiabilité
- 2.Forme normale conjonctive et transformation de Tseitin
- 3.Modéliser un problème en SAT
- 4.Ce que « difficile » veut dire
- 5.Les cas où la difficulté disparaît
- 6.La résolution, ou comment prouver qu'il n'y a rien
- 7.DPLL : chercher, et savoir revenir en arrière
- 8.CDCL : apprendre de ses échecs
- 9.Ce qui fait tourner un solveur moderne
- 10.Un problème complet, du français au graphique