Une manière de résoudre une grille consiste à encoder le problème comme une formule de la logique propositionnelle de sorte que le puzzle a une solution si et seulement si la formule est satisfiable.
Dans ce projet, on va utiliser dans un premier temps le solveur SAT minisat pour déterminer si une formule est satisfiable. Ensuite, dans un deuxième temps, on réalisera notre propre solveur SAT, dont le fonctionnement sera donné en cours de logique.
Par exemple, la ligne du fichier
790304108000006000000080059030000497000000000217000030470010000000700000302609071
correspond à la grille de Sudoku:
------------- |790|304|108| |000|006|000| |000|080|059| ------------- |030|000|497| |000|000|000| |217|000|030| ------------- |470|010|000| |000|700|000| |302|609|071| -------------Travail à réaliser.
1. Écrire un programme OCaml pour lire le contenu de ce fichier et stocker chaque grille dans une matrice d'entiers.
2. Écrire également un programme pour afficher les grilles (vous pouvez vous inspirer de l'affichage ci-dessus).
Travail à réaliser
3. En vous inspirant de l'encodage décrit dans l'article de Tjark Weber A SAT-based Sudoku Solver, construire, pour chaque grille de Sudoku, une formule propositionnelle en FNC équivalente à la grille.
Vous pourrez par exemple utiliser les types OCaml suivants pour représenter les atomes, les clauses et les formules en FNC :
type cellule = { i : int; j : int }
type atome = { cellule : cellule; d : int; signe : bool }
type clause = atome list
type fnc = clause list
Voici un exemple très simple d'une formule en CNF dans ce format.
c c start with comments c c p cnf 5 3 1 -5 4 0 -1 5 3 4 0 -3 -4 0Les lignes qui commencent pas un c sont des commentaires (vous pouvez donc les ignorer). La ligne p cnf 5 3 indique que le fichier contient une formule en CNF avec au plus 5 variables et 3 clauses. Chaque ligne suivante décrit une clause. Ainsi, la ligne 1 -5 4 0 représente la clause x1 ou (non x5) ou x4, le caractère 0 indique simplement la fin de la ligne.
L'utilisation de minisat est très simple. Pour savoir si la formule en CNF contenu dans un fichier grille.dimacs est satisfiable, il suffit d'exécuter la commande
minisat -verb=0 grille.dimacsSi la formule est satisfiable, minisat affichera simplement SATISFIABLE à l'écran.
Ce solveur peut également renvoyer la valeur des variables propositionnelles qui satisfont la formules en entrée. Pour cela, il suffit d'appeler minisat de la manière suivante:
minisat -verb=0 grille.dimacs fichier_solutionoù fichier_solution est le nom d'un fichier de sortie dans lequel minisat va écrire la solution. Le format de ce fichier de sortie est le suivant
SAT -1 -2 -3 -4 -5 0La première ligne contient uniquement SAT pour indiquer que la formule est satisfiable. La ligne suivante contient la valeur des variables propositionnelles (séparées par un caractère espace).
Travail à réaliser
4. Traduire chaque formule propositionnelle représentant une grille de Sudoku dans un fichier au format Dimacs
5. À l'aide de la fonction de la bibliothèque standard Sys.command : string -> int, appeler minisat pour trouver une solution aux fichiers Dimacs générés, et extraire les solutions des grilles de Sudoku à partir des modèles renvoyés par le solveur.
6. Vérifier que la solution renvoyée pour le solveur SAT est correcte
7. Afficher les solutions des grilles. (vous pouvez simplement utiliser la même fonction que pour afficher les grilles initiales)
Travail à réaliser
8. En suivant les règles présentées dans ce document, programmer un solveur SAT pour déterminer si les formules propositionnelles générées au point 3. sont satisfiables.
9. Utiliser ce solveur SAT pour trouver les solutions aux grilles de Sudoku
10. Vérifier les solutions renvoyées par votre solveur.
11. Afficher ces solutions.