Logique et satisfiabilité (SAT)
Écrire un problème sous forme de clauses logiques et le confier à un solveur SAT, puis comprendre comment ce solveur cherche sa solution.
10 chapitresExercices corrigés du parcours
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.NP-complétude et 3-SAT
S'appuie sur : ch. 8, Complexité algorithmique et Green IT (Mathématiques appliquées)
- 5.Les cas faciles : 2-SAT, Horn et XOR
- 6.La résolution et les preuves d'insatisfiabilité
- 7.DPLL : chercher, et savoir revenir en arrière
S'appuie sur : ch. 9, La récursivité (Algorithmique)
- 8.CDCL : l'apprentissage de clauses
- 9.Les heuristiques d'un solveur moderne
- 10.Projet : modéliser et résoudre un problème complet