| 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/12/10 16:45]
ecoquery [Conversion d'une formule en CNF] |
enseignement:logique:projet:2015 [2015/12/15 14:40] (Version actuelle)
ecoquery [Conversion d'une formule en CNF] |
| 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)//. Au passage, on incrémente le numéro de la prochaîne variable fraîche qui devient 4. | * 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> |
| |
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