CM2 Flashcards
Méthode de résolution naïve en logique propositionnelle
Essayer toutes les assignations possibles pour les variables (⊤,⊥)
Qu’est-ce qu’une proposition valide ?
Une proposition qui est vraie pour toute assignation possible des variables
Qu’est-ce qu’une proposition insatisfiable ?
Une proposition qui est fausse pour toute assignation possible des variables
Qu’est-ce qu’une proposition non-valide ?
Une proposition qui est fausse pour certaines assignations possibles des variables
Qu’est-ce qu’une proposition satisfiable ?
Une proposition qui est vraie pour certaines assignations possibles des variables
Étapes de la méthode DPLL (Davis-Putnam-Logemann-Loveland)
- Nier la formule initiale
- Clausifier la formule niée
- Appliquer les simplifications possibles
- Appliquer l’algorithme DPLL
Principe du “Splitting” (DPLL)
- S[A := ⊤] est S dans lequel on a supprimé toutes les clauses contenant A et supprimé ¬A des autres clauses
- S[A := ⊥] est S dans lequel on a supprimé toutes les clauses contenant ¬A et supprimé A des autres clauses
- S est insatisfiable si S[A := ⊤] ∧ [A := ⊤] l’est
Simplification possibles (DPLL)
- Clauses unitaires à traiter en priorité
- Clauses pures à traiter en priorité
- Tautologies à supprimer
Algorithme DPLL
- Si S = ∅ :
- Retourner satisfiable
- ∅ ∈ S :
- Retourner insatisfiable
- Si clause unitaire U (resp. ¬U) ∈ S :
- Renvoyer DPLL(S[U := ⊤ (resp. ⊥)])
- Si P (resp. ¬P) pur ∈ S :
- Renvoyer DPLL(S[P := ⊤ (resp. ⊥)])
- Choisir A ∈ S :
- Renvoyer DPLL(S[A := ⊤]) ∨ DPLL(S[A := ⊥])
Étapes de la méthode de Résolution propositionnelle
- Nier la formule initiale
- Clausifier la formule niée
- Appliquer la règle de résolution sur les clausses de Sat et mettre les résolvantes dans S
Règle de résolution
C∨A | ¬A∨C’
______________
C∨C’
Algorithme de Résolution
- Sat = ∅
- Tant que S != ∅
- Choisir C une clause de S
- Enlever C de S
- Si C = ∅ :
- Renvoyer insatisfiable
- Si C ∈ Sat ou C est une tautologie
- Passer à la clause suivante
- Appliquer la résolution sur C et toutes les clauses de Sat
- Rajouter toutes les résolvantes à S
- Rajouter C à Sat
- Renvoyer satisfiable
Étapes de la méthode des tableaux
- Nier la formule initiale
- Appliquer des règles jusqu’à clore toutes les branches
Règle ⊙⊥
⊥
___
⊙
Règle ⊙¬⊤
¬⊤
____
⊙