Exemple d'application pour un solver SAT¶
Pour chaque case inconnue, on définit une variable booléenne
V ssi la case est minée
Quelles sont les contraintes du plateau ?¶
Pour chaque case de la bordure, on a une contrainte sur les variables
Exemple :
$(x_0 \land \neg x_1) \lor (x_1 \land \neg x_0)$¶
Le plateau correspond une formule qui doit être satisfiable
- c'est la conjonction des formules exprimant les contraintes pour chaque case
- assez facile à exprimer à l'aide d'un algorithme
- on obtient ...
let bigformula = Et (Ou (Et (Var "X1" , Non(Var "X0")) , Et (Var "X0" , Non(Var "X1"))) , Et (Ou (Et (Et (Var "X3" , Var "X2") , Non(Var "X1")) , Ou (Et (Et (Var "X3" , Var "X1") , Non(Var "X2")) , Et (Et (Var "X2" , Var "X1") , Non(Var "X3")))) , Et (Ou (Ou (Et (Var "X4" , Et (Non(Var "X3") , Non(Var "X2"))) , Et (Var "X3" , Et (Non(Var "X4") , Non(Var "X2")))) , Et (Var "X2" , Et (Non(Var "X4") , Non(Var "X3")))) , Et (Ou (Ou (Ou (Et (Et (Var "X7" , Var "X6") , Et (Non(Var "X5") , Et (Non(Var "X4") , Non(Var "X3")))) , Ou (Et (Et (Var "X7" , Var "X5") , Et (Non(Var "X6") , Et (Non(Var "X4") , Non(Var "X3")))) , Et (Et (Var "X6" , Var "X5") , Et (Non(Var "X7") , Et (Non(Var "X4") , Non(Var "X3")))))) , Ou (Ou (Et (Et (Var "X7" , Var "X4") , Et (Non(Var "X6") , Et (Non(Var "X5") , Non(Var "X3")))) , Et (Et (Var "X6" , Var "X4") , Et (Non(Var "X7") , Et (Non(Var "X5") , Non(Var "X3"))))) , Et (Et (Var "X5" , Var "X4") , Et (Non(Var "X7") , Et (Non(Var "X6") , Non(Var "X3")))))) , Ou (Ou (Ou (Et (Et (Var "X7" , Var "X3") , Et (Non(Var "X6") , Et (Non(Var "X5") , Non(Var "X4")))) , Et (Et (Var "X6" , Var "X3") , Et (Non(Var "X7") , Et (Non(Var "X5") , Non(Var "X4"))))) , Et (Et (Var "X5" , Var "X3") , Et (Non(Var "X7") , Et (Non(Var "X6") , Non(Var "X4"))))) , Et (Et (Var "X4" , Var "X3") , Et (Non(Var "X7") , Et (Non(Var "X6") , Non(Var "X5")))))) , Et (Ou (Ou (Et (Var "X8" , Et (Non(Var "X7") , Non(Var "X6"))) , Et (Var "X7" , Et (Non(Var "X8") , Non(Var "X6")))) , Et (Var "X6" , Et (Non(Var "X8") , Non(Var "X7")))) , Et (Ou (Ou (Et (Var "X9" , Et (Non(Var "X8") , Non(Var "X7"))) , Et (Var "X8" , Et (Non(Var "X9") , Non(Var "X7")))) , Et (Var "X7" , Et (Non(Var "X9") , Non(Var "X8")))) , Et (Ou (Ou (Et (Var "X13" , Et (Non(Var "X12") , Non(Var "X11"))) , Et (Var "X12" , Et (Non(Var "X13") , Non(Var "X11")))) , Et (Var "X11" , Et (Non(Var "X13") , Non(Var "X12")))) , Et (Ou (Et (Et (Var "X14" , Var "X13") , Non(Var "X12")) , Ou (Et (Et (Var "X14" , Var "X12") , Non(Var "X13")) , Et (Et (Var "X13" , Var "X12") , Non(Var "X14")))) , Et (Ou (Et (Et (Var "X15" , Var "X14") , Non(Var "X13")) , Ou (Et (Et (Var "X15" , Var "X13") , Non(Var "X14")) , Et (Et (Var "X14" , Var "X13") , Non(Var "X15")))) , Ou (Et (Var "X15" , Non(Var "X14")) , Et (Var "X14" , Non(Var "X15"))))))))))));
On cherche les modèles de la formule (par exemple avec la variante de l'algo de Quine)
modeles bigformula;
Conclusion ?
