====== Projet de LIF11 2015: vérification d'un additionneur binaire et résolution ====== ===== Introduction ===== Les 4 séances de TP de logique visent à implémenter un programme permettant de vérifier un circuit d'additionneur binaire. Il utilisera pour cela un solveur testant la (non)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 [[http://minisat.se/|MiniSat]]. Cependant, contrairement à MiniSat, le solveur qui sera implémenté en TP utilisera directement le principe de résolution pour prouver l'insatisfiabilité de formules. Un [[http://spiralconnect.univ-lyon1.fr/webapp/forum/forum.html?id=5015157|forum]] est mis à votre disposition pour échanger sur le projet. Attention il ne s'agit pas de déposer du code source pour le mettre à disposition des autres, mais bien de poser / de répondre à des questions autour du projet. ==== Modalités de rendu ==== == Rendu intermédiaire == Le rendu intermédiaire consistera en une archive zip((pas de rar ou autre format exotique)) contenant: * Le contenu de le projet de départ modifié par vos soins pour les deux premières parties. * Un fichier ''etudiants.txt'' contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants). Le nom de l'archive sera de la forme ''//nom1//-//nom2//.zip'' où //nom1// et //nom2// sont les noms des deux étudiants du binôme. Cette archive est à déposer sur spiral au plus tard le vendredi 13 novembre 2015 à 23h59 dimanche 15 novembre 2015 à 23h59. La zone de dépôt pour le rendu **intermédiaire** est accessible ici: **dépôt fermé** Ce rendu intermédiaire concerne les parties 1 (prise en main) et 2 (modélisation) du projet == Rendu final == Le rendu final consistera en une archive .zip ou .tar.gz((pas de rar ou autre format exotique)) contenant: * Le contenu de le projet de départ modifié par vos soins * Un fichier ''etudiants.txt'' contenant les nom(s), prénom(s) et numéro(s) du/des étudiants ayant réalisé le projet (maximum 2 étudiants). * Un fichier au format .pdf d'au maximum 5 pages A4 en police 11 pts((pas de fichier en police 14 ou 16 pts pour faire du remplissage, cela se voit au premier coup d'oeil)), contenant: * une introduction (max. 0,5 page); * une description des difficultés rencontrées, des solutions apportées et une argumentation autour des choix techniques effectués; * une conclusion dans laquelle on pourra indiquer d'un point de vue plus personnel les apports et les manques du projet (max. 1 page). Le nom de l'archive sera de la forme ''//nom1//-//nom2//.zip'' où //nom1// et //nom2// sont les noms des deux étudiants du binôme. Cette archive est à déposer sur spiral au plus tard le vendredi 18 décembre 2015 à 23h59 dimanche 20 décembre 2015 à 23h59((la zone de dépôt sera automatiquement fermée à ce moment)). Il **fortement** recommandé de tester l'accès à la zone de dépôt avant la date butoir((l'excuse "je n'avais pas accès au dépôt" ne sera pas acceptée)). La zone de dépôt pour le rendu **final** est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=5015155 Le non respect de ces consignes entraînera une sanction dans la note du projet. ==== Projet de départ ==== L'archive {{:enseignement:logique:projet:inf3034l-2015-base.zip|}} contient un projet C/C++. Ce projet de départ fourni contient une arborescence de projet avec : * un fichier ''/Lisez-moi.txt'' qui décrit le contenu de l'archive; * un dossier ''/unittest-cpp'' qui est une bibliothèque pour simplifier l'écriture des tests. //Vous n'avez pas à vous intéresser à son contenu//; * un dossier ''/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 : ''main'' est utilisé pour construire le programme ''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 concernant le solveur par résolution. * ''/src/adder.hpp'' et ''/src/adder.cpp'' sont encore quasiment vides et destinés à recevoir vos fonctions concernant la génération de formules permettant de vérifier un additionneur. * une collection d'autres fichiers dont certains seront générés automatiquement. Il n'est pas utile de les lire. Leur principal objectif est de définir une fonction ''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). Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une [[http://forge.univ-lyon1.fr|forge]] avec un hébergement de dépôts [[http://mercurial.selenic.com/|mercurial]] (normalement déjà vu en LIF7). Le projet fourni((qui peut être récupéré via ''hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2015-base'')) peut être poussé vers cette forge. * Pour créer un projet: http://forge.univ-lyon1.fr/projects/new * Pour être ajouté à un projet, un étudiant doit s'être connecté au moins une fois sur http://forge.univ-lyon1.fr. Le manager du projet pourra alors l'ajouter via Configuration -> Membres. * L'url mercurial((pour le push/pull/clone)) de votre projet est accessible depuis Configuration -> Dépôt * Quelques {{:enseignement:maven-forge-ic.pdf|slides}} pour la gestion de projet (regarder la partie forge) * Voir [[:enseignement:aide:forge|l'aide sur la forge]] pour un scénario d'utilisation pour des TPs/projets ==== Organisation du projet ==== Le projet est divisé en quatre grandes étapes qui correspondent grossièrement aux 4 séances de TP prévues : - //Première partie : prise en main//. Les premières fonctions à écrire comme ''numerote'' sont conceptuellement simples mais demandent un réel travail d'immersion et de prise en main du projet. - //Deuxième partie : modélisation//. L'objectif est ici de fabriquer la formule qui correspond à la spécification de l'additionneur binaire à n-bit (c.f. {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}), de lire une implémentation de l'additionneur sous forme de formule, puis de créer une formule permettant de vérifier la correction de cette implémentation. - //Troisième partie : résolution naïve //. L'objectif de cette partie est réaliser un solveur naïf basé sur la méthode de résolution - //Quatrième partie : optimisations//. Il s'agit d'améliorer les performances du solveur en ajoutant des stratégies et des index permettant d'accélérer le processus de résolution. 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. ===== Première partie : prise en main ===== Pour de l'aide sur les bases du C++ utiles à ce TP voir : * [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIF11-15/Intro_Cpp.html|l'introduction au C++]] * [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIF11-15/Code_LIF10_Example/Simple.cpp|le code d'exemple]]. ==== Tests unitaires avec UnitTest++ ==== Le projet est fourni avec la bibliothèque ''[[http://unittest-cpp.sourceforge.net/|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''. === Exercices === * Prendre connaissance et comprendre le contenu du fichier Lisez-moi.txt. Prendre particulièrement attention à ce qu'il est :!: DEMANDE DE NE PAS FAIRE :!:. * Comprendre le test ''TEST(lit_ecrit_formule)''. * Lancer la compilation et l'exécution des tests via ''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. ==== Forme normale conjonctive ==== Les structures codant les clauses et les formules conjonctives (que l'on abrégera désormais CNF pour [[http://fr.wikipedia.org/wiki/Forme_normale_conjonctive|Conjunctive Normal Form]]) sont définies par des ''typedef'' utilisant différents [[http://www.cplusplus.com/reference/stl/|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 cls_t; typedef vector cnf_t; * La classe ''[[http://www.cplusplus.com/reference/stl/vector/|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()''. * La classe ''[[http://www.cplusplus.com/reference/stl/set/|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 [[http://www.cplusplus.com/reference/stl/set/begin/|cet exemple]]. === Exercices sur les clauses === * Avec un itérateur de type ''cls_t::const_iterator'', implémenter la méthode ''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 [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIF11-15/Intro_Cpp.html|l'affichage des éléments d’un conteneur]]. * Écrire un ''TEST''((Ce test ne contient pas de ''CHECK'', on fera une simple vérification visuelle.)) qui crée une clause ''cl1'' contenant les littéraux //1//, //4//, //7// et //6//((Vous pouvez pour cela utiliser la notation des [[http://www.cplusplus.com/reference/std/initializer_list/|initializer_list]] avec par exemple ''cl1 = { 7, 6, 1, 4, 1};''.)) et une autre clause ''cl2'' de votre choix puis les affiche. * Écrire un ''TEST'' avec les vérifications suivantes : * ''CHECK(cl1 != cl2);'' * ''CHECK(cl2 != cl1);'' * ''CHECK(cl1 == cl1);'' * ''CHECK(cl2 == cl2);'' * Vérifier que les quatre tests s'évaluent à ''true''. === Exercices sur CNF === * Avec un itérateur ou avec ''size()'', implémenter la méthode ''ostream& operator <<(ostream& out, const cnf_t& c)''. Cette méthode utilisera l'opérateur précédemment défini pour ''cls_t''. * Ajouter un ''TEST'' pour l'affichage d'une CNF ''c'' contenant les clauses ''cl1'' et ''cl2''. * Écrire une fonction ''bool est_dans(const cls_t& cl, const cnf_t& c)'' permettant de tester l'appartenance d'une clause à une CNF. * Écrire un ''TEST'' pour vérifier notamment que ''est_dans(cl1, c)'' et que ''est_dans(cl2, c)''. ==== Arbre de syntaxe abstraite et litéraux ==== Pour des raisons d'efficacité, il faut éviter de représenter les variables propositionnelles par des chaînes (classe ''[[http://www.cplusplus.com/reference/string/|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 & corresp)'' permettant de numéroter les variables d'une formule. La classe ''[[http://www.cplusplus.com/reference/stl/map/|map]]'' de la STL est un conteneur associatif qui permet, dans le cas de ''map'', de faire correspondre une unique variable à une chaîne((C'est ainsi une fonction partielle dont on définit [[http://fr.wikipedia.org/wiki/Graphe_d%27une_fonction|le graphe]].)). L'algorithme de ''numerote'' est le suivant : * si la formule est une variable * si la variable a déjà un numéro, ne rien faire; * sinon, lui attribuer un numéro (on peut prendre la taille actuelle de ''corresp'' comme numéro) et ajouter la correspondance entre le nom de la variable et ce numéro dans ''corresp''; * sinon, appeler récursivement la fonction de numérotation sur le ou les argument(s). Pour l'efficacité, on représentera également les littéraux (c'est-à-dire des variables avec ou sans négation) par des entiers : * Les //littéraux positifs// sont représentés par les entiers naturels //pairs//. On injecte ainsi //la variable// //p// qui vaut ''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//. * Les //littéraux négatifs// sont représentés par les entiers naturels //impairs//. //Le littéral// //~p// vaut ainsi ''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'', 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. === Exercices sur les map === * Regarder et comprendre le code de la fonction ''string formule2string(formule f)'' de transformation des formules en chaînes de caractères. * Écrire la méthode ''void numerote(formule f, map & m)''. On inspirera pour cela de ''formule2string'' ainsi que de [[http://www.cplusplus.com/reference/stl/map/operator%5B%5D/|l'exemple d'utilisation de map]]. * Écrire un test unitaire qui vérifie le nombre de variables comptées lors de la numérotation de quelques formules. === Exercices sur les littéraux === * Écrire la fonction ''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. * Écrire la fonction ''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. * Écrire la fonction ''var_t lit2var(lit_t l)'' qui prend un littéral en argument et retourne sa variable. * Écrire la fonction ''bool positif(lit_t l)'' qui renvoie ''true'' si le littéral passé en argument est un littéral positif. * Tester ces fonctions avec ''UnitTest++''. Par exemple, on aura ''var2lit(2,true) = var2lit(2) = 4'', ''var2lit(2,false) = 5'', ''neg(4) = 5'', ''neg(5)=4'', ''lit2var(4) = 2'', ''lit2var(5) = 2'', ''positif(4) = true'' et ''positif(5) = false''. Plus généralement, on a les égalités suivantes entre les fonctions ''var2lit'', ''positif'' et ''lit2var'' : ''∀ v∈var_t, ∀ b∈ bool, positif(var2lit(v,b)) = b ∧ lit2var(var2lit(v,b)) = v'' 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é. ===== Deuxième partie : modélisation ===== ==== Substitutions ==== 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'' qui à chaque variable substituée associe la formule qui la remplacera. ''formule.hpp'' défini le type ''subs_t'' comme alias de ''map''. === Exercice === * En s'appuyant sur la définition de l'application d'une substitution (cf {{:enseignement:logique:logique-memo1.pdf|mémo 1}}), coder la fonction récursive formule applique(formule f, const subs_t & 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 modifiée par l'application de la substitution. Attention, afin de simplifier la gestion de la mémoire, on suppose que chaque formule n'est utilisée qu'une seule fois, ce qui signifie que lorsqu'une variable est remplacée, elle l'est par une copie de la formule associée et pas par la formule directement. ==== Génération de la spécification d'un additionneur ==== 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 2 * n entrées sont données par les variables ''p1'' ... ''p//n//'' et ''q1'' ... ''q//n//'' et que les (//n+1//) sorties sont codées par les formules //A1// ... //An//, //B// (//B// est le dernier bit de a somme, celui avec le poids le plus fort). On utilisera les formules suivantes qui expriment la somme et la retenue pour un additionneur qui calcule la somme de trois entrée à 1 bit : * S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}) * R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}). La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit: * Additionneur 1-bit : on retourne le vecteur V=[A1,B] de taille //2// avec * A1 = S [ p1/t, q1 / u, ⊥ / w], on calcule cette formule en construisant la substitution [ p1/t, q1 / u, ⊥ / w] en en l'appliquant à S avec la méthode ''applique'' * B = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, sauf que c'est R qui est modifiée et plus S. * Additionneur //n//-bits : soit V'=[A'1, ... , A'n-1,B'] le vecteur de taille //n// obtenu pour un additionneur de taille //n-1//, on va construire le vecteur résultat V =[A'1, ... , A'n-1, A'n,B'] de taille //n+1// * A//1// à A//n-1// : on ne change rien : A'//i//=A//i// ; * A//n// = S [ p//n// / t, q//n// / u, B' / w ], B' est le dernier bit de sortie d'un additionneur à //n-1//-bit que l'on va l'additionner aux bits p//n//et q//n//. Autrement dit, B', est la retenue de la somme de p//n-1//et q//n-1// quand on pose l'addition ; * B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à //n-1//-bits, //i.e.// B' est le bit de poids le plus fort du vecteur V'. C'est-à-dire que B est la retenue de l'addition de p//n// et q//n// avec la retenue de p//n-1// et q//n-1//. === Exercices === * Écrire la fonction ''additionneur'' suivante qui construira les formule A//i//, en commençant par A//1// jusqu'à A//n//, puis A//n+1// (i.e. la dernière valeur de B):vector additionneur(int taille); * Écrire les tests unitaires associé et vérifier pour //n=2// que votre formule est bien celle d'un additionneur binaire ==== Génération d'une formule pour vérifier la correction d'un additionneur ==== Une fois obtenues les formules de spécification de l'additionneur //n//-bits via ''additionneur'', on peut les comparer à celle de l'additionneur à vérifier (que l'on appelera additionneur //candidat//). Pour cela, il suffit de vérifier que chaque sortie de l'additionneur candidat est équivalente à la sortie correspondante de la spécification. === Exercice === Coder la fonction ''formule_verifier_additionneur'' qui génère une formule valide si et seulement si l'additionneur candidat passé en argument est correct. Si on suppose que les sorties de l'additionneur //n//-bits candidat sont notées A'//1//, ... , A'//n//, A'//n+1//, on peut générer la spécification A//1//, ... , A//n//, A//n+1// via la fonction ''additionneur'', puis construite la formule ( (A//1// ⇔ A'//1//) ∧ ... ∧ (A//n// ⇔ A'//n//) ∧ (A//n+1// ⇔ A'//n+1//) ). Cette dernière formule est valide si et seulement si l'additionneur candidat est correct. La fonction ''main'' dans ''main.cpp'' utilisera la fonction ''formule_verifier_additionneur'' si on passe l'argument ''--check-adder'' en ligne de commande. La partie suivante vise à implémenter un solveur vérifiant la non satisfiabilité d'une formule (i.e. la validité de sa négation) via la méthode de résolution. ==== Pour tester en ligne de commande ==== Afin de vous permettre de tester en ligne de commande l'état actuel du projet vous pouvez ajouter le code suivant à la fin de "formule.cpp": //////////////////////////////////////////////////////////////////////////////// // Code pour la réécriture en CNF équivalente d'une formule cnf_t cnf_union(const cnf_t& lhs, const cnf_t& rhs){ cnf_t res = lhs; res.reserve(lhs.size() + rhs.size()); res.insert(res.end(), rhs.cbegin(), rhs.cend()); return res; } cnf_t cnf_product(const cnf_t& lhs, const cnf_t& rhs){ //product E x F = { (x union y) | x in E /\ y in F} cnf_t res; cls_t xy; for (auto& x : lhs){ for (auto& y : rhs){ xy.clear(); set_union(x.cbegin(), x.cend(), y.cbegin(), y.cend(), std::inserter(xy, xy.end()));// res.push_back(xy); } } return res; } // Déclaration pour les appels mutuellement recursifs cnf_t rewriteDNF(formule f, const map & corresp, bool pos=true); cnf_t rewriteCNF(formule f, const map & c, bool pos) { cnf_t res; switch (f->op) { case o_variable:{ res = { {var2lit(c.find(* (f->nom))->second, pos)} }; return (res); } case o_non: return rewriteDNF(f->arg, c, !pos); break; case o_et: { cnf_t c1 = rewriteCNF(f->arg1, c, pos); cnf_t c2 = rewriteCNF(f->arg2, c, pos); return cnf_union(c1, c2); } case o_ou: { cnf_t c1 = rewriteCNF(f->arg1, c, pos); cnf_t c2 = rewriteCNF(f->arg2, c, pos); return cnf_product(c1, c2); } case o_implique: { cnf_t c1 = rewriteDNF(f->arg1, c, !pos); cnf_t c2 = rewriteCNF(f->arg2, c, pos); return cnf_product(c1, c2); } case o_equivaut: { cnf_t c1a = rewriteDNF(f->arg1, c, !pos); cnf_t c2a = rewriteCNF(f->arg2, c, pos); cnf_t ca = cnf_product(c1a, c2a); cnf_t c1b = rewriteCNF(f->arg1, c, !pos); cnf_t c2b = rewriteDNF(f->arg2, c, pos); cnf_t cb = cnf_product(c1b, c2b); return cnf_union(ca, cb); } } } cnf_t rewriteDNF(formule f, const map & c, bool pos) { cnf_t res; switch (f->op) { case o_variable:{ res = { {var2lit(c.find(* (f->nom))->second, pos)} }; return (res); } case o_non: return rewriteCNF(f->arg, c, !pos); break; case o_et: { cnf_t c1 = rewriteDNF(f->arg1, c, pos); cnf_t c2 = rewriteDNF(f->arg2, c, pos); return cnf_product(c1, c2); } case o_ou: { cnf_t c1 = rewriteDNF(f->arg1, c, pos); cnf_t c2 = rewriteDNF(f->arg2, c, pos); return cnf_union(c1, c2); } case o_implique: { cnf_t c1 = rewriteCNF(f->arg1, c, !pos); cnf_t c2 = rewriteDNF(f->arg2, c, pos); return cnf_union(c1, c2); } case o_equivaut: { cnf_t c1a = rewriteCNF(f->arg1, c, !pos); cnf_t c2a = rewriteDNF(f->arg2, c, pos); cnf_t ca = cnf_union(c1a, c2a); cnf_t c1b = rewriteDNF(f->arg1, c, !pos); cnf_t c2b = rewriteCNF(f->arg2, c, pos); cnf_t cb = cnf_union(c1b, c2b); return cnf_product(ca, cb); } } } Il faut également remplacer ''main.cpp'' par la version suivante: {{:enseignement:logique:projet:main.cpp|}}. Ajouter la ligne suivante après les ''#include'' dans le fichier ''formule.hpp'': #include Enfin il faut ajouter la ligne suivante après la déclaration de ''writeDimacs'' dans ''formule.hpp'': // fonction de transformation en CNF, version equivalente exponentielle //////// cnf_t rewriteCNF(formule f, const map & corresp, bool pos=true); Il est ensuite possible d'appeler ''./verifier --no-tseitin --use-minisat'' pour tester la validiter d'une formule, ou ''./verifier --check-adder --no-tseitin --use-minisat'' pour vérifier un additionneur. Il y a un bug dans la fonction ''writeDimacs'' (dans ''formule.cpp''): il faut remplacer la ligne out << ( (positif(l)?1:-1) * lit2var(l) ) << " ";par la ligne out << ( (positif(l)?1:-1) * (1+lit2var(l)) ) << " "; Le projet de base sur la forge et l'archive {{:enseignement:logique:projet:inf3034l-2015-base.zip|}} ont été mis à jour en intégrant ces modifications ===== Troisième partie: solveur naïf ===== ==== Conversion d'une formule en CNF ==== La [[http://en.wikipedia.org/wiki/Tseitin-Transformation|transformation de Tseitin]] (//c.f.// TD du 19/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: * //tseitin(p) = (p,vide)// * //tseitin(¬f)// : * soit //(p',c') = tseitin(f)// * renvoyer //(¬p',c')// * //tseitin(f1 ∨ f2)// : * soient //(p1,c1) = tseitin(f1)//, //(p2,c2) = tseitin(f2)// et //p// un nouveau littéral * renvoyer //(p, (¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2) ∧ c1 ∧ c2)// * tseitin(f1 ∧ f2) : * soient //(p1,c1) = tseitin(f1)//, //(p2,c2) = tseitin(f2)// et //p// un nouveau littéral * renvoyer //(p, (p ∨ ¬p1 ∨ ¬p2) ∧ (¬p ∨ p1) ∧ (¬p ∨ p2) ∧ c1 ∧ c2)// * tseitin(f1 ⇒ f2) : * soient //(p1,c1) = tseitin(f1)//, //(p2,c2) = tseitin(f2)// et //p// un nouveau littéral * renvoyer //(p, (¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2) ∧ c1 ∧ c2)// * tseitin(f1 ⇔ f2) : * soient //(p1,c1) = tseitin(f1)//, //(p2,c2) = tseitin(f2)// et //p// un nouveau littéral * renvoyer //(p, (¬p ∨ ¬p1 ∨ p2) ∧ (¬p ∨ p1 ∨ ¬p2) ∧ (p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1 ∨ ¬p2) ∧ c1 ∧ c2)// La CNF équisatifiable finale est obtenue comme suit: * soit //(l,c) = tseitin(f)// * la CNF est //l ∧ c// 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 fraiches. Ainsi en C/C++ on définira les deux fonctions : lit_t tseitin(formule f, const map & m, cnf_t & c, var_t & next); void tseitin(formule f, const map & m, cnf_t & c); 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)//, m, cl, 3)'' * ''tseitin(//a//, m, cl, 3)'' 0 est le lit positif correspondant à //a//, on ajoute rien à cl * ''tseitin(//b//, m, cl, 3)'' 2 est le lit positif correspondant à //b//, on ajoute rien à cl * on a les 2 branches de //(a ∨ b)// on ajoute donc //(¬p ∨ p1 ∨ p2) ∧ (p ∨ ¬p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3}}'' et 6 est le littéral positif qui code //(a ∨ b)//. Au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 4. * ''tseitin(c, m, cl = {{7,0,2},{6,1},{6,3}}, 4)'' 4 est le lit positif correspondant à //c//, on ajoute rien à cl * on a les 2 branches de //(a ∨ b) ⇒ c// on ajoute donc //(¬p ∨ ¬p1 ∨ p2) ∧ (p ∨ p1) ∧ (p ∨ ¬p2)// à cl pour obtenir ''cl = {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5}}'' et 8 est le littéral positif qui code //f// (au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 5, mais comme on ne tirera plus de variable fraîche par la suite, cela ne se voit pas) 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//. La fonction ''tseitin'' a ''m'' comme paramètre **en lecture seule** (déclaration ''**const** map & m''), or si vous utilisez ''m[]'', comme pour un tableau, vous allez avoir une erreur assez peu intelligible car ''[[http://en.cppreference.com/w/cpp/container/map/operator_at|[] ]]'' **est une méthode qui peut modifier m**. A la place, il faut utiliser ''[[http://en.cppreference.com/w/cpp/container/map/find|find]]'' qui est une méthode en lecture seule. === Exercices === * Écrire la fonction ''lit_t tseitin(formule, map&, cnf_t&, var_t&)'' telle que décrite. * Écrire les tests unitaires pour vérifier chacun des cas du ''switch (f->op)'' de la fonction précédente. * Écrire la fonction ''void tseitin(formule f, map&, cnf_t&)'' qui appelle l'autre fonction ''tseitin''. * Écrire les tests unitaires vérifiant le nombre de clauses et de littéraux générés lors de cette transformation. Si le programme ''minisat'' est disponible en ligne de commande sur votre machine, vous pouvez dès à présent tester votre approche en utilisant l'argument ''--use-minisat''. Le programme appellera ''minisat'' pour tester la (non-)satisfiabilité de la formule de vérification ==== Calcul de résolvantes ==== Une fois la CNF obtenue, il est possible d'utiliser la méthode de //résolution// pour tester son insatisfiabilité. Cette méthode consiste à combiner des clauses entre elles pour essayer de déduire la clause vide. La clause obtenue par combinaison de deux clauses est appelée //résolvante// 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 : * Une première fonction ''pivot'', étant données deux clauses //cl1// et //cl2//, trouve un littéral //l// de //cl1// tel que //¬l// est présent dans //cl2//. Cette fonction prend les deux clauses en paramètre, ainsi qu'un paramètre ''l_pivot'' qui est un littéral passé par référence. Si //l// existe, la fonction reverra ''true'' et affectera ''l_pivot'' à //l//. Sinon la fonction renvoie simplement ''false''. 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: * les représentations des littéraux sont triées dans les clauses((i.e. les itérateurs parcourent les entiers représentant les littéraux dans l'ordre croissant)) * si n représente un littéral //l//, alors //¬l// est représenté par n+1 ou n-1. * Une seconde fonction ''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. bool pivot(cls_t c1, cls_t c2, lit_t & l_pivot); cls_t resolvante(cls_t c1, cls_t c2, lit_t l_pivot); === Exercices === * Écrire la fonction ''pivot''. * Écrire la fonction ''resolvante''. * Écrire les tests unitaires pour ces fonctions. ==== Méthode de résolution par ajout de clauses à une CNF ==== Implémenter l'algorithme de recherche d'un arbre de résolution par ajout de clauses dans une CNF (voir cours/TD). On utilisera par exemple une [[http://www.cplusplus.com/reference/queue/queue/|pile]] avec un ''vector'' 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 :\\ * //∀ cl ∈ cnf// * //q.push( cl )// * //cnf = ∅// * **tant que** (//¬q.empty( )//) * //cl = q.pop( )// * **si** (//cl≡⊥//) * **renvoyer** //true// * **si** (//cl ≢⊤// et //cl ∉ cnf//) * //∀ cl2 ∈ cnf// * //cl_r = resolvante(cl, cl2)// * //q.push( cl_r )// * //cnf.push( cl )// * **fin tant que** * **renvoyer** //false// Le prototype formel C++ attendu est le suivant : bool unsat(cnf_t f); === Exercices === * Écrire la fonction ''tautologie'' qui vérifie si une clause est valide (auquel cas il est n'est pas intéressant de l'ajouter à la CNF) * Écrire la fonction ''directement_impliquee_par'' qui vérifie si une clause est dans la CNF. Une version plus optimisée (voir partie 4) consistera à vérifier si la clause ne contient pas une clause présente dans la CNF. Si une clause est directement impliquée par la CNF, il est inutile de la traiter. La signature de cette fonction doit comporter des références (''&''), contrairement au fichier ''resolution.cpp'' fourni à l'origine: bool directement_impliquee_par(cls_t & c, cnf_t & f); * Écrire la fonction ''unsat''. * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''unsat''. 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. A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier l'insatisfiabilité (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 ''unsat'' 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 quatrième partie du projet. ===== Quatrième partie: optimisations ===== L'objectif de cette partie est de rendre plus efficace le solveur résolution naïf, en utilisant les optimisations suivantes: * indexation des clauses * suppression des clauses contenant au moins une autre clause présente dans la CNF * heuristique de choix de clause ==== Type abstraits pour CNF ==== Afin de pouvoir enrichir facilement les structures de données des CNFs, on en fait un type abstrait, c'est à dire que l'on ajoute les fonctions suivantes, qui devront remplacer les utilisations des fonctions/méthodes correspondantes la classe ''%%cnf_t%%'' (qui était jusqu'ici un ''%%vector%%''). struct cnf_t { vector _clauses; }; vector::const_iterator cbegin(const cnf_t& c); vector::const_iterator cend(const cnf_t& c); cnf_t cnf(vector cls); void add(cnf_t & cnf, cls_t cls); unsigned int size(const cnf_t & cnf); === Exercices === - Effectuer les changements indiqués ci-dessus dans ''%%formule.hpp%%'' (replacement du type ''%%cnf_t%%'' et fonctions additionnelles). Implémenter ces fonctions additionnelles dans ''%%formule.cpp%%''. - Remplacer les appels ''%%xxx.cbegin()%%'', ''%%xxx.cend()%%'', etc, par des appels appropriés à ces fonctions. ==== Indexations des clauses ==== On souhaite à présent construire un index afin de trouver directement les clauses avec lesquelles on peut trouver une résolvante pour une clause //c// donnée. Cet index va indiquer pour chaque littéral quelles sont les clauses qui le contiennent. Pour faciliter la gestion mémoire, on numérote les clauses en utilisant l'indice auquel elles apparaissent dans le vecteur ''%%_clauses%%''. L'index stockera ainsi pour chaque littéral une liste des numéros des clauses qui le contiennent: struct cnf_t { vector _clauses; vector > _index; } === Exercices === - Modifier la structure de CNF conformément au code ci-dessus. Mettre à jour les fonctions ''add(...)'' et ''cnf(...)'' pour créer et maintenir cet index. - Implementer resolvantes, qui utilise l'index pour calculer toutes les résolvantes d'une clause ''cls'' avec les clauses d'une CNF ''cnf'':vector resolvantes(const cls_t & cls, const cnf_t & cnf); - Modifier ''unsat'' pour utiliser ''resolvantes'' au lieu de ''pivot'' et ''resolvante''. ==== Suppression des clauses contenant au moins une autre clause présente dans la CNF ==== On peut remarquer que si une clause //c// est présente dans la CNF, il est inutile de traiter des clauses qui contiennent //c//. On souhaite utiliser cette remarque pour éviter d'ajouter de telles clauses. === Exercice === - Modifier ''%%directement_impliquee_par(...)%%'' pour tester non si la clause appartient à la CNF, mais si une clause de la CNF est contenue dans la clause testée. On pourra pour cela implémenter la fonction suivante (à déclarer dans ''%%formule.hpp%%'' et à coder dans ''%%formule.cpp%%''): bool contient(const cls_t & c1, const cls_t & c2); === Indexation supplémentaire === On peut remarquer que les clauses contenues dans la clause //c// que l'on veut tester possèdent tous leur littéraux en commun avec //c//. En particulier, leur premier littéral est dans //c//. Créer un deuxième index pour stocker pour chaque littéral //l// les (numéro des) clauses //c// telles //l// est le plus petit littéral dans //c//: struct cnf_t { vector _clauses; vector > _index; vector > _index2; }; == Exercices == - Modifier la structure ''cnf_t'' ainsi que les fonctions ''%%cnf(...)%%'' et ''%%add(...)%%'' pour refléter ce changement. - Utiliser ensuite cet index dans ''%%directement_impliquee_par(...)%%'' pour ne parcourir que les clauses dont le premier littéral apparaît dans la clause à tester. ==== Heuristique de choix de clause ==== On peut remarquer que combiner de petites clauses pour obtenir de nouvelles résolvantes a plus de chances de mener à la clause vide. On souhaite donc changer l'ordre de la file de traitement des clauses en donnant la priorité aux clauses plus petites. Pour cela on va utiliser le conteneur ''[[http://www.cplusplus.com/reference/queue/priority_queue/|priority_queue]]'' de la STL. Ce conteneur nécessite une fonction de comparaison permettant de savoir si une clause est plus prioritaire qu'une autre. === Exercices === - Implémenter la fonction suivante qui renvoie ''true'' si //c1// est moins prioritaire que //c2// (//i.e.// //c1// est plus grande en taille que //c2//):bool moins_prioritaire(const cls_t & c1, const cls_t & c2)**Remarque:** ''priority_queue'' utilise un ordre //total// et //strict//. Il faut donc: * avoir un deuxième critère de comparaison si les clauses ont la même taille (par exemple comparer le numéro du plus petit littéral qui n'est pas commun aux deux clauses) * renvoyer ''false'' si c1 et c2 sont les mêmes clauses - Ajouter le code suivant avant la fonction ''unsat'':class compare_clauses { public: bool operator() (const cls_t & c1, const cls_t & c2) { return moins_prioritaire(c1,c2); } };changer ensuite la déclaration de la file de traitement dans ''unsat'' par priority_queue, compare_clauses >Il pourra être nécessaire de changer quelques appels de fonction, l'API de ''priority_queue'' étant légèrement différente de celle de ''vector''.