Année 2012-2013
Les 4 séances de TP de logique visent à implémenter un programme testant la satisfiabilité d'une formule mise sous forme normale conjonctive, c'est-à-dire sous la forme d'un ensemble de clauses. La méthode utilisée par ce programme est le principe de résolution (voir Mémo 4) qui consiste à combiner des paires de clauses, l'une contenant un littéral et l'autre sa négation, pour en produire une nouvelle. Ainsi de (¬p ∨ p1 ∨ … ∨ px) et (p ∨ q1 ∨ … ∨ qy) on déduit (p1 ∨ … ∨ px ∨ q1 ∨ … ∨ qy). On effectue cette déduction tant que possible jusqu'à :
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 vendredi 11 janvier 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/spiral/spiral.html#/activities/goto_folder/1992964
Le non respect de ces consignes entraînera une sanction dans la note du projet.
L'archive lif11-2012-enonce.zip (v1.1) 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/resolution.hpp
et /src/resolution.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).Le projet est divisé en trois 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>
Pour de l'aide sur les rudiments du C++ voir l'introduction au C++ et le code d'exemple.
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îne7).
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.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. CM du 23/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>Une erreur s'était glissée dans la définition précédente : il faut bien lire … ∧ c1 ∧ c2 pour les clauses produites et non … ∧ p1 ∧ p2 comme indiqué avant la correction.</note>
<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
.Le calcul des résolvante est la première brique réellement liée à la résolution proprement dite. Le calcul des résolvantes est effectué ainsi :
pivot
, étant données deux clauses cl1 et cl2, trouve un littéral l de cl1 tel que ¬l est présent dans cl2. On traite le cas où un tel littéral n'existe pas en renvoyant -18). On codera de préférence cette fonction avec un algorithme linéaire dans la taille des clauses, en s'appuyant sur les remarques suivantes:resolvante
, étant données deux clauses et un littéral dans la première clause, calcule la clause qui est la résolvante des deux premières.lit_t pivot(const cls_t& cl1, const cls_t& cl2); cls_t resolvante(const cls_t& cl1, lit_t l, const cls_t& cl2);
pivot
.resolvante
.
Implémenter l'algorithme de recherche d'un arbre de résolution par ajout de clauses dans une CNF (voir td). On utilisera par exemple une pile avec un vector<clause>
sous-jacent pour stocker les clauses à traiter. Ce vecteur sera initialisé avec les clauses contenues dans la CNF résultant de la traduction de la formule de départ via la transformation de Tseitin. Ensuite on répète tant que possible la recherche, le calcul et l'ajout de résolvante. L'algorithme en pseudo-code est le suivant :
Entrée : cnf l'ensemble initial de clauses, que l'on complète au fur et à mesure;
Variable locale : q la pile des clauses restant à traiter, quand elle est vide on a saturé l'espace de recherche;
Résultat : true si on peut dériver la clause vide, false sinon;
Algorithme :
Le prototype formel C++ attendu est le suivant :
bool resolution(const cnf_t& cls);
resolution
.resolution
.
<note tip>Une clause est équivalente à ⊤ si elle contient un littéral et sa négation. D'après la manière dont son codés les littéraux et les clauses, si p et ¬p sont dans une clause, ils se suivent lorsqu'on parcourt la clause. On peut ainsi détecter les clauses équivalentes à ⊤ via un simple parcours de la clause en comparant le littéral courant à la négation de celui qui vient d'être lu.</note>
<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 resolution
et de simplification que l'on peut apporter lors du calcul des résolvantes, pour éviter d'en introduire des inutiles. C'est l'objet de la troisième partie du projet.
</note>
Les résolvantes avec des petites clauses sont celles qui ont le plus de chances de:
Pour cela, on utilise une file de priorité pour stocker les clauses à traiter afin de considérer les petites clauses en premier. La classe priority_queue
de la STL est très semblable à la classe queue
, la différence essentielle est qu'elle est paramétrée par la classe de comparaison qui permet de trier les objets stockés selon leur priorité. La déclaration de la classe de comparaison est un peu particulière : c'est un foncteur (objet-fonction, functor pour function-object en anglais).
En pratique c'est une classe pour laquelle on définit operator()
et qui s'utilise comme une fonction. Dans l'exemple suivant, on déclare une première file q
qui classe les entiers selon l'ordre par défaut (à savoir, l'ordre naturel 0 < 1 < 2 < 3 …) et une suivante pq
qui utilise un ordre personnalisé mycomp
où les entier impairs sont triés en premiers 1 < 3 < 5 < … < 0 < 2 < 4 …
#include <iostream> #include <queue> using namespace std; struct mycomp { inline bool operator() (const size_t& lhs, const size_t& rhs) const{ if (lhs%2 != rhs%2) return (lhs%2==1); else return (lhs<rhs); } }; int main (int argc, char* argv[]){ priority_queue<size_t, vector<size_t>> q; //ordre par défaut priority_queue<size_t, vector<size_t>, mycomp> pq; //ordre personnalisé for(size_t i = 5; i < 10; ++i){ q.push(i); pq.push(i); } for(size_t i = 0; i < 5; ++i){ q.push(i); pq.push(i); } size_t x,y; while(!q.empty()){ x = q.top(); y = pq.top(); cout << "x = " << x << ", y = " << y << endl; q.pop(); pq.pop(); } return 0; }
inline bool operator() (const cls_t& lhs, const cls_t& rhs) const
du foncteur de comparaison less_prioritary
entre clauses qui classe d'abord les clauses selon la taille;resolution
précédente pour que la pile q soit désormais une priority_queue
utilisant le foncteur less_prioritary
précédemment défini;resolution
en donnant priorité aux petites clauses.
On peut remarquer que si une clause C1 est incluse dans une clause C, toute résolvante de C avec une autre clause C2 contiendra soit C1, soit la résolvante de C1 et C2. Si C1 est dans la CNF courante, il est inutile de calculer des résolvantes avec C. Il s'agit d'écrire une fonction qui renvoie vrai si cl1
est incluse dans cl2
:
bool subsume(const cls_t& cl1, const cls_t& cl2);
Ensuite, il faut modifier la fonction resolution
pour:
L'algorithme résultant en pseudo-code est le suivant :
Entrée : cnf l'ensemble initial de clauses;
Variable locale : q la pile des clauses restant à traiter;
Résultat : true si on peut dériver la clause vide, false sinon;
Algorithme :
subsume
qui teste l'inclusion de clauses.subsume
.resolution
existante puis apporter la première modification indiquée, à savoir le test ∄ p' ∈ cnf. p' ⊆ p.resolution
existante puis apporter la seconde modification indiquée, à savoir le test si p' ⊆ p' ' pour chaque p' ' ∈ cnf .Créer un index, appelé index multiple, sous la forme d'un tableau dont les indices sont les littéraux de la CNF et les cases contiennent la liste des clauses contenant le littéral concerné. Cet index peut être utilisé pour trouver facilement les clauses avec lesquelles on peut calculer une résolvante.
Un deuxième index, appelé index simple, peut être créé sous la forme d'un tableau dont les indices sont les littéraux de la CNF et les cases contiennent la liste des clauses telles que leur plus petit littéral est l'indice de la case. Cet index peut être utilisé pour restreindre le nombre de clauses à regarder pour en trouver une qui peut subsumer une clause C. En effet, si C' subsume C, alors le premier littéral de C' est un des littéraux de C.
Plutôt que de stocker les clauses directement dans les index, on stocke l'indice de la clause dans la CNF. Cela permet d'accélérer les opérations de mises à jour des index.
typedef cnf_t::size_type cls_ref_t; typedef typedef vector< set<cls_ref_t> > idx_t;
Cela complique en revanche la gestion de la suppression des clauses: en effet, lorsqu'une clause est supprimée dans la cnf, cela invalide les index des clauses suivantes10). On désactivera donc la suppression de clauses. Afin de pouvoir comparer les performances à la fin du projet, on gardera de côté la version sans index mais avec suppression des clauses subsumées.
void add_clause(cnf_t & cnf, idx_t & idx_simple, const cls_t & c)
qui ajoute une clause dans la cnf et rajoute sa référence (i.e. son numéro de case) dans l'ensemble des clauses de son premier littéral dans idx_simple.
resolution
.bool est_subsumee(const cnf_t & cnf, const idx_t & idx_simple, const cls_t & c)
qui vérifie s'il existe dans la CNF une clause qui subsume la clause c
.
est_subsumee
dans resolution
à la place du premier est d'inclusion (∄ cl' ∈ cnf t.q. cl' ⊆ cl) .void add_clause(cnf_t & cnf, idx_t & idx_simple, idx_t & idx_multiple, const cls_t & c)
cls2string
et cnf2string
, on se limite à l'opérateur operator«
pour cls_t
et cnf_t
;resolution
, détails sur les optimisations “priorité aux petites clauses” et “subsomption”;CHECK
, on fera une simple vérification visuelle.cl1 = { 7, 6, 1, 4, 1};
.