Exercices corrigés de Satisfiabilité booléenne
Ces 15 exercices accompagnent le cours de Satisfiabilité booléenne et suivent son ordre, notion par notion. Chacun se corrige dans la page, au clic : pas de compte à créer, pas de fichier à rendre, et la correction dit ce qui ne va pas plutôt que de donner une note.
Ce que difficile veut dire3 exercices
Vérifier n'est pas trouver, le rapport clauses sur variables, et le sens d'une réduction.
Le cours : Ce que « difficile » veut dire
DPLL3 exercices
Dérouler une trace, distinguer propager de décider, et le coût d'une réfutation.
Forme normale conjonctive3 exercices
Descendre une négation, repérer les littéraux purs et les clauses inutiles.
Le cours : Forme normale conjonctive et transformation de Tseitin
Modéliser en SAT3 exercices
Traduire « au moins un » et « au plus un », et en chiffrer le coût.
Le cours : Modéliser un problème en SAT
Résolution et propagation3 exercices
Produire un résolvant, propager une clause unitaire, simplifier une formule.
Le cours : La résolution, ou comment prouver qu'il n'y a rien
Les notions ci-dessus sont enseignées dans le cours de Satisfiabilité booléenne, chapitre par chapitre. Les autres parcours sont dans les exercices corrigés.