M1 Jacques Herbrand

Course : Logical Aspects of AI

Year : 2019 - 2020

Part 1 : SAT / SMT

Lecture slides

Reading materials

Practice : a SAT-based Sudoku Solver

Following the paper of Tjark Weber for a SAT-based Sudoku solver, implement your own CDCL SAT solver and use it to solve Sudoku puzzles.

Send the sources of your program to sylvain.conchon@lri.fr in a Unix (compressed) archive name.tgz. Your archive must also include a README file describing how to compile and run your Sudoku solver. It must also include a (short) report (2 pages max.) describing the salient parts of your code.

Décodage des grilles de Sudoku

Chaque ligne du fichier correspond à une grille de Sudoku. Les grilles sont simplement codées à l'aide de 81 caractères qui correspondent aux valeurs initiales des cases. Les premiers 9 caractères correspondent à la première ligne de la grille, les 9 suivants à la deuxième ligne etc.

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 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).

Utilisation du solveur minisat

Le solveur SAT minisat prend en entrée un fichier contenant une formule en FNC. Cette formule est décrite dans un format très simple appelé Dimacs.

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 0
Les 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.dimacs
Si 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_solution
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 0
La 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).