Utilisation d'un solver (minisat)
minisat est un solveur de formules SAT en ligne de commande : on lui donne une formule sous forme d'un fichier texte et il tente de déterminer si la formule est satisfiable et, si oui, pour quelles valeurs de variables.
Pour pouvoir utiliser minisat, veuillez utiliser Binder (cliquer sur le titre du TP) ou installer minisat sur votre machine (si vous avez OCaml)
Fichier dimacs cnf¶
Imaginons que l'on souhaite savoir si la formule suivante est satisfiable : $$(x_1 \lor x_2 \lor x_3) \land (x_1 \lor \lnot x_2) \land (x_2 \lor \lnot x_3) \land (\lnot x_2 \lor \lnot x_3 \lor \lnot x_1) $$
On encode pour cela la formule dans un fichier au format DIMACS CNF (test.cnf dans cet exemple) :
p cnf 3 4
1 2 3 0
1 -2 0
2 -3 0
-1 -2 -3 0p cnf 3 4 signifie que la formule est en CNF, qu'elle comporte $3$ variables et $4$ clauses.
Chacune des lignes suivantes correspond à une clause, où un nombre positif correspond à une variable et un nombre négatif à sa négation. $0$ indique la fin d'une ligne.
Puis on appelle minisat sur le fichier, ce qui produit un fichier de sortie nommé ici test.out :
Sys.command "minisat test.cnf test.out; cat test.out"
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 3 | | Number of clauses: 4 | | Parse time: 0.00 s | | Eliminated clauses: 0.00 Mb | | Simplification time: 0.00 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== =============================================================================== restarts : 1 conflicts : 0 (-nan /sec) decisions : 1 (0.00 % random) (inf /sec) propagations : 2 (inf /sec) conflict literals : 0 (-nan % deleted) Memory used : 11.00 MB CPU time : 0 s SATISFIABLE SAT 1 -2 -3 0
- : int = 0
minisat a donc trouvé que la formule est satisfiable avec comme assignation :
$$v(x_1) = 1, ~v(x_2) = 0, ~v(x_3) = 0$$
Écriture et lecture dans un fichier en OCaml¶
Il est pratique d'utiliser un langage de programmation pour générer un fichier .cnf correspondant à une grosse formule.
L'écriture et la lecture dans un fichier en OCaml se fait à travers un channel.
open_out donne un channel pour pouvoir écrire dans un fichier :
let f = open_out "test" (* ouvre un fichier test en écriture *)
val f : out_channel = <abstr>
Printf.fprintf est une fonction ressemblant à la fonction printf en C et permettant d'écrire sur un channel (et notamment dans un fichier) :
Printf.fprintf f "blabla\n" (* écrit blabla dans le fichier, puis un saut de ligne *)
- : unit = ()
Comme pour printf, on peut écrire le contenu de variables en utilisant %d (pour un entier), %s (pour une string)... :
let x = 2 in
let text = "abc" in
Printf.fprintf f "%s %d" text x; (* écrit "abc 2" dans le fichier *)
- : unit = ()
Quand la modification du fichier est terminée, on peut flush (forcer l'écriture du texte) et fermer le channel :
flush f;
close_out f
- : unit = ()
Exercice
Vérifier le contenu du fichier test sur Jupyter (en allant dans le même dossier que ce notebook).
Pour avoir plus d'informations sur l'écriture et la lecture, regarder https://ocaml.org/docs/file-manipulation.
Vous aurez besoin de lire dans un fichier pour afficher proprement la solution des exercices suivants.
Voici une fonction pour afficher le contenu d'un fichier :
let print_file file =
let f = open_in file in
try while true do
print_endline (input_line f)
done
with _ -> ();;
print_file "test"
val print_file : string -> unit = <fun>
blablaabc 2
- : unit = ()
Problème des 8 dames¶
On considère un échiquier $n\times n$ et on souhaite y placer $n$ dames dessus sans qu'elles ne puissent se prendrent l'une l'autre (c'est-à-dire qu'il n'y a pas deux dames sur la même ligne, colonne ou diagonale).
Exercice
- Écrire une fonction
dames npour écrire dans un fichier une formule SAT sous forme CNF pour résoudre ce problème. Pour cela, on pourra utiliser une variable booléenne pour chaque case et encoder les contraintes suivantes :
- Pour chaque ligne, il y a au moins une dame.
- Pour tout $p = (i_1, j_1) \neq q = (i_2, j_2)$, si $p$ et $q$ sont sur la même ligne, colonne ou diagonale, alors $p$ ou $q$ est faux.
- Résoudre le problème avec minisat.
- Lire dans le fichier solution et l'afficher graphiquement.
Solution
let dames n =
let f = open_out "dames.cnf" in
let endl () = Printf.fprintf f "0\n" in
Printf.fprintf f "p cnf 0 0\n";
for i = 0 to n - 1 do
for j = 1 to n do Printf.fprintf f "%d " (i*n + j) done;
endl ();
done;
for i1 = 0 to n - 1 do
for j1 = 1 to n do
for i2 = 0 to n - 1 do
for j2 = 1 to n do
if (i1, j1) <> (i2, j2) &&
(i1 = i2 || j1 = j2 || abs (i1 - i2) = abs (j1 - j2))
then Printf.fprintf f "-%d -%d 0\n" (i1*n + j1) (i2*n + j2);
done
done
done
done;
flush f;
close_out f;;
dames 40;
Sys.command "minisat dames.cnf dames.out";;
(*print_file "dames.out"*)
val dames : int -> unit = <fun>
WARNING! DIMACS header mismatch: wrong number of variables. WARNING! DIMACS header mismatch: wrong number of clauses.
WARNING: for repeatability, setting FPU to use double precision ============================[ Problem Statistics ]============================= | | | Number of variables: 1600 | | Number of clauses: 207000 | | Parse time: 0.02 s | | Simplification time: 0.07 s | | | ============================[ Search Statistics ]============================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Limit Clauses Lit/Cl | | =============================================================================== | 100 | 1600 103520 208560 | 37957 100 184 | 0.000 % | =============================================================================== restarts : 3 conflicts : 223 (2373 /sec) decisions : 2010 (0.00 % random) (21389 /sec) propagations : 13049 (138861 /sec) conflict literals : 49491 (0.70 % deleted) Memory used : 20.00 MB CPU time : 0.093972 s SATISFIABLE
- : int = 10
Solution
let get_vars file =
let f = open_in file in
let _ = input_line f in
input_line f
|> String.split_on_char ' '
|> List.map int_of_string
|> List.filter ((<) 0) in
let print_sol n vars =
for i = 0 to n - 1 do
for j = 1 to n do
if List.mem (i*n + j) vars then Format.printf "||"
else Format.printf ".."
done;
Format.printf "\n"
done;
Format.printf "@." in
get_vars "dames.out" |> print_sol 40
........................................................................||...... ............................||.................................................. ....||.......................................................................... ..............................................................||................ ..........................................||.................................... ........||...................................................................... ..................................................||............................ ............................................||.................................. ..............................||................................................ ..........................||.................................................... ........................................||...................................... ................................||.............................................. ..........||.................................................................... ......................................||........................................ ..............................................................................|| ......................||........................................................ ............................................................................||.. ......................................................................||........ ....................||.......................................................... ......................................................||........................ ||.............................................................................. ..........................................................................||.... ..................................................................||............ ..||............................................................................ ....................................||.......................................... ....................................................................||.......... ..............................................||................................ ..........................................................||.................... ........................||...................................................... ................||.............................................................. ..................................||............................................ ..............||................................................................ ..................||............................................................ ................................................||.............................. ................................................................||.............. ............................................................||.................. ......||........................................................................ ............||.................................................................. ....................................................||.......................... ........................................................||......................
- : unit = ()
3-coloration¶
Exercice
Faire de même pour résoudre le problème de $3$-coloration d'un graphe (transformer un graphe - sous forme de liste d'adjacence, par exemple - en formule SAT qui soit satisfiable si et seulement si le graphe est $3$-coloriable. Vérifier sur des exemples.