Logique
SAT : satisfaction de formules booléennes
Thomas Pietrzak
Licence Informatique
Clauses de Horn
Prolog
Fait : a
But : b1, …, bn
Clause : a :== c1, …, cn
Logique
Fait : a
But : b1 ⋀ … ⋀ bn
Clause : c1 ⋀ … ⋀ cn ⇒ a ≣ ¬c1 ⋁ … ⋁ ¬cn ⋁ a
Motivation
Trouver des variables qui satisfont une formule = résoudre un problème
Peu de variables : facile à faire la table de vérité.
Beaucoup de variables : exponentiel.
SAT
Soit 𝜑 une formule : existe-t-il une valuation v telle que [𝜑 ]v = 1 ?
FNC
Forme normale conjonctive (FNC) : conjonction de disjonctions
('1,1 _ . . . '1,n1 ) ^ · · · ^ ('k,1 _ . . . 'k,n1 )
Littéral : variable propositionnelle ou négation de variable propositionnelle
Classes de complexité
Classe NP
Il existe un algorithme non-déterministe résolvant ce problème en temps polynomial.
Classe NP-complet
Ce problème appartient à NP.
Tous les problèmes de la classe NP se réduisent à ce problème en temps polynomial.
Théorème de Cook
SAT est NP-complet
Problèmes NP-complets
Tous les problèmes NP-complets sont équivalents à SAT.
En résolvant SAT on résout tous les autres problèmes.
3-SAT
SAT avec clauses de 3 variables
Équivalence entre SAT et 3-SAT
(a1 ⋁ a2 ⋁ … ⋁ an) ≣ (a1 ⋁ a2 ⋁ b1) ⋀ (a3 ⋁ ¬b1 ⋁ b2) ⋀ … ⋀ (an-1 ⋁ an ⋁ ¬bn-3)
n-SAT
SAT avec clauses de n variables
Équivalence entre SAT et n-SAT
(a1 ∨ a2 ∨ … ∨ am) ≣ (a1 ∨ a2 ∨ … ∨ an-1 ∨ b1) ∧
(an+1 ∨ …∨ a2n-3 ∨ ¬b1 ∨ b2) ∧ … ∧ (am-n+1 ∨ … ∨ am ∨ ¬bk)
2-SAT
SAT avec clauses de 2 variables
Pas NP-complet (P)
Résolution SAT
Table de vérité
2 possibilités par variable booléenne
Valuations à calculer : au plus 2n
300 variables : 2300, soit plus que le nombre d’atomes dans l’univers (≃ 1080 ≃ 2266)
Il va falloir simplifier…
Simplifications
(a ⋁ a ⋁ …) ≣ (a ⋁ …) : suppression des occurrences multiples
(a ⋁ ¬a ⋁ …) ≣ ⊤ : suppression des clauses contenant des opposés
C’est bien, mais avec ça on n’ira pas loin…
Propagation unitaire
Clause unaire : a ou ¬a
a ⋀ ¬a ⋀ … ≣ ⊥
a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ≣ (b1 ⋁ … ⋁ bn) ⋀ R et v(a) = ⊤
¬a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ≣ (c1 ⋁ … ⋁ cn) ⋀ R et v(a) = ⊥
Élimination des littéraux purs
Littéral pur : littéral qui est soit toujours positif, soir toujours négatif
(a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ≣ (d1 ⋁ … ⋁ dn) ⋀ R et v(a) = ⊤
(¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (¬a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ≣ (d1 ⋁ … ⋁ dn) ⋀ R et v(a) = ⊥
Davis-Putnam (DP)
Résultante
c1 = (a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) c2 = (¬a ⋁ d1 ⋁ d2 ⋁ … ⋁ dn)
Résultante : r = (b1 ⋁ b2 ⋁ … ⋁ bn ⋁ d1 ⋁ d2 ⋁ … ⋁ dn)
c1 ⋀ c2 satisfiable ssi r satisfiable
Démonstration ⇒
Soit a = ⊤ : c2 satisfiable et ¬a = ⊥ ➔ d1 ⋁ d2 ⋁ … ⋁ dn satisfiable, donc r aussi
Soit a = ⊥ : c1 satisfiable et a = ⊥ ➔ b1 ⋁ b2 ⋁ … ⋁ bn satisfiable, donc r aussi
Exemple
(a ⋁ b) ⋀ (a ⋁ ¬c) ⋀ (¬a ⋁ c)
Il faut factoriser a
Exemple
(a ⋁ b) ⋀ (a ⋁ ¬c) ⋀ (¬a ⋁ c)
≣ (a ⋁ (b ⋀ ¬c)) ⋀ (¬a ⋁ c)
Exemple
(a ⋁ b) ⋀ (a ⋁ ¬c) ⋀ (¬a ⋁ c)
≣ (a ⋁ (b ⋀ ¬c)) ⋀ (¬a ⋁ c)
≣ (b ⋀ ¬c) ⋁ c
On calcule la résultante
Exemple
(a ⋁ b) ⋀ (a ⋁ ¬c) ⋀ (¬a ⋁ c)
≣ (a ⋁ (b ⋀ ¬c)) ⋀ (¬a ⋁ c)
≣ (b ⋀ ¬c) ⋁ c
≣ (b ⋁ c) ⋀ (¬c ⋁ c)
On remet en FNC
Exemple
(a ⋁ b) ⋀ (a ⋁ ¬c) ⋀ (¬a ⋁ c)
≣ (a ⋁ (b ⋀ ¬c)) ⋀ (¬a ⋁ c)
≣ (b ⋀ ¬c) ⋁ c
≣ (b ⋁ c) ⋀ (¬c ⋁ c)
≣b⋁c
Algorithme DP
1. Éliminer les clauses unitaires tant qu’il y en a
a ⋀ ¬a ⋀ R ≣ ⊥ ➔ Formule non satisfiable
a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ➔ (b1 ⋁ … ⋁ bn) ⋀ R
¬a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ➔ (c1 ⋁ … ⋁ cn) ⋀ R
Formule vide ➔ Formule satisfiable
2. Éliminer les littéraux purs
(a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ➔ (d1 ⋁ … ⋁ dn) ⋀ R
(¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (¬a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ➔ (d1 ⋁ … ⋁ dn) ⋀ R
3. On simplifie les résultantes
(a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ (¬a ⋁ d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R
➔ (b1 ⋁ b2 ⋁ … ⋁ bn ⋁ d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(¬b ⋁ c)
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(¬b ⋁ c)
➔ (b ⋁ ¬c)^(¬b ⋁ c)
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(¬b ⋁ c)
➔ (b ⋁ ¬c)^(¬b ⋁ c)
➔ ¬c ⋁ c
Exemple
(a ⋁ b)^(¬a ⋁ ¬c)^d^(d ⋁ ¬a)^(¬d ⋁ e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(e ⋁ f)^(¬b ⋁ c ⋁ e ⋁ ¬f)^(¬b ⋁ c)
➔ (a ⋁ b)^(¬a ⋁ ¬c)^(¬b ⋁ c)
➔ (b ⋁ ¬c)^(¬b ⋁ c)
➔ ¬c ⋁ c
➔⊤
Algorithme DP
On n’obtient pas la valuation qui prouve la satisfiabilité.
Problème : simplification des résultantes
(a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ (¬a ⋁ d1 ⋁ d2 ⋁ … ⋁ dn) ≣ b1 ⋁ b2 ⋁ … ⋁ bn ⋁ d1 ⋁ d2 ⋁ … ⋁ dn
Que vaut a ?
Besoin d’un algorithme constructif.
Davis–Putnam–
Logemann–Loveland
(DPLL)
Valuation partielle
F[x/⊥] est la formule F dans laquelle x est évaluée à ⊥
F[x/⊤] est la formule F dans laquelle x est évaluée à ⊤
F est satisfaisable ssi F[x/⊥] est satisfaisable ou F[x/⊤] est satisfaisable.
Propriétés
a[a/⊤] = ⊤ (a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) [a/⊤] = ⊤
a[a/⊥] = ⊥ (a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn)[a/⊥] = (b1 ⋁ b2 ⋁ … ⋁ bn)
¬a[a/⊤] = ⊥ (¬a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn)[a/⊤] = (b1 ⋁ b2 ⋁ … ⋁ bn)
¬a[a/⊥] = ⊤ (¬a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn)[a/⊥] = ⊤
Alternative à résultante
F = (a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ (¬a ⋁ d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R
Recherche par cas
a = ⊤ ➔ F satisfaisable ssi (d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R est satisfaisable
a = ⊥ ➔ F satisfaisable ssi (b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ R est satisfaisable
Arbre de recherche
x est la variable pivot
F[x/⊥] F[x/⊤]
Clauses unitaires
a clause unitaire dans F ⇒ F satisfiable ssi F[x/⊤] satisfiable.
¬a clause unitaire dans F ⇒ F satisfiable ssi F[x/⊥] satisfiable.
(a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn))[a/⊤] ≣ (b1 ⋁ … ⋁ bn)[a/⊤]
(¬a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn))[a/⊥] ≣ (c1 ⋁ … ⋁ cn)[a/⊥]
Élimination des littéraux purs
a présent et ¬a jamais présent dans F ⇒ F satisfiable ssi F[x/⊤] satisfiable.
¬a présent et a jamais présent dans F ⇒ F satisfiable ssi F[x/⊥] satisfiable.
((a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn))[x/⊤] = (d1 ⋁ … ⋁ dn)[x/⊤]
((¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (¬a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn))[x/⊥] = (d1 ⋁ … ⋁ dn )[x/⊥]
Algorithme DPLL
1. Éliminer les clauses unitaires tant qu’il y en a
a ⋀ ¬a ⋀ … ≣ ⊥ ➔ Formule non satisfiable
a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ➔ ((b1 ⋁ … ⋁ bn) ⋀ R)[a/⊤]
¬a ⋀ (¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ R ➔ ((c1 ⋁ … ⋁ cn) ⋀ R)[a/⊥]
Formule vide ➔ Formule satisfiable
2. Éliminer les littéraux purs
(a ⋁ b1 ⋁ … ⋁ bn) ⋀ (a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ➔ ((d1 ⋁ … ⋁ dn) ⋀ R)[a/⊤]
(¬a ⋁ b1 ⋁ … ⋁ bn) ⋀ (¬a ⋁ c1 ⋁ … ⋁ cn) ⋀ (d1 ⋁ … ⋁ dn) ⋀ R ➔ ((d1 ⋁ … ⋁ dn) ⋀ R)[a/⊥]
3. On simplifie les résultantes
(a ⋁ b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ (¬a ⋁ d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R
➔ ((b1 ⋁ b2 ⋁ … ⋁ bn) ⋀ R)[a/⊥]
➔ ((d1 ⋁ d2 ⋁ … ⋁ dn) ⋀ R)[a/⊤]
F
Exemple
(a ⋁ ¬b ⋁ c ⋁ ¬d ⋁ f)^(¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^(¬a ⋁ ¬d)^(b ⋁ c ⋁ d ⋁ ¬e)
F
Exemple F[a/⊤] F[a/⊥]
(a ⋁ ¬b ⋁ c ⋁ ¬d ⋁ f)^(¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^(¬a ⋁ ¬d)^(b ⋁ c ⋁ d ⋁ ¬e)
➔ (¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^ ¬d ^(b ⋁ c ⋁ d ⋁ ¬e)[a/⊤]
F
Exemple F[a/⊥] F[a/⊥]
(a ⋁ ¬b ⋁ c ⋁ ¬d ⋁ f)^(¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^(¬a ⋁ ¬d)^(b ⋁ c ⋁ d ⋁ ¬e)
F[d/⊥]
➔ (¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^ ¬d ^(b ⋁ c ⋁ d ⋁ ¬e)[a/⊤]
➔ (¬b ⋁ ¬c ⋁ ¬f) ^(b ⋁ c ⋁ ¬e)[a/⊤][d/⊥]
F
Exemple F[a/⊥] F[a/⊥]
(a ⋁ ¬b ⋁ c ⋁ ¬d ⋁ f)^(¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^(¬a ⋁ ¬d)^(b ⋁ c ⋁ d ⋁ ¬e)
F[d/⊥]
➔ (¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^ ¬d ^(b ⋁ c ⋁ d ⋁ ¬e)[a/⊤]
➔ (¬b ⋁ ¬c ⋁ ¬f) ^(b ⋁ c ⋁ ¬e)[a/⊤][d/⊥] F[f/⊥]
➔ (b ⋁ c ⋁ ¬e)[a/⊤][d/⊥][f/⊥]
F
Exemple F[a/⊤] F[a/⊥]
(a ⋁ ¬b ⋁ c ⋁ ¬d ⋁ f)^(¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^(¬a ⋁ ¬d)^(b ⋁ c ⋁ d ⋁ ¬e)
F[d/⊥]
➔ (¬b ⋁ ¬c ⋁ ¬d ⋁ e)^(¬b ⋁ ¬c ⋁ d ⋁ ¬f)^ ¬d ^(b ⋁ c ⋁ d ⋁ ¬e)[a/⊤]
➔ (¬b ⋁ ¬c ⋁ ¬f) ^(b ⋁ c ⋁ ¬e)[a/⊤][d/⊥] F[f/⊥]
➔ (b ⋁ c ⋁ ¬e)[a/⊤][d/⊥][f/⊥]
F[b/⊤]
➔ ⊤[a/⊤][d/⊥][f/⊥][b/⊤]