CM2

Question 1

Méthode de résolution naïve en logique propositionnelle

Answer 1

Essayer toutes les assignations possibles pour les variables (⊤,⊥)

Question 2

Qu’est-ce qu’une proposition valide ?

Answer 2

Une proposition qui est vraie pour toute assignation possible des variables

Question 3

Qu’est-ce qu’une proposition insatisfiable ?

Answer 3

Une proposition qui est fausse pour toute assignation possible des variables

Question 4

Qu’est-ce qu’une proposition non-valide ?

Answer 4

Une proposition qui est fausse pour certaines assignations possibles des variables

Question 5

Qu’est-ce qu’une proposition satisfiable ?

Answer 5

Une proposition qui est vraie pour certaines assignations possibles des variables

Question 6

Étapes de la méthode DPLL (Davis-Putnam-Logemann-Loveland)

Answer 6

• Nier la formule initiale
• Clausifier la formule niée
• Appliquer les simplifications possibles
• Appliquer l’algorithme DPLL

Question 7

Principe du “Splitting” (DPLL)

Answer 7

• 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

Question 8

Simplification possibles (DPLL)

Answer 8

• Clauses unitaires à traiter en priorité
• Clauses pures à traiter en priorité
• Tautologies à supprimer

Question 9

Algorithme DPLL

Answer 9

• 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 := ⊥])

Question 10

Étapes de la méthode de Résolution propositionnelle

Answer 10

• 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

Question 11

Règle de résolution

Answer 11

C∨A | ¬A∨C’
______________
C∨C’

Question 12

Algorithme de Résolution

Answer 12

• 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

Question 13

Étapes de la méthode des tableaux

Answer 13

• Nier la formule initiale
• Appliquer des règles jusqu’à clore toutes les branches

Question 14

Règle ⊙_⊥

Answer 14

⊥
___
⊙

Question 15

Règle ⊙_¬⊤

Answer 15

¬⊤
____
⊙

Question 16

Règle ⊙

Answer 16

¬P P
_____
⊙

Question 17

Règle α_¬¬

Answer 17

¬¬P
_____
P

Question 18

α_∧

Answer 18

P∧Q
______
P, Q

Question 19

β_¬∧

Answer 19

¬(P∧Q)
________
¬P ∣ ¬Q

Question 20

β_∨

Answer 20

P∨Q
_____
P ∣ Q

Question 21

α_¬∨

Answer 21

¬(P∨Q)
________
¬P, ¬Q

Question 22

β_⇒

Answer 22

P⇒Q
______
¬P ∣ Q

Question 23

α_¬⇒

Answer 23

¬(P⇒Q)
________
P, ¬Q

Question 24

β_⇔

Answer 24

P⇔Q
_____________
¬P, ¬Q ∣ P, Q

Question 25

β_¬⇔

Answer 25

¬(P⇔Q)
_____________
¬P, Q ∣ P, ¬Q