Exercices corrigés de Logique et solveurs SAT
Ces 23 exercices accompagnent le cours de Logique et solveurs SAT 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.
Logique propositionnelle2 exercices
Compter les modèles d'une formule, et ce que l'implication ne dit pas.
Le cours : Logique propositionnelle et satisfiabilité
Les cas faciles2 exercices
Reconnaître une clause de Horn, et propager jusqu'au bout sans jamais décider.
Le cours : Les cas faciles : 2-SAT, Horn et XOR
CDCL2 exercices
Lire un graphe d'implication, et calculer le niveau de retour.
Le cours : CDCL : l'apprentissage de clauses
Ce qui rend un solveur rapide2 exercices
Les deux littéraux surveillés, et le seul chiffre qui décide de ce qu'il faut optimiser.
Le cours : Les heuristiques d'un solveur moderne
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 : NP-complétude et 3-SAT
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.
Les notions ci-dessus sont enseignées dans le cours de Logique et solveurs SAT, chapitre par chapitre. Les autres parcours sont dans les exercices corrigés.