M1 Jacques Herbrand

Course : Logical Aspects of AI

Year : 2019 - 2020

Part 1 : SAT / SMT

Lecture slides

Reading materials

Decision procedures - An algorithmic point of view by Daniel Kroening and Ofer Strichman.
Formalization of DPLL and DPLL Modulo Theories by Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli.
A chapter about SAT/SMT in the book of EJCIM 2018 (in French), by Sylvain Conchon and Laurent Simon.
A persistent Union-Find data structure in OCaml, by Sylvain Conchon and Jean-Christophe Filliâtre.
Some details about the implementation of chaff (in particular, two-watched literals), by Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik.
Heuristics for determining the quality of learning clauses, by Gilles Audemard and Laurent Simon.
Correctness proof of Nelson-Oppen, by Cesare Tinelli and Mehdi Harandi.
Deciding combinations of theories, by Robert Shostak.
About the combination of decision procedures, by Sylvain Conchon and Sava Krstic.
A Model-Constructing Satisfiability Calculus, by Leonardo de Moura and Dejan Jovanovic.
Delayed theory combination, by Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio and Roberto Sebastiani.
Splitting on demand in sat modulo theories, by C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli.

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

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