Différences

Ci-dessous, les différences entre deux révisions de la page.

--- enseignement:logique:projet:2015 [2015/11/23 12:29]
ecoquery ancienne révision (2015/11/15 18:50) restaurée
+++ enseignement:logique:projet:2015 [2015/12/15 14:40] (Version actuelle)
ecoquery [Conversion d'une formule en CNF]
@@ Ligne 20: / Ligne 20: @@
 Cette archive est à déposer sur spiral au plus tard le <del>vendredi 13 novembre 2015 à 23h59</del> dimanche 15 novembre 2015 à 23h59.
-La zone de dépôt pour le rendu **intermédiaire** est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=5015156
+La zone de dépôt pour le rendu **intermédiaire** est accessible ici: **dépôt fermé**
 <note tip>Ce rendu intermédiaire concerne les parties 1 (prise en main) et 2 (modélisation) du projet</note>
@@ Ligne 35: / Ligne 35: @@
 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((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)).
+Cette archive est à déposer sur spiral au plus tard le <del>vendredi 18 décembre 2015 à 23h59</del> 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
@@ Ligne 393: / Ligne 393: @@
 <code c++>
 lit_t tseitin(formule f, const map<string, var_t> & m, cnf_t & c, var_t & next);
-cnf_t tseitin(formule f);
+void tseitin(formule f, const map<string, var_t> & m, cnf_t & c);
 </code>
@@ Ligne 399: / Ligne 399: @@
 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 ∨ b)//, m, cl, 3)''
-      * ''tseitin(//a//, cl, 3)''  0 est le lit positif correspondant à //a//, on ajoute rien à cl
+      * ''tseitin(//a//, m, 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
+      * ''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)//
+      * 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, cl = {{7,0,2},{6,1},{6,3}}, 4)'' 4 est le lit positif correspondant à //c//, on ajoute rien à cl
+    * ''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 litéral positif qui code //f//
+    * 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)
@@ Ligne 417: / Ligne 417: @@
 === Exercices ===
-  * Écrire la fonction ''lit_t tseitin(formule, map<string, int>&, cnf_t&, var_t)'' telle que décrite.
+  * Écrire la fonction ''lit_t tseitin(formule, map<string, int>&, 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, map<string, int>&, cnf_t&)'' qui appelle l'autre fonction ''tseitin''.
+  * Écrire la fonction ''void tseitin(formule f, map<string, int>&, 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.
@@ Ligne 432: / Ligne 432: @@
   * 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 entier représentant les littéraux dans l'ordre croissant))
+    * 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.
@@ Ligne 481: / Ligne 481: @@
   * É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.
 <note important>La signature de cette fonction doit comporter des références (''&''), contrairement au fichier ''resolution.cpp'' fourni à l'origine: <code c++>bool directement_impliquee_par(cls_t & c, cnf_t & f);</code></note>
-  * Écrire la fonction ''resolution''.
+  * Écrire la fonction ''unsat''.
-  * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''resolution''.
+  * Écrire les tests unitaires vérifiant le bon comportement de la fonction ''unsat''.
 <note tip>Une clause est équivalente à ⊤ si elle contient un littéral et sa négation. D'après la manière dont son codés les littéraux et les clauses, si p et ¬p sont dans une clause, ils se suivent lorsqu'on parcourt la clause. On peut ainsi détecter les clauses équivalentes à ⊤ via un simple parcours de la clause en comparant le littéral courant à la négation de celui qui vient d'être lu.</note>
 <note important>
-A la fin de cette partie, le projet dispose de toutes les fonctionnalités pour vérifier 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 ''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 quatrième partie du projet.
+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.
 </note>
-===== Optimisations =====
+===== Quatrième partie: optimisations =====
-FIXME A venir FIXME
+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<cls_t>%%'').
+<code>struct cnf_t {
+  vector<cls_t> _clauses;
+};
+vector<cls_t>::const_iterator cbegin(const cnf_t& c);
+vector<cls_t>::const_iterator cend(const cnf_t& c);
+cnf_t cnf(vector<cls_t> cls);
+void add(cnf_t & cnf, cls_t cls);
+unsigned int size(const cnf_t & cnf);
+</code>
+=== 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:
+<code c++>
+struct cnf_t {
+  vector<cls_t> _clauses;
+  vector<vector<unsigned int> > _index;
+}
+</code>
+=== 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'':<code c++>vector<cls_t> resolvantes(const cls_t & cls, const cnf_t & cnf);</code>
+  - 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%%''):
+<code>bool contient(const cls_t & c1, const cls_t & c2);
+</code>
+=== 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//:
+<code>struct cnf_t {
+  vector<cls_t> _clauses;
+  vector<vector<unsigned int> > _index;
+  vector<vector<unsigned int> > _index2;
+};
+</code>
+== 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//):<code c++>bool moins_prioritaire(const cls_t & c1, const cls_t & c2)</code>**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'':<code c++>class compare_clauses {
+public:
+  bool operator() (const cls_t & c1, const cls_t & c2) {
+    return moins_prioritaire(c1,c2);
+  }
+};</code>changer ensuite la déclaration de la file de traitement dans ''unsat'' par <code c++>priority_queue<cls_t, vector<cls_t>, compare_clauses ></code>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''.

Emmanuel COQUERY

Outils de la page

Différences