| Les deux révisions précédentes
Révision précédente
Prochaine révision
|
Révision précédente
|
enseignement:logique:projet:2015 [2015/11/24 08:24]
ecoquery [Quatrième partie: optimisations] |
enseignement:logique:projet:2015 [2015/12/15 14:40] (Version actuelle)
ecoquery [Conversion d'une formule en CNF] |
| Cette archive est à déposer sur spiral au plus tard le <del>vendredi 13 novembre 2015 à 23h59</del> dimanche 15 novembre 2015 à 23h59. | 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> | <note tip>Ce rendu intermédiaire concerne les parties 1 (prise en main) et 2 (modélisation) du projet</note> |
| 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. | 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 | La zone de dépôt pour le rendu **final** est accessible ici: http://spiralconnect.univ-lyon1.fr/webapp/activities/activities.jsp?containerId=5015155 |
| 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 : | 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) ⇒ 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) |
| |
| |
| |
| * 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: | * 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. | * 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. | * 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. |
| * É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. | * É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> | <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 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> | <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> | </note> |
| |
| |
| ===== Quatrième partie: optimisations ===== | ===== 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: | L'objectif de cette partie est de rendre plus efficace le solveur résolution naïf, en utilisant les optimisations suivantes: |
| * heuristique de choix de clause | * heuristique de choix de clause |
| |
| ==== Type abstraits pour clause et CNF ==== | ==== Type abstraits pour CNF ==== |
| |
| Afin de pouvoir enrichir facilement les structures de données des clauses et des CNFs, on en fait des types abstraits, c'est à dire que l'on ajoute les fonctions suivantes, qui devront remplacer les utilisations des fonctions/méthodes correspondantes des classes ''%%vector%%'' et ''%%set%%''. | 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>%%''). |
| | |
| === Type abstrait pour les clauses === | |
| | |
| <code>struct cls_t { | |
| set<lit_t> _lits; | |
| } ; | |
| | |
| set<lit_t>::const_iterator cbegin(const cls_t & c); | |
| set<lit_t>::const_iterator cend(const cls_t & c); | |
| cls_t cls(set<lit_t> lits); | |
| void insert(cls_t & c, lit_t l); | |
| bool empty(cls_t & c); | |
| </code> | |
| === Type abstrait pour les CNFs === | |
| |
| <code>struct cnf_t { | <code>struct cnf_t { |
| === Exercices === | === Exercices === |
| |
| - Effectuer les changements indiqués ci-dessus dans ''%%formule.hpp%%'' (replacement des types ''%%cls_t%%'' et ''%%cnf_t%%'' et fonctions additionnelles). Implémenter ces fonctions additionnelles dans ''%%formule.cpp%%''. | - 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. | - Remplacer les appels ''%%xxx.cbegin()%%'', ''%%xxx.cend()%%'', etc, par des appels appropriés à ces fonctions. |
| |
| ==== Indexations des clauses ==== | ==== Indexations des clauses ==== |
| |
| - Construire et maintenir la structure d'index (cnf() et add()) L'index stocke les id des clauses (id = numéro dans le veteur de 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: |
| - Implementer resolvantes, qui utilise l'index | <code c++> |
| - Utiliser resolvantes au lieu de resolvante dans unsat | 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 ==== | ==== 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%%''): | - 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%%''): |
| === Indexation supplémentaire === | === 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//. | 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// | 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 { | <code>struct cnf_t { |
| }; | }; |
| </code> | </code> |
| Bien pense à modifier 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. | == 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 ==== | ==== Heuristique de choix de clause ==== |
| |
| <code> | 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. |
| </code> | |
| | === 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''. |
| | |
| | |
| |
Sauf mention contraire, le contenu de ce wiki est placé sous les termes de la licence suivante : CC Attribution-Noncommercial-Share Alike 3.0 Unported