Ce document est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 3.0 Unported
Version du 12/12/2016
L'objectif de ce projet est de se familiariser avec des techniques de base de test de satisfiabilité booléenne via l'implémentation d'un solveur SAT et d'utiliser la résolution SAT pour résoudre des Sudoku.
Le projet se découpe ainsi en deux parties: une partie solveur SAT et une partie modélisation en formule conjonctive (par fois appelée cnf) du problème de planification.
Le projet peut être réalisé en binôme, mais pas en groupe de 3 étudiants ou plus.
Remplir lors de la première séance la case tomuss
num_binomeavec le numéro d'étudiant de votre binôme (8 chiffres). Si vous n'avez pas de binôme, laissez cette case vide.
La version finale du projet (avec toutes les parties) doit être déposée sur tomuss dans la case
rendu_prj_finalpour le 18/12/2016.
Les archives à déposer doivent avoir la même structure que l'archive fournie. Attention en particulier à ne pas déposer d'archive contenant des résidus de compilation ou des exécutables. Utiliser la commande
make cleanavant de créer l'archive à déposer.
Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une forge avec un hébergement de dépôts mercurial.
Le projet fourni peut être récupéré via la commande suivante exécutée dans le répertoire cloné d'un dépôt mercurial vierge:
hg pull https://forge.univ-lyon1.fr/hg/inf3034l-liflc-projet-2016Le projet est par ailleurs également téléchargeable ici: lien archive
Le projet contient ce sujet, des exemples et un code de départ en C++. Il est demandé de regarder le code fourni afin d'avoir une idée de ce qui est déjà implémenté et de ce qui reste à faire.
La base de code fournie suppose que l'on travail dans un environnement de type Unix (Linux, MacOSX). Bien que le code soit assez générique vis-à-vis du système d'exploitation, aucune garantie n'est donnée sur le fonctionnement sous Windows et le projet sera testé sous Linux et/ou MacOSX.
Liens utiles:
Le travail pour ce projet peut être divisé en 4 parties correspondant chacune à une séance de TP et du travail autour. Après la première séance de TP, il est ainsi conseillé d'anticiper chaque séance afin d'avoir déjà des questions prêtes en début de créneau de TP.
Cette partie consiste à écrire un programme qui lit une formule conjonctive au format Dimacs et génère un fichier indiquant si la formule est satisfiable. Dans le cas où la formule est satisfiable, le fichier contiendra également les littéraux vrais dans un des modèles de la formule.
Le format Dimacs se présente de la manière suivante:
c sont des commentaires.p cnf n m indique que la formule conjonctive contiendra \(n\) variables et \(m\) clauses. Les variables sont numérotées de \(1\) à \(n\). Une telle ligne est optionnelle.Par exemple, la formule conjonctive \((p\vee q\vee \neg r)\wedge(\neg p \vee \neg q)\wedge(\neg p\vee r)\wedge(\neg p\vee q\vee \neg r)\) sera représentée par le fichier suivant (avec \(p\) a pour numéro \(1\), \(q\) a pour numéro \(2\) et \(r\) a pour numéro \(3\)):
p cnf 3 4
1 2 -3 0
-1 -2 0
-1 3 0
-1 2 -3 0Les fichiers résultat ont la forme suivante:
SAT si la formule conjonctive est satisfiable, soit UNSAT dans le cas contraire.Par exemple, un modèle de la formule précédente est \(I\) avec \(I(p)\) est faux (donc le littéral \(\neg p\) est affecté à vrai), \(I(q)\) est vrai (donc le littéral \(q\) est affecté à vrai) et \(I(r)\) est faux (donc le littéral \(\neg r\) est affecté à vrai). Ce résultat correspond au fichier suivant:
SAT
-1 2 -3 0Les fonctions permettant de lire le format Dimacs et d'écrire le résultat sont déjà écrites dans le fichier dimacs.cpp. Le fichier sat.cpp contient des squelettes de fonctions pour implémenter le solveur SAT.
Le logiciel minisat est un solveur SAT utilisant les formats d'entrée et de sortie expliqués ci-dessus. Il peut se substituer à votre propre solveur SAT à des fins de comparaison ou pour tester la partie modélisation de Sudoku indépendamment de la partie SAT.
Les formules conjonctives ayant une forme très régulière (conjonction de clauses), elles peuvent être représentées simplement par un tableau (vector) de clauses. Les clauses sont elles-mêmes représentées comme des ensembles de littéraux. Les littéraux sont représentés par des entiers positifs (pairs pour les littéraux positifs, impairs pour les littéraux négatifs).
De même, chaque variable se voit attribuer un numéro unique. Attention les entiers utilisés pour numéroter les littéraux et les variables sont différents. Si une variable \(p\) est numérotée avec un entier \(n\), le littéral positif correspondant (i.e. \(p\)) est numéroté avec l'entier \(2n\), alors que le littéral négatif correspondant (i.e. \(\neg p\)) est numéroté avec l'entier \(2n+1\).
Attention, ce codage sous forme d'entiers est donc différent du codage Dimacs. Les fonctions fournies pour lire et écrire ces fichiers s'occupent de faire la conversion correctement.
Afin de permettre de faire facilement évoluer le code (en particulier afin d'ajouter facilement des éléments additionnels), on encapsule ces types dans des struct.
On obtient les structures définies dans le fichier sat.hpp.
Coder les fonctions var2lit, lit2var, positif et oppose.
Le projet est fourni avec une bibliothèque de tests unitaires: unittest-cpp.
Des exemples de tests unitaires se trouvent dans les fichiers test-exemples.cpp et test-code-fourni.cpp. Les tests sont exécutés via la commande make test1.
Il est à noter que tout fichier nommé
test-xxx.cppsera considéré comme contenant des tests unitaires. En particulier, les fonctions définies dans ces fichiers ne seront pas incluses dans les autres exécutables.
Lancer make test. Un test échoue. Trouver et supprimer ce test.
Écrire des tests pour vérifier le bon fonctionnement des fonctions traitant des littéraux.
Par la suite, lorsque l'on demandera de tester une fonction, cela sous-entendra qu'il faut le faire via un test unitaire.
Dans un premier temps, on va implémenter un solveur naïf qui évoluera ensuite au gré des optimisations vers un solveur plus efficace.
La structure etat_t est utilisée pour conserver les informations concernant l'exploration courante de l'espace de recherche, comme la valeur affectée à chaque variable ou le numéro de la dernière variable sur laquelle on a effectué un choix.
Au cours de l'exploration de l'espace de recherche, on peut représenter les interprétations des variables propositionnelles par un tableau qui à chaque numéro de variable fait correspondre une valeur (de type val_t):
vrai si la variable est affectée à vraifaux si la variable est affectée à fauxindeterminee si la variable n'est pas affectéeLe type val_t est une énumaration C++. Il est ainsi possible d'utiliser les valeurs dans un switch.
Coder la fonction init_etat afin d'initialiser le tableau des valeurs en mettant toutes les variables à la valeur indeterminee. Le numéro de la dernière variable affectée pourra par exemple être initialisé à -1.
Coder la fonction valeur qui calcule la valeur d'un littéral. Tester la fonction.
La valeur d'une clause peut être déterminée comme suit:
vrai si elle possède un littéral de la valeur courante est vrai,faux si tous ses littéraux sont faux,indeterminee dans les autres cas.Coder la fonction evaluer_clause et la tester.
La valeur d'une formule conjonctive peut être déterminée comme suit:
faux si elle possède une clause qui s'évalue à faux,vrai si toutes ses clauses s'évaluent à vrai,indeterminee dans les autres cas.Coder la fonction evaluer_cnf et la tester.
Le test des fonctions sur les formules conjonctives peut utiliser des fichiers au format Dimacs. Il suffit de s'inspirer de la fonction
maindemain-sat.cpppour cela ou des tests danstest-code-fourni.cpp. Attention aux noms des fichiers qui doivent être relatifs au répertoirec++(depuis lequel est exécutérun-test).
Afin d'explorer l'espace de recherche, on peut procéder en suivant le pseudo-code suivant:
fonction chercher(etat, cnf):
l = choisit_litteral(etat, cnf)
ret_arr = affecte(etat, cnf, l)
val_cnf = evaluer_cnf(etat, cnf)
si val_cnf == vrai
|| (val_cnf == indeterminee && chercher(etat, cnf)) alors
renvoyer true
fin si
retour_arriere(etat, cnf, ret_arr)
l = oppose(l)
ret_arr = affecte(etat, l)
val_cnf = evaluer_cnf(etat, cnf)
si val_cnf == vrai
|| (val_cnf == indeterminee && chercher(etat, cnf)) alors
renvoyer true
sinon
retour_arriere(etat, cnf, ret_arr)
renvoyer false
fin si
fin chercherLa fonction choisit_litteral choisit un littéral à affecter à vrai, i.e. une variable et une valeur pour cette variable.
La fonction affecte modifie l'état de l'exploration en changeant la valeur de la variable. Elle change également la dernière variable affectée. Plus tard, cette fonction pourra faire des déductions comme de la propagation unitaire. La fonction renvoie les informations nécessaires au retour arrière, c'est à dire pour le moment l'avant-dernière variable affectée et le littéral affecté.
La fonction retour_arriere utilise les informations précédentes pour remettre l'état à sa valeur avant la dernière affectation de littéral.
Ces fonctions sont à implémenter dans sat.cpp. Les tests peuvent utiliser des formules conjonctives lues dans un fichier dimacs de manière similaire à ce qui se fait dans la fonction main du fichier main-sat.cpp.
Implémenter la fonction affecte, puis la fonction retour_arriere et les tester.
Le choix du littéral à affecter peut se faire de manière heuristique pour tenter de rendre l'exploration plus efficace. Pour ce solveur naïf, on prendra la première variable qui n'a pas encore de valeur et lui donnera la valeur vrai. On pourra ici utiliser la dernière variable affectée (numéro \(n\)) pour connaître la variable à affecter ensuite (numéro \(n+1\)).
Implémenter la fonction choisi_litteral et la tester.
La fonction chercher permet de terminer l'implémentation du solveur naïf.
Implémenter la fonction chercher et la tester.
Le problème de Sodoku consiste à placer des nombres sur une grille \(n^2\times n^2\) (pour le sudoku classique \(n=3\)).
Un problème de Sudoku sera représenté par un fichier représentant la grille initiale à compléter:
0 correspondent aux cases à remplirLes régions sont des sous-grilles carrées de taille \(n\times n\) découpant la grille initiale en \(n\times n\) parties disjointes. On suppose que les lignes et les colonnes sont numérotées à partir de \(0\) en partant du haut et de la gauche. Les coordonnées du coin supérieur gauche de chaque région sont ainsi de la forme \((i\times n, j \times n)\) où \(0\leq i\leq n-1\) et \(0\leq j\leq n-1\).
Compléter une grille de Sudoku se fait en respectant les 3 contraintes suivantes:
Pour résoudre un Sudoku, on procède comme suit:
sudoku2dimacs, va convertir un problème de Sudoku en formule conjonctive (sous forme de fichier Dimacs), telle que la solution du Sudoku correspond au modèle de cette formule (un problème de Sudoku traditionnel n'admet normalement qu'une seule solution).sat calcule un éventuel modèle de la formule conjonctive.res2sudoku, convertit le résultat obtenu en grille de sudoku complétée.Les fonctions lit_sudoku et ecrit_sudoku permettent de lire et écrire des grilles de sudoku. Le fichier exemples/sudoku/grille-test1.txt contient un exemple de grille de sudoku \(3^2\times 3^2\)
Afin de coder le problème de Sudoku sous forme de formule conjonctive, on introduit \(n^2\) variables booléennes par case de la grille. On note la variable \(p_{i,j}^v\) la \(v^{ième}\) variable de la case située à la position \((i,j)\) dans la grille (avec \(0\leq i\leq n^2-1\),\(0\leq i\leq n^2-1\) et \(1\leq v\leq n^2\)). On utilisera la convention que la variable \(p_{i,j}^v\) prend la valeur vrai si et seulement si la case \((i,j)\) voit être remplie avec la valeur \(v\).
On suppose que l'on numérote les variables comme suit (où \(num(p)\) est le numéro de la variable \(p\)):
Autrement dit: les variables d'une même case sont numérotées consécutivement. Le numéro de la première variable d'une case suit immédiatement le numéro de la dernière variable de la case précédente, les cases étant considérées lignes par ligne.
Par exemple, si on considère une grille de Sudoku de taille \(2^2\times 2^2\):
Sur une grille de taille \(3^2\times 3^2\), \(num(p_{0,8}^9)=80\) et \(num(p_{8,8}^9)=728\).
Coder et tester la fonction l_case_v(n2,i,j,v) qui renvoie le littéral positif associé à la variable codant la valeur v dans la case (i,j) si le nombre le nombre de lignes dans la grille de Sudoku est n2 (i.e. \(n^2\)). Cette fonction doit avoir un temps de calcul constant.
Afin de coder le problème de Sudoku sous forme d'un ensemble de clauses plus facilement, on introduit une contrainte appelée "exactement \(1\) vrai parmi \(n\)". Une contrainte peut être vue comme une formule contraignant les valeurs de certaines variables. Dans le cas de "exactement \(1\) vrai parmi \(n\)", cette formule va imposer que parmi \(n\) littéraux, un littéral prend la valeur vrai, les autres prenant la valeur faux.
En s'appuyant sur les remarques suivantes, déduire un ensemble de clauses codant cette contrainte:
Coder la fonction exactement_1_parmi_n. Si votre solveur SAT est fonctionnel, il est possible de tester ces clauses en utilisant la fonction cherche.
La première chose dont on veut s'assurer est que toutes les cases sont remplies et que l'on n’a pas placé 2 nombres différents dans la même case. Pour cela il suffit que pour chaque case il y ait exactement une des variables codant les valeurs de la case à vrai.
Commencer à coder la fonction genere_probleme_sat en utilisant pour chaque case du sudoku la fonction exactement_1_parmi_n afin d'assurer que chaque case possède exactement une valeur.
Chaque ligne doit comporter des nombres différents. Comme il y a autant de nombres que la taille de la ligne, chaque nombre doit apparaître exactement une fois. Donc pour chaque nombre \(v\), pour chaque ligne \(i\) il y a exactement une case \((i,j)\) dans la ligne pour laquelle la variable \(p^v_{i,j}\) vaut vrai.
Continuer le codage de la fonction genere_probleme_sat en utilisant pour chaque ligne et chaque nombre la fonction exactement_1_parmi_n afin d'assurer que chaque valeur est placée exactement une fois sur chaque ligne.
On peut remarquer qu'assurer que toutes les valeurs sont différentes sur chaque colonne et dans chaque région est similaire au cas des lignes.
Coder les contraintes sur les colonnes et les régions dans genere_probleme_sat.
Enfin il reste à prendre en compte les nombres déjà placés sur la grille. Si la case \(i,j\) a la valeur \(v\), il suffit de forcer la valeur de la variable \(p^v_{i,j}\) à vrai en utilisant une clause unitaire.
Terminer la fonction genere_probleme_sat en générant une clause unitaire par case déjà remplie dans la grille.
La dernière étape consiste à convertir un modèle en grille de sudoku résolue. C'est le programme res2sudoku qui s'en charge. Il prend en argument la grille de sudoku initiale, le fichier contenant un modèle de la formule conjonctive et le nom du fichier dans lequel écrire le résultat.
Le fichier main-res2sudoku.cpp contient un squelette de code pour res2sudoku (lecture et écriture des fichiers).
Compléter le code de la fonction main dans main-res2sudoku.cpp afin de remplir la variable sudoku_resolu avec le bon nombre pour chaque case de la grille.
L'objectif est ici de construire un index pour accéder rapidement au clauses qui contiennent un littéral donné.
L'index sera codé dans un tableau de tableau de pointeur sur clauses. On ajoutera donc le champ suivant à cnf_t:
vector< vector<cls_t*> > indexOn rappelle qu'en C++, il est possible de récupérer l'adresse du contenu d'un vecteur via &, comme le montre le test suivant:
struct toto {
std::vector<int> a;
};
TEST(ref_in_vector) {
using namespace std;
vector<toto> v1;
toto t1;
t1.a.push_back(1);
v1.push_back(t1);
// rappel: 1Lu est 1 en unsigned long
CHECK_EQUAL(1Lu,v1[0].a.size());
vector<toto*> v2;
v2.push_back(&v1[0]);
CHECK_EQUAL(1Lu,v2[0]->a.size());
v1[0].a.push_back(3);
CHECK_EQUAL(2Lu,v2[0]->a.size());
}Créer une fonction genere_index(cnf_t& cnf) qui génère la structure d'index et appeler cette fonction avant la recherche.
À cause du fonctionnement de vector (i.e. réallocation du tableau sous-jacent au vector en cas de manque de place), l'approche précédement proposée qui consistait à insérer dans l'index des pointeurs sur clause au fur et à mesure peut mener à des erreurs de segmentation. Il faut donc construire l'index seulement une fois que toutes les clauses ont été ajoutées à la formule conjonctive.
On peut remarquer que si l'affectation d'un littéral rend la CNF fausse, c'est qu'une des clauses contenant l'opposé du littéral devient fausse. On peut donc optimiser la vérification de la valeur de vérité de la CNF en ne vérifiant que les clauses contenant le littéral opposé au littéral affecté. Afin de réutiliser ce test dans evaluer_cnf, on peut ajouter un champ booléen est_faux dans etat_t (attention à gérer correctement ce champs dans retour_arriere). Par défaut, ce champ vaudra false (i.e. la CNF n'est pas fausse) et pourra être modifié en true (i.e. la CNF est devenue fausse) dans affecte si une clause est dédectée comme étant devenue fausse. Dans evaluer_cnf, il suffit alors d'utiliser ce champ pour tester si la CNF est fausse (au lieu de regarder toutes les clauses).
A ce stade, l'indexation se fait au moment de la construction de la CNF et l'index est utilisé dans affecte pour tester les clauses fausse.
La propagation unitaire consiste à déduire des valeurs à partir de l'affectation courante selon le principe suivant: si tous les littéraux d'une clause sauf un (que l'on appellera \(l\)) sont faux, alors pour que la clause puisse s'évaluer à vrai il est nécessaire que \(l\) prenne la valeur vrai. Une telle clause est dite unitaire.
On peut remarquer que les littéraux déduits (i.e. ceux que l'on a affecté à vrai suite à la déduction précédente) peuvent eux-même déclencher de nouvelles propagations, c'est-à-dire permettre de déduire d'autre propagations. Il faut donc itérer la déduction des littéraux jusqu'à ce qu'il n'y ait plus aucun littéral déductible.
Pour gérer correctement le retour arrière, il ne faut plus se contenter d'un seul littéral affecté (litteral_affecte dans infos_retour_arriere_t), mais il sera nécessaire de gérer une collection (e.g. un vector) de littéraux. Lors du retour arrière la valeur de chacun de ces littéraux sera à remettre à indeterminee.
Vérifier si une clause est unitaire n'est pas très différent de vérifier si elle est fausse. On peut ainsi combiner le calcul à la volée de la valeur des clauses avec la propagation unitaire.
Écrire une fonction bool verifie_clause(const cls_t & clause, const etat_t & etat, lit_t & l, val_t & val) qui a le comportement suivant:
l au littéral propagé, affecte indeterminee à val et renvoie true;val la valeur de la clause et renvoie false.Tester cette fonction.
Le pseudo-code suivant permet de procéder à une propagation unitaire:
fonction propager(l, etat, cnf, ret_arr):
lit_a_propager = {}
ajouter(l, lit_a_propager)
tant que lit_a_propager non vide
lp = prendre(lit_a_propager)
mettre_a_vrai(lp, etat)
ajouter(lp, ret_arr.litteral_affectes)
olp = oppose(lp)
clauses = clauses_contenant_l(cnf, olp) // utilisation de l'index
pour cl dans clauses:
si verifie_clause(cl, etat, l2, val)
ajouter(l2, lit_a_propager)
sinon si val == faux
etat.est_faux = true
renvoyer false
fin si
fin pour
fin tant que
renvoyer true
fin propagerOn peut remarquer que la fonction propager renvoie false si elle mène à une contradiction (i.e. elle s'évalue à faux). Elle met par ailleurs à jour le contenu de ret_arr et de etat en fonction des déductions faites lors de la propagation.
Coder la fonction propager et utiliser cette fonction dans affecte. Modifier la fonction retour_arriere (gestion de la collection des littéraux). Tester ces deux fonctions.
Ces optimisations sont optionnelles et donneront des points bonus.
Marquage des clauses vraies
Ajouter à la structure de clause un champ booléen est_vraie afin d'éviter de tester la valeur d'une clause dont on sait déjà qu'elle est vraie. La liste des clauses qui peuvent être rendues vraies par l'affectation d'un littéral est facilement obtenue via l'index. Il faut gérer correctement le retour arrière par l'ajout d'une liste de pointeurs sur clauses.
Littéraux surveillés
Pour qu'une clause soit unitaire ou fausse, il faut qu'il y ait au maximum un littéral dont la valeur est indéterminée dans cette clause. Il est donc inutile de tester les clauses pour tous leur littéraux: il suffit d'en distinguer deux (i.e. ajouter deux champs littéraux à la structure de clause) et de ne traiter la clause (i.e. effectuer la propagation unitaire) que si l'un des deux est affecté. Attention, si lors du traitement, la valeur de la clause reste indéterminée (en particulier si la clause n'est pas unitaire), il faut changer de littéral surveillé en le remplaçant par un autre littéral dont la valeur est indéterminée. Cette optimisation ne nécessite pas de gestion lors du retour arrière, car même si les littéraux surveillés sont modifiés cela ne change pas leur utilisation.
Littéraux monotones
On peut remarquer que si l'opposé d'un littéral n'apparaît dans aucune clause dont la valeur est indéterminée, on peut affecter ce littéral sans que la formule conjonctive ne devienne fausse pour autant. En ajoutant un compteur d'occurrences (dans les clauses à valeur indéterminee) pour chaque littéral, on peut facilement déterminer quand un littéral devient monotone (son opposé ayant son compteur d'occurrences à 0). Chaque fois qu'une clause devient vraie, le compteur des littéraux qui sont dans cette clause et qui dont la valeur est indéterminée est décrémenté. Lors du retour arrière, il est nécessaire de rétablir la valeur des compteurs de littéraux modifiés.
Ce document est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 3.0 Unported
Cette commande compile et lance l'exécutable run-tests depuis le répertoire c++.↩