| 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/25 09:05]
ecoquery [Heuristique de choix de clause] |
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 ===== |
| |
| FIXME: en cours de modification | |
| |
| 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: |
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