Course : Logical Aspects of AI
Year : 2019 - 2020
Part 1 : SAT / SMT
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.
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).
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).