====== Projet de logique 2013 ====== ===== Introduction ===== 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 [[http://minisat.se/|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. ==== Modalités de rendu ==== Le rendu 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). Cette archive est à déposer sur spiral au plus tard le dimanche 22 décembre 2013 à 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 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. ==== Projet de départ ==== L'archive {{:enseignement:logique:projet:lif11-2013-enonce.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'' 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 : ''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. * 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]]. Le projet fourni((qui peut être récupéré via ''hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2013-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 : bases de SAT//. Les algorithmes de test SAT travaillant sur des clauses, il faut tout d'abord récursivement convertir une formule arbitraire en forme normale conjonctive. Une version naïve du test de satisfiabilité est ensuite à réaliser - //Troisiè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}}). - //Quatrième partie : optimisations//. Il s'agit d'améliorer les performances du solveur en ajoutant des stratégies et des index permettant de couper l'arbre de recherche. 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/LIFC++/Intro_Cpp.html|l'introduction au C++]] * [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIFC++/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'', écrire une fonction pour l'affichage de clauses, ayant la signature ''string cls2string(const cls_t& cl)''. 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/LIFC++/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()'', écrire une fonction d'affichage pour les CNFs, ayant la signature ''string cnf2string(const cnf_t& c)''. implémenter la méthode ''ostream& operator<<(ostream& out, const cnf_t& c)''. 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++''. 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 : un solveur SAT simple ===== ==== Conversion d'une formule en CNF ==== La [[http://en.wikipedia.org/wiki/Tseitin-Transformation|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: * //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); cnf_t tseitin(formule f); 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 à cl * ''tseitin(//b//, 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)// * ''tseitin(c, 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 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//. 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 ''cnf_t tseitin(formule f)'' qui appelle ''numerote'' et 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. ==== Calcul de la valeur courante d'une CNF ==== 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 à vrai * FAUX si la variable est affectée à faux * INDETERMINEE si la variable n'est pas affectée === Exercices === * Écrire la fonction ''val_t valeur_lit(vector, 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. * Écrire la fonction ''val_t valeur_clause(vector, cls_t)'' qui étant utilise la fonction précédente pour déterminer la valeur de la clause.\\ Remarque: si la clause contient //un// littéral qui vaut VRAI, alors elle sa valeur est VRAI. Si //tous// les littéraux de la clause valent FAUX, alors la clause vaut FAUX. Sinon sa valeur est INDETERMINEE. * Écrire la fonction ''val_t valeur_cnf(vector, cnf_t)'' qui utilise la fonction précédente pour déterminer la valeur de la CNF.\\ Remarque: si la CNF contient //une// clause qui vaut FAUX, alors elle vaut FAUX. Si //toutes// ses clauses valent VRAI, alors elle vaut VRAI. Sinon sa valeur est INDETERMINEE. 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 ==== Exploration de l'espace de recherche ==== Écrire la fonction récursive bool cherche(vector & valeurs, var_t suiv, const cnf_t & cnf); qui renvoie ''true'' si ''cnf'' est satisfiable, sachant que: * ''valeur'' contient les valeurs des variables * ''suiv'' 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: - si ''suiv'' est supérieur à la taille de ''valeurs'', alors évaluer la CNF et renvoyer VRAI si elle est satisfaite. - sinon: - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' - Appeler récursivement la fonction avec ''suiv+1'' - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' - sinon mettre la valeur de ''suiv'' à FAUX dans ''valeurs'' - Appeler à nouveau récursivement la fonction avec ''suiv+1'' - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' - sinon la CNF n'est pas satisfiable pour l'affectation courante: remettre la valeur de ''suiv'' à INDETERMINEE, puis renvoyer ''false''. Dans la définition de la fonction ''cherche'', on suppose que la longueur du tableau ''vector & valeurs'' passé en paramètre est //égale au nombre de variables (différentes) de la cnf//. Ainsi: * il n'y a pas besoin de faire de ''push_back'' ou de ''resize'', l'allocation et l'initialisation est à la charge de la fonction qui appelle ''cherche'' ; * on peut déterminer que toute les variables ont été affectées en comparant ''suiv'' et ''valeurs.size()''. Modifier la fonction main de façon à: - transformer la formule lue en CNF équisatisfiable; - initialiser un tableau de valeurs à INDETERMINEE pour chaque identifiant de variable; - appeler la fonction cherche et afficher le résultat. 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. ===== Troisième partie: modélisation ===== Dans cette partie, on modélise un additionneur //n//-bits (la spécification, cf {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}) qui est utilisé pour vérifier un additionneur dont la représentation est donnée dans un fichier. ==== 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. === 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 map & 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. ==== Formules de spécification ==== 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=[B,A1] 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'[B',A'n-1,...,A'1] le vecteur de taille //n// obtenu pour un additionneur de taille //n-1//, on va construire le vecteur résultat V =[B,An,An-1,...,A1] 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, c'est le bit de poids le plus fort du vecteur V', c'est la retenue de l'addition de p//n// et q//n// evec 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 1 :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 * 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 ¬( (A//1// ⇔ A'//1//) ∧ ... ∧ (A//n// ⇔ A'//n//) ∧ (B//n// ⇔ B'//n//) ). On testera la satisfiabilité de cette formule: si elle est insatisfiable, l'additionneur passé en argument est correct. Vous disposez de la fonction ''lit_formule**__s__**'' qui fonctionne similairement à ''lit_formule'', mais en lit plusieurs d'un coup et renvoie un ''vector'' (//c.f.// ''parser.hpp''). 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. La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle. ===== Quatrième partie: optimisations ===== ==== Couper l'arbre de recherche ==== 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. === Exercice === 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. ==== Indexation des clauses ==== 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. === Exercices === * Écrire une fonction vector > indexe_clauses(const cnf_t& cnf) qui renvoie une telle structure initialisée en fonction de la forme conjonctive passée en argument. * Écrire une fonction bool contient_insatisfaite(var_t variable, const vector& valeurs,const vector >& index_clauses) * ''index_clauses'' est la structure d'indexation des clauses * ''variable'' est le numéro d'une variable. On appelle l le littéral correspondant à variable et prenant la valeur FAUX * ''valeurs'' est le tableau des valeurs affectées aux variables * la fonction renvoie true si une des clauses contenant l s'évalue à FAUX dans l'interprétation courante (i.e. valeurs). * Remplacer les appels à ''valeur_cnf'' dans ''cherche'' par une utilisation de la fonction ''contient_insatisfaite''. ==== Propagation unitaire ==== 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 L//1// ∨ ... ∨ L//k//. Si tous les littéraux de cette clause valent FAUX, sauf un certain L//j// qui vaut INDETERMINEE, alors cette clause ne pourra s'évaluer à VRAI que si L//j// 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 L//j//: si L//j// est un littéral positif, V doit prendre la valeur VRAI, si L//j// est un littéral négatif, elle doit prendre la valeur FAUX. On peut également remarquer que si L//j// se voit affecter la valeur VRAI, alors ¬L//j// a pour valeur FAUX. Cela peut avoir deux conséquences: * La CNF peut s'évaluer à FAUX auquel cas on sait que les valeurs choisies pour les variables n°1 à //n// ne permettront pas de montrer que la CNF est satisfiable; * Une ou plusieurs autres clauses peuvent devenir unitaires, ceci entrainant l'affectation d'autres variables et ainsi de suite jusqu'à ce que la CNF s'évalue à FAUX ou qu'aucune clause ne soit rendue unitaire. 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. === Exercices === - Créer une nouvelle fonctionvector propage(lit_t lit, vector & valeurs, cnf_t & cnf, vector > & 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: * Initialiser le ''vector'' résultat à un ''vector'' vide * Initialiser un ''vector'' contenant au départ ''lit''. Cette structure contiendra la liste courante des littéraux que l'on veut affecter à VRAI. * Tant qu'il reste des littéraux à traiter: * Retirer un littéral L des littéraux à traiter * Vérifier si le littéral a déjà une valeur. Si c'est le cas, ne rien faire. * Ajouter la variable V correspondant à L dans le vector résultat * Affecter la bonne valeur à V * Utiliser l'index pour accéder aux clauses à vérifier (pour propagation unitaire ou contradiction((i.e. la clause s'évalue à FAUX)) ) * Pour chaque clause unitaire trouvée, ajouté le littéral qui n'a pas de valeur dans les littéraux à traiter * Si une clause s'évalue à FAUX alors la CNF aussi et la propagation unitaire s'arrête. On remet alors à INDETERMINEE la valeur des variables du ''vector'' résultat, puis on renvoie un vector vide. * Renvoyer le résultat - Modifier la fonction cherche de façon à utiliser ''propage'' au lieu de ''contient_insatisfaite'' * En particulier, bien penser à remettre la valeur des variables affectée par ''propage'' à INDETERMINEE lors des retours arrière. ===== Références ===== * Jean Gallier: //[[http://www.cis.upenn.edu/~jean/gbooks/logic.html|Logic for Computer Science: Foundations of Automatic Theorem Proving]]//. ===== Compiler sous MacOSX / Windows ===== ==== Sous Windows ==== Faire fonctionner le projet sous Windows nécessite l'utilisation de [[http://www.cygwin.com/|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''. ==== Sous MacOSX ==== 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 [[http://brew.sh/|Homebrew]], [[http://www.macports.org/|Macports]] ou encore [[http://fink.thetis.ig42.org/|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. ===== Mise à jour du projet ===== * v0, 09/10/13 : version initiale par EC; * v1, 14/10/13: maj date rendu, dépôt spiral, projet initial et lien forge. * v2, 15/10/13: ajout de fonctions: lit2var et positif. * v3, 16/10/13: informations compilation Windows/MacOSX * v4, 16/11/13: aide sur erreur ''m[]'' qui n'est pas const * v5, 24/11/13: modif partie sur additionneur * v6, 18/12/13: mise à jour de la description de la fonction ''cherche'' dans sa première version