Exercices SAT
Exercice 1
- Se familiariser avec la syntaxe DIMACS des formules CNF.
- Tester le solveur Minisat
exécutable dans un navigateur
sur les formules booléennes de l'exercice 2 cette fiche (les exercices 3, 4 et 5 permettront de tester Minisat sur des formules
de plus grande taille).
Exercice 2
- Appliquer à la main un algorithme polynomial
(cf. Wikipedia
ou bien 2SAT (Muli Safra))
pour déterminer la satisfiabilité des formules suivantes :
(x ∨ y) ∧ (x ∨ ¬ z) ∧ (¬ x ∨ y) ∧ (y ∨ z)(x ∨ y) ∧ (z ∨ ¬ t) ∧ (x ∨ t) ∧ (x ∨ z) ∧ (¬ y ∨ t)(¬ x ∨ y) ∧ (¬ y ∨ z) ∧ (¬ z ∨ x)(¬ x ∨ y) ∧ (¬ y ∨ z) ∧ (¬ z ∨ x) ∧ (x ∨ y) ∧ (¬ y ∨ ¬ z)
-
Ecrire un programme de complexité polynomiale (langage au choix) résolvant 2-SAT.
Exercice 3
Le principe des tiroirs
est un test classique pour un solveur propositionnel car le nombre d'étapes
pour la résolution propositionnelle
est exponentielle en fonction du nombre de chaussettes.
Modéliser (voir par exemple ce document, pigeon = chaussette, nid = tiroir)
et résoudre via Minisat pour (2,2), (3,2) pigeons/nids. Benchmarker Minisat pour (n,n) et (n+1,n) pigeons/nids
avec n variant de 5 à 10 et représenter graphiquement les temps de calcul (en ordonnée) relativement à n (en abcisse).
Exercice 4
Résoudre à l'aide de Minisat le problème du coloriage de cartes.
Exercice 5
Résoudre à l'aide de Minisat le problème des n-reines.