Outils de la page

Piste:

Différences

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

Lien vers cette vue comparative

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/14 08:38]
ecoquery [Méthode de résolution par ajout de clauses à une CNF] 		enseignement:logique:projet:2015 [2015/12/15 14:40] (Version actuelle)
ecoquery [Conversion d'une formule en CNF]
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 : 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 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)     * 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 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:   * 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.
CC Attribution-Noncommercial-Share Alike 3.0 Unported 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
enseignement/logique/projet/2015.1450078687.txt.gz · Dernière modification: 2015/12/14 08:38 de ecoquery Haut de page