Ceci est une ancienne révision du document !
Les 4 séances de TP de logique visent à implémenter un programme testant la satisfiabilité d'une formule mise sous forme normale conjonctive (CNF), c'est-à-dire sous la forme d'un ensemble de clauses. Un exemple de tel solveur est MiniSat. Ce programme sera ensuite utilisé pour vérifier un circuit d'additionneur représenté à partir d'une spécification, tous deux représentés par des formules.
Ce programme va explorer l'espace de recherche (les combinaisons de valeurs possibles pour les variables) afin de déterminer la satisfiabilité de la formule testée.
Le rendu consistera en une archive .zip ou .tar.gz1) contenant:
etudiants.txt
contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants).Cette archive est à déposer sur spiral au plus tard le dimanche 22 décembre 2013 à 23h593). Il fortement recommandé de tester l'accès à la zone de dépôt avant la date butoir4).
La zone de dépôt est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=2647044
Le non respect de ces consignes entraînera une sanction dans la note du projet.
L'archive lif11-2013-enonce.zip contient un projet C/C++. Ce projet de départ fourni contient une arborescence de projet avec :
/Lisez-moi.txt
qui décrit le contenu de l'archive;/UnitTest
qui est une bibliothèque pour simplifier l'écriture des tests. Vous n'avez pas à vous intéresser à son contenu;/src
qui contient les sources fournies :/src/Makefile
permet de construire le projet avec make
, mais aussi de lancer les tests, de néttoyer le projet etc./src/main.cpp
et /src/main-test.cpp
sont les deux programmes exécutables du projet aux sens évidents : Resolution
qui lit une formule et évalue sa satisfiabilité et run-test
./src/formule.hpp
et /src/formule.cpp
donnent la structure d'arbre de syntaxe abstraite d'une formule et la structure de CNF. Quelques fonctions de base sont implémentées dont notamment formule2string
copier
qui constituent de bon exemples de fonctions récursives de parcours de l'arbre de syntaxe abstraite./src/sat.hpp
et /src/sat.cpp
sont encore quasiment vides et destinés à recevoir vos fonctions.lit_formule
qui crée l'arbre de syntaxe abstraite à partir d'une formule sous fourme de chaîne (typiquement, saisie au clavier ou lue dans un fichier).<note tip>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 fourni5) peut être poussé vers cette forge.</note>
Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues :
numerote
sont conceptuellement simples mais demandent un réel travail d'immersion et de prise en main du projet.<note important> Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci n'implique pas de devoir s'échanger les sources entre binômes. Le projet est à rendre après les vacances de Noël sous la forme d'une archive comme celle qui vous est fournie. Les modalités exactes du rendu seront données en temps utile. </note>
<note warning> Pour de l'aide sur les bases du C++ utiles à ce TP voir :
</note>
Le projet est fourni avec la bibliothèque UnitTest++
qui simplifie (grandement) l'expression et la gestion de tests unitaires. Un test peut être vu comme une fonction sans arguments dont on attend que le résultat s'évalue à true
.
Dans UnitTest++
un test est une macro de la forme TEST(nom_du_test) { code du test }
.
Dans le corps de cette fonction/macro certaines assertions CHECK(test)
sont vérifiées.
Il est possible de faire autant de CHECK
que l'on veut dans un TEST
, possiblement aucun. Le fichier main-test.cpp
contient l'exemple initial suivant :
// Un test simple qui réussit TEST(test1) { CHECK(2 == 1+1); } // Un test simple qui échoue TEST(test2) { CHECK(2 == 1+2); }
Le Makefile fourni dans le projet de départ permet d'exécuter les tests définis dans main-test.cpp
simplement via make test
.
TEST(lit_ecrit_formule)
.make test
. Comprendre l'affichage produit. Ne pas s'inquiéter des warnings (relativement inoffensifs) produits lors de la compilation du code qui vous est fourni.
Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour Conjunctive Normal Form) sont définies par des typedef
utilisant différents conteneurs de la STL. Une cnf_t
est un tableau dynamique (vector
) qui contient des clauses cls_t
représentées par des ensembles de littéraux (set
), les littéraux lit_t
étant codés par des entiers.
typedef unsigned int var_t; typedef int lit_t; typedef set<lit_t> cls_t; typedef vector<cls_t> cnf_t;
vector
permet un accès en temps constant via ses indices avec c[i]
comme les tableaux C et offre l'avantage d'être dynamique. On peut par exemple ajouter autant d'éléments que l'on veut avec c.push_back()
. Le nombre d'élément d'un vector
est donnée avec c.size()
.set
offre l'avantage de garantir l'unicité et un ordre total sur les éléments qu'il contient. En revanche, il est obligatoire d'utiliser les itérateurs pour parcourir son contenu, voir cet exemple.cls_t::const_iterator
, string cls2string(const cls_t& cl)
.ostream& operator«(ostream& out, const cls_t& cl)
qui permettra d'afficher des élément sur un ostream
comme cout
et cerr
. Voir l'exemple de l'affichage des éléments d’un conteneur.TEST
avec les vérifications suivantes :CHECK(cl1 != cl2);
CHECK(cl2 != cl1);
CHECK(cl1 == cl1);
CHECK(cl2 == cl2);
true
.size()
, string cnf2string(const cnf_t& c)
.ostream& operator«(ostream& out, const cnf_t& c)
. c. Cette méthode utilisera l'opérateur précédemment défini pour cls_t
.TEST
pour l'affichage d'une CNF c
contenant les clauses cl1
et cl2
.bool est_dans(const cls_t& cl, const cnf_t& c)
permettant de tester l'appartenance d'une clause à une CNF.TEST
pour vérifier notamment que est_dans(cl1, c)
et que est_dans(cl2, c)
.
Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe string
en C++) et leur préférer des entiers (var_t
dans le projet).
Il faut donc écrire une fonction void numerote(formule f, map<string,var_t> & corresp)
permettant de numéroter les variables d'une formule.
La classe map
de la STL est un conteneur associatif qui permet, dans le cas de map<string,var_t>
, de faire correspondre une unique variable à une chaîne8).
L'algorithme de numerote
est le suivant :
corresp
comme numéro) et ajouter la correspondance entre le nom de la variable et ce numéro dans corresp
;Pour l'efficacité, on représentera également les littéraux (c'est-à-dire des variables avec ou sans négation) par des entiers :
2
dans l'ensemble des littéraux positifs en multipliant par 2, le littéral p vaut ainsi 4
: c'est le 3ème entier pair associé à la 3ème variable.5
: c'est le 3ème entier impair associé à la 3ème variable.
Il faut ainsi prêter garder à ne pas mélanger la proposition dont la string
est p
avec sa représentation numérotée dans un map<string,var_t>
, ici 2
, et les littéraux associés dont les formules sont p et ~p valant respectivement 4
et 5
. Pour cela, il est vivement recommander d'utiliser systématiquement par la suite les fonctions var2lit
et neg
demandées en exercices.
string formule2string(formule f)
de transformation des formules en chaînes de caractères.void numerote(formule f, map<string,var_t> & m)
. On inspirera pour cela de formule2string
ainsi que de l'exemple d'utilisation de map.lit_t var2lit(var_t v, bool p = true)
qui injecte une variable v
dans l'ensemble des littéraux. Le booléen p
indique si le littéral est positif ou négatif. La déclaration bool p = true
permet d'affecter une valeur par défaut à ce paramètre ce qui permet de considérer alors var2lit
comme une fonction à un seul argument.lit_t neg(lit_t l)
qui prend un littéral et retourne sa négation. La fonction renvoie donc l+1
ou l-1
selon le cas.var_t lit2var(lit_t l)
qui prend un littéral en argument et retourne sa variable.bool positif(lit_t l)
qui renvoie true
si le littéral passé en argument est un littéral positif.UnitTest++
.<note important> Cette première partie donne les bases sur lesquelles s’appuyer dans la suite du projet. Ces bases doivent être solides. Bien garder les tests unitaires rédigés au fur et à mesure de l'avancement : ils permettent de s'assurer de la correction du code, de la non-régression lors des modifications et sont attendus dans le rendu final du projet comme la preuve que le programme a été convenablement testé. </note>
La transformation de Tseitin (c.f. TD du 07/10) permet d'obtenir à partir d'une formule f une CNF ayant la propriété d'être satisfiable si et seulement si f l'est. Cette transformation se fait via une fonction récursive tseitin, qui ajoute des clauses générées à une CNF passée en argument. Son principe de fonctionnement est le suivant: étant donnée f, la fonction renvoie un nouveau littéral l ainsi qu'une CNF c tels que c et l s'évaluent à vrai si et seulement si f s'évalue à vrai. La fonction tseitin(f) peut être algorithmiquement définie comme suit:
La CNF équisatifiable finale est obtenue comme suit:
On peut remarquer que les CNFs ne font que grossir, on peut ainsi passer la CNF en argument par référence : les ensembles de clauses c1 et c2 dans (p, … ∧ c1 ∧ c2) sont produites par les appels récursifs de tseitin. On passe également un compteur par référence var_t & next
pour générer de nouvelles variables frâiches. Ainsi en C/C++ on définira les deux fonctions :
lit_t tseitin(formule f, const map<string, int> & m, cnf_t & c, var_t & next); cnf_t tseitin(formule f);
<note tip> On donne l'exemple suivant avec f = (a ∨ b) ⇒ c, m le dictionnaire tel que a est numéroté par 0, b par 1, c par 2 (la prochaine variable fraîche est donc next = 3) et cl ={} un ensemble initialement vide de clauses. On a les appels récursifs suivants :
tseitin((a ∨ b) ⇒ c, m, cl = {}, 3)
tseitin((a ∨ b), cl, 3)
tseitin(a, cl, 3)
0 est le lit positif correspondant à a, on ajoute rien à cltseitin(b, cl, 3)
2 est le lit positif correspondant à b, on ajoute rien à clcl = 7_0_2_6_1_6_3
et 6 est le littéral positif qui code (a ∨ b)tseitin(c, cl = 7_0_2_6_1_6_3, 4)
4 est le lit positif correspondant à c, on ajoute rien à clcl = 7_0_2_6_1_6_3_9_7_4_8_6_8_5
et 8 est le litéral positif qui code f
Il faut enfin ajouter {8}
à cl pour obtenir finalement cl= 7_0_2_6_1_6_3_9_7_4_8_6_8_5_8
comme codage de Tseitin de (a ∨ b) ⇒ c.
</note>
lit_t tseitin(formule, map<string, int>, cnf_t, var_t)
telle que décrite.switch (f→op)
de la fonction précédente.cnf_t tseitin(formule f)
qui appelle numerote
et l'autre fonction tseitin
.
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
):
val_t valeur_lit(vector<val_t>, lit_t)
qui étant donnés le tableau des valeurs des variables suivant leur numéro et un littéral donne la valeur de ce littéral.val_t valeur_clause(vector<val_t>, cls_t)
qui étant utilise la fonction précédente pour déterminer la valeur de la clause.val_t valeur_cnf(vector<val_t>, cnf_t)
qui utilise la fonction précédente pour déterminer la valeur de la CNF.<note tip> Par exemple, pour évaluer la valeur de vérité de la formule f = (a ∨ b) ⇒ c, on a besoin de connaître les valeurs des variables a, b et c. Considérons la correspondance m = { a ↦ 0; b ↦ 1; c ↦ 2; d ↦ 3} et l’interprétation où a & c sont VRAI, b FAUX et d INDETERMINEE. Cette interprétation est représentée par le vecteur [VRAI | FAUX | VRAI | INDETERMINEE]. On a dans cet exemple valeur_lit(v, ¬c) = FAUX, valeur_lit(v, ¬b) = VRAI et valeur_lit(v, ¬d) = INDETERMINEE
</note>
Écrire la fonction récursive
bool cherche(vector<val_t> & valeurs, var_t suiv, const cnf_t & cnf);
qui renvoie true
si cnf
est satisfiable, sachant que:
valeur
contient les valeurs des variablessuiv
est une variable non affectée. On considère que toutes les variables dont le numéro est inférieur au numéro de suiv
ont une valeur dans valeurs
.La fonction procédera comme suit:
suiv
à VRAI dans valeurs
suiv+1
true
suiv
à FAUX et tester à nouveau la satisfiabilité de la formule (comme en 2/3)true
suiv
à INDETERMINEE, puis renvoyer false
.Modifier la fonction main de façon à:
<note important>
A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier la satisfiabilité (et donc aussi la validité) d'une formule. L'efficacité algorithmique de la méthode dépend des stratégies de recherche implémentée dans cherche
et de simplification que l'on peut apporter lors du calcul de valeurs de la CNF, pour éviter d'effectuer trop de calculs. C'est l'objet de la quatrième partie du projet.
Avant cela on va coder dans la troisième partie une application qui utilise le solveur: un vérificateur d'additionneur binaire n-bits. </note>
Dans cette partie, on modélise un additionneur n-bits (la spécification, cf TD2) qui est utilisé pour vérifier un additionneur dont la représentation est donnée dans un fichier.
La génération d'une spécification pour l'additionneur n-bits fait utilise des substitutions. Une substitution sera représentée par une map<string,formule>
qui à chaque variable substituée associe la formule qui la remplacera.
formule applique(formule f, const map<string,formule> & substitution)
qui fabrique la formule sur laquelle la substitution à été appliquée à partir de la formule de départ et de la substitution à appliquer. Attention, la formule de départ ne doit pas être modéfiée par l'application de la substitution.
La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules.
On considère que les entrées sont données par les variables p1
… pn
et q1
… qn
et que les sorties sont codées par les formules A1 … An, Bn. B1 … Bn sont les retenues générées par la somme dans la colonne n.
On utilisera les formules suivantes:
La génération de cette spécification par récurrence peut être définie comme suit:
Écrire la fonction additionneur
suivante:
vector<formule> additionneur(int taille);
On pourra procéder de manière itérative en s'appuyant sur deux vector<formule>
: un qui contiendra les Ai, l'autre contenant les Bi.
A la fin de la fonction, il suffira de renvoyer les vector
contenant les Ai juste après lui avoir ajouté la formule Bn
Modifier ensuite le main
de façon à accepter un argument --check-adder
. Si cet argument est présent on supposera par convention que le fichier de formules contient les formules A'1, … , A'n, B'n d'un additionneur n-bits. On appellera la fonction additionneur(n)
pour récupérer les n+1 formules de la spécification correspondante. On construira la formule ¬( (A1 ⇔ A'1) ∧ … ∧ (An ⇔ A'n) ∧ (Bn ⇔ B'n) ). On testera la satisfiabilité de cette formule: si elle est insatisfiable, l'additionneur passé en argument est correct.
<note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation.</note>
L'exploration de l'espace de recherche implémentée précédement ne teste la satisfaction de la forme conjonctive que lorsque la valeur de toutes les variables est connue. Un moyen d'améliorer l'efficacité du solveur consiste à tester systématiquement la valeur de la CNF à chaque affectation de variable de façon à éviter d'explorer un morceau de l'arbre de recherche dont on sait qu'il mènera toujours à des évaluation de la CNF valant FAUX.
Modifier la fonction cherche
pour tester la satisfaction à chaque affectation de variable de façon à détecter au plus tôt les combinaisons de valeurs partielles insatisfiables. Si la CNF vaut FAUX, alors on peut renvoyer directement false
sans faire l'appel récursif. Attention, il faut bien penser à remettre id_var à INDETERMINEE avant de renvoyer false, sous peine de fausser la suite de l'exploration de l'arbre de recherche.
Remarque: cette remise à zéro fait partie du “retour arrière” lors de l'exploration de l'arbre de recherche.
Pour améliorer l'efficacité des tests de satisfiabilité, l'étape suivante consiste à indexer les clauses par les littéraux qui les contiennent. Plus précisément, il s'agit de construire une structure qui associe à chaque littéral la liste des clauses dans lequel il apparaît. Il suffit de tester uniquement cette liste lors de l'affectation d'un littéral à faux pour vérifier si l'affectation rend la forme conjonctive insatisfaite.
La structure d'indexation proposée consiste en un tableau contenant des listes de clauses. Les indice du tableau correspondent aux numéros des littéraux.
vector<vector<cls_t> > indexe_clauses(const cnf_t& cnf)
qui renvoie une telle structure initialisée en fonction de la forme conjonctive passée en argument.
bool contient_insatisfaite(var_t variable, const vector<val_t>& valeurs,const vector<vector<cls_t> >& index_clauses)
index_clauses
est la structure d'indexation des clausesvariable
est le numéro d'une variable. On appelle l le littéral correspondant à variable et prenant la valeur FAUXvaleurs
est le tableau des valeurs affectées aux variablesvaleur_cnf
dans cherche
par une utilisation de la fonction contient_insatisfaite
.L'objectif de cette optimisation est, étant données certaines valeurs choisies pour les variables n°1 à n, d'affecter les variables dont la valeur est INDETERMINEE et qui doivent nécessairement prendre une certaine valeur pour que la CNF aie une chance de s'évaluer à VRAI.
Pour cela, on s'appuie sur la remarque suivante. Soit une clause L1 ∨ … ∨ Lk. Si tous les littéraux de cette clause valent FAUX, sauf un certain Lj qui vaut INDETERMINEE, alors cette clause ne pourra s'évaluer à VRAI que si Lj prend la valeur VRAI. On dira que cette clause est devenue unitaire. Il est ainsi inutile de tester les valeurs pour la variable V de Lj: si Lj est un littéral positif, V doit prendre la valeur VRAI, si Lj est un littéral négatif, elle doit prendre la valeur FAUX.
On peut également remarquer que si Lj se voit affecter la valeur VRAI, alors ¬Lj a pour valeur FAUX. Cela peut avoir deux conséquences:
On peut définir une fonction propage
qui va se charger d'effectuer la propagation unitaire. A la manière de contient_insatisfaite
, elle va s'appuyer sur l'index des clauses pour trouver rapidement les clauses à traiter. En effet, à l'exception des clauses qui sont unitaire dès le début, une clause ne peut être rendue unitaire que si un de ses littéraux est affecté à FAUX. On peut donc, lors de l'affectation d'une valeur à une variable, savoir, grâce à l'index, quelles sont les clauses à tester pour savoir si elles sont unitaires.
Lors du retour arrière, il est important de défaire le travail effectué par la propagation unitaire. Comme celle-ci peut toucher des variables dont les numéros ne se suivent pas forcément, il faudra stocker la liste des variables à remettre à zéro au cas où le choix de valeur ayant déclenché la propagation unitaire ne permet pas de montrer que la CNF est satisfiable.
vector<var_t> propage(lit_t lit, vector<val_t> & valeurs, cnf_t & cnf, vector<vector<cls_t> > & index)
Cette fonction renvoie la liste des variables affectées. Par convention, si cette liste est vide on supposera que la propagation a mené à une contradiction. La fonction aura le comportement suivant:
vector
résultat à un vector
videvector<lit_t>
contenant au départ lit
. Cette structure contiendra la liste courante des littéraux que l'on veut affecter à VRAI.vector
résultat, puis on renvoie un vector vide.propage
au lieu de contient_insatisfaite
propage
à INDETERMINEE lors des retours arrière.
Faire fonctionner le projet sous Windows nécessite l'utilisation de Cygwin (installé en salle TP Nautibus, à vérifier pour les salles Ariane). La compilation peut se faire en invoquant make
comme sous Linux. Sous Cygwin, les lettres des lecteurs sont des répertoires dans /cygdrive. Ainsi pour aller dans le répertoire U:\LIF11\projet
il faut faire cd /cygdrive/u/LIF11/projet
Il faut par ailleurs modifier le Makefile en changeant l'option -std=c++0x
en -std=gnu++0x
.
La version de g++ fournie avec MacOSX est parfois trop vieille pour fonctionner avec l'option -std=c++0x
. Il alors faut installer une version plus récente du compilateur (e.g. g++-4.7) avec Homebrew, Macports ou encore Fink.
Pour compiler il faut ensuite faire (dans le cas où le g++ installé est la version 4.7): make CXX=g++-4.7
, ou bien make CXX=g++-4.7 test
pour exécuter les tests.
hg clone https://forge.univ-lyon1.fr/hg/inf3034l-2013-base
CHECK
, on fera une simple vérification visuelle.cl1 = { 7, 6, 1, 4, 1};
.