====== Projet de logique ====== ** Année 2012-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, 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 {{:enseignement:logique:logique-memo4.pdf|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'à : * soit l'obtention de la clause vide et on conclue que l'ensemble initial de clauses est //insatisfiable//; * soit l'impossibilité de déduire de nouvelles clauses et on conclue que l'ensemble initial de clauses est //satisfiable//; ==== 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 vendredi 11 janvier 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/spiral/spiral.html#/activities/goto_folder/1992964 Le non respect de ces consignes entraînera une sanction dans la note du projet. ==== Projet de départ ==== L'archive {{:enseignement:logique:lif11-2012-enonce.zip|}} (v1.1) 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/resolution.hpp'' et ''/src/resolution.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). ==== Organisation du projet ==== Le projet est divisé en trois 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 la résolution//. La résolution travaillant sur des clauses, il faut tout d'abord récursivement convertir une formule arbitraire en forme normale conjonctive. Une version naïve de la méthode de résolution est ensuite à réaliser - //Troisième partie : optimisations//. Il s'agit d'améliorer les performances de la résolution en ajoutant des stratégies et des index permettant de produire les résolvantes plus efficacement. 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//. ===== Première partie : prise en main ===== Pour de l'aide sur les rudiments du C++ voir [[http://liris.cnrs.fr/romuald.thion/files/Enseignement/LIFC++/Intro_Cpp.html|l'introduction au C++]] et [[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. * 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 : bases de la résolution ===== ==== Conversion d'une formule en CNF ==== La [[http://en.wikipedia.org/wiki/Tseitin-Transformation|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: * //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 frâiches. 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); 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. 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//. === 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 résolvantes ==== 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//. On traite le cas où un tel littéral n'existe pas en renvoyant -1((Une autre convention est possible, comme renvoyer une paire ou passer un booléen par référence)). 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 entier 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. 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); === 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 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 resolution(const cnf_t& cls); === Exercices === * Écrire la fonction ''resolution''. * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''resolution''. 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 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. ===== Troisième partie: optimisations ===== ==== Priorité aux petites clauses ==== Les résolvantes avec des petites clauses sont celles qui ont le plus de chances de: - générer la clause vide - générer une clause qui subsume des clauses existantes. Pour cela, on utilise une [[http://www.cplusplus.com/reference/queue/priority_queue/|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 #include 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> q; //ordre par défaut priority_queue, 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; } === Exercices === * Sur le modèle donné, écrire la fonction ''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; * Modifier la fonction ''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; * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''resolution'' en donnant priorité aux petites clauses. ==== Subsomption ==== 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: - Ne pas ajouter à la CNF des clauses qui sont subsumées par (qui contiennent) au moins une clause déjà dans la CNF; - Lors de l'ajout d'une clause dans la CNF, supprimer de la CNF les clauses qui sont subsumées strictement (qui contiennent strictement) la clause ajoutée. 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 :\\ * //∀ cl ∈ cnf// * //q.push( cl )// * //cnf = ∅// * **tant que** (//¬q.empty( )//) * //cl = q.pop( )// * **si** (//cl≡⊥//) * **renvoyer** //true// * **si** (//cl ≢⊤// et //∄ cl' ∈ cnf// t.q. //cl' ⊆ cl//) * //∀ cl2 ∈ cnf// * //cl_r = resolvante(cl, cl2)// * //q.push( cl_r )// * //∀ cl3 ∈ cnf // * **si** //cl ⊆ cl3// * //cnf.erase(cl3)// * //cnf.push( cl )// * **fin tant que** * **renvoyer** //false// === Exercices === * Écrire la fonction ''subsume'' qui teste l'inclusion de clauses. * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''subsume''. * Copier et renommer la fonction ''resolution'' existante puis apporter la //première// modification indiquée, à savoir le test //∄ p' ∈ cnf. p' ⊆ p//. * Vérifier la non-régression de votre modification avec les tests unitaires existants. * (optionnel) Évaluer la différence de performance entre les deux versions. * Copier et renommer la fonction ''resolution'' existante puis apporter la //seconde// modification indiquée, à savoir le test **si** //p' ⊆ p' '// pour chaque // p' ' ∈ cnf //. * Vérifier la non-régression de de votre modification avec les tests unitaires existants. * (optionnel) Évaluer la différence de performance entre les trois versions. ==== Indexation ==== 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. === Structure d'index === 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 > 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 suivantes((ou, si on a procédé par échange de la clause à supprimer et de la dernière clause de la cnf por éviter le décalage, cela invalide l'index de la clause échangée)). 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. === Exercices === * Construction et utilisation de l'index simple: * Écrire une fonction 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. * Désactiver la suppression des clauses dans ''resolution''. * Écrire des tests unitaires pour vérifier son bon fonctionnement. * Écrire une fonction 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''. * Écrire des tests unitaires pour vérifier son bon fonctionnement. * Utiliser ''est_subsumee'' dans ''resolution'' à la place du premier est d'inclusion (//∄ cl' ∈ cnf// t.q. //cl' ⊆ cl//) . * Construction de l'index multiple et utilisation pour le calcul du pivot: * Modifier la fonction add_clause en ajoutant un paramètre correspondant à l'index multiple:void add_clause(cnf_t & cnf, idx_t & idx_simple, idx_t & idx_multiple, const cls_t & c) * Écrire des tests unitaires pour vérifier son bon fonctionnement. * Utiliser l'index multiple pour trouver les résolvantes à ajouter aux clauses à traiter en utilisant la remarque suivante: une clause //C// peut être combinée avec une autre clause //C'// en utilisant un littéral //l ∈ C// comme pivot si et seulement si //C'// se trouve référencée dans l'index multiple dans la case du littéral //¬ l// * Comparer les performance des deux versions du solveur "resolution": * Celle qui supprime les clauses de la CNF qui sont subsumée par la clause qui va être ajoutée * Celle qui ne fait pas cette suppression, mais qui utilise les index pour le premier test de subsomption (//∄ cl' ∈ cnf// t.q. //cl' ⊆ cl//) et le calcul des résolvantes. ===== Références ===== * Jean Gallier: //[[http://www.cis.upenn.edu/~jean/gbooks/logic.html|Logic for Computer Science: Foundations of Automatic Theorem Proving]]//, en particulier le [[http://www.cis.upenn.edu/~cis510/tcl/chap4.pdf|chapitre 4]]. ===== Mise à jour du projet ===== * v0, 18/10/12 : version initiale par EC; * v1, 21/10/12 : alignement sujet/code et réorganisation par RT; * v11, 23/10/12 : suppression des méthodes de ''cls2string'' et ''cnf2string'', on se limite à l'opérateur ''operator<<'' pour ''cls_t'' et ''cnf_t''; * v12, 20/11/12 : correction mineure Tseitin et exemple afférant; * v13, 04/12/12 : ajout du pseudo-code de lalgo de ''resolution'', détails sur les optimisations "priorité aux petites clauses" et "subsomption"; * v14, 20/12/12 : ajout de détails concernant l'utilisation des index