Principe générale
Soit F = C1 ∧ … ∧ Cm
une FNC :
- On dérive des nouvelles clauses qui sont des conséquences
logiques de F
- une clause D est une
conséquence logique de F si tous les modèles de F doivent aussi être des modèles de
F
- en particulier F est
satisfiable ssi F ∧ D
est satisfiable.
- on note F ⊨ D
- Jusqu’à dériver la clause vide qui n’est pas
satisfiable: on a donc F ⊨ ∅, soit F
contradictoire.
La règle de résolution
Soit C = x ∨ C0
et D = ¬x ∨ D0.
C’est un IF-THEN-ELSE!
- C ∧ D peut se
lire comme : IF x
THEN D0
ELSE C0.
- En particulier, quelque soit la valeur de x, soit C0 soit D0 doit être vrai, ie
C0 ∨ D0
!
Remarques :
- C0 ∨ D0
s’appelle le résolvant de C et D.
- Si F contient C et D alors on a bien F ⊨ C0 ∨ D0.
Cas extrême
- Si C = x et D = ¬x, le résolvant de
C et D est la clause vide ∅!
- C ∧ D est
clairement contradictoire!
Réfutation
Une réfutation de F par
résolution (ie une preuve que F est contradictoire) est une suite
D1, …, Dk
de clauses telles que :
- Pour i < k,
Di + 1 est
le résolvant de deux clauses de F ∪ {D1, …, Di}.
- Dk = ∅.
Exemple: (x∨y∨z) ∧ (x∨¬y) ∨ (¬z∨x∨y) ∨ (¬x∨z∨y) ∧ (¬y∨¬x∨z) ∧ (¬z∨¬x)
- D1 = (x∨y)
par résolution de (x∨y∨z) et
(¬x∨z∨y).
- D2 = x par
résolution de D1 et
(x∨¬y)
- D3 = ¬x ∨ z
par résolution de (¬x∨z∨y) ∧ (¬y∨¬x∨z)
- D4 = ¬x par
résolution de D3 et
(¬z∨¬x)
- D5 = ∅ par résolution de
D2 et D4 !
Correction et Efficacité
La résolution est correcte, ie, si F admet une réfutation {D1, …, Dk}
par résolution, alors F est
contradictoire :
- On a F ⊨ Di
pour tout i ≤ k par
récurrence
- En particulier F ⊨ Dk + 1
soit F ⊨ ∅.
- Soit F
contradictoire!
- On peut aussi efficacement vérifier la correction d’une réfutation
en recalculant les résolvants donnés.
Complétude
La résolution est complète : toute formule FNC
contradictoire admet une réfutation par résolution.
- Plus difficile à prouver que la correction
- On le prouve via un algorithme un peu brutal pour rechercher une
contradiction !
Davis-Putnam Resolution
Soit F une FNC et x une variable de F. On note DP(F,x)
la FNC qui contient :
- toutes les clauses de F ne
contenant pas la variable x
- tous les résolvants possibles sur x
F = (x∨C1) ∧ … ∧ (x∨Cp) ∧ (¬x∨D1) ∧ … ∧ (¬x∨Dq) ∧ E1 ∧ … ∧ Er
Alors DP(F,x) = ⋀i ≤ p⋀j ≤ q(Ci∨Dj) ∧ E1 ∧ … ∧ Er
Toutes clauses de DP(F,x)
sont des conséquences logiques de F obtenu par résolution : si F est satisfiable alors DP(F,x)
l’est aussi.
Équisatisfiabilité
F = (x∨C1) ∧ … ∧ (x∨Cp) ∧ (¬x∨D1) ∧ … ∧ (¬x∨Dq) ∧ E1 ∧ … ∧ Er
DP(F,x) = ⋀i ≤ p⋀j ≤ q(Ci∨Dj) ∧ E1 ∧ … ∧ Er
Si DP(F,x)
est satisfiable alors F est
satisfiable !
Preuve : soit ω un modèle de F, alors :
- ω satisfait E1 ∧ … ∧ Er
évidemment. Si ω satisfait
Ci, Dj pour tous
i ≤ p et j ≤ q alors ω satisfait x ∨ Ci
et ¬x ∨ Dj
aussi, donc ω satisfait F.
- Sinon, supposons que ω ne
satisfait pas Ci pour un
certain i ≤ p.
- Comme ω ⊨ DP(F,x),
ω satisfait (Ci∨D1), …, (Ci∨Dq)?
- En particulier, ω
satisfait D1, …, Dq.
Donc ω ∪ {x ↦ 1}
satisfait ¬x ∨ D1, …, ¬x ∨ Dq.
- Évidemment ω ∪ {x ↦ 1} satisfait x ∨ C1, …, x ∨ Cp.
- Donc ω ∪ {x ↦ 1}
satisfait F!
- On raisonne symétriquement si ω ne satisfait pas Dj pour un
certain i (il faudra mettre
x à 0 dans ce cas).
Complétude de la résolution
Soit F une formule FNC et
x une variable de F.
- F est satisfiable si et
seulement si DP(F,x)
est satisfiable.
- DP(F,x)
contient strictement moins de variable que F.
- On applique Fi + 1 := DP(Fi,xi)
jusqu’à ne plus avoir de variables :
- si Fn
n’a pas de clauses alors F est
satisfiable
- sinon Fn doit
contenir la clause vide : F est contradictoire et on a
une réfutation par dérivation de ce fait !.
while(var(F)):
x=var(F)[0]
F=DP(F,x)
if ∅ in F:
return UNSAT
else:
return SAT
La résolution est complète !
Bornes inférieures
Il existe des formules qui n’ont pas de petites
réfutations.
Pigeon Hole Principle PHPn, m:
avec n pigeons et m boîtes.
- Proposition atomique pi, j,
“le pigeon i va dans la boîte
j”.
- “Chaque pigeon est dans une boîte”. Pour
chaque i, on a ⋁j = 1..m pi, j
- “Chaque boîte contient au plus un pigeon”. Pour tout j
et i < i′ : ¬pi, j ∨ ¬pi′, j
PHPn, n − 1
n’a pas de réfutation en résolution plus petite que 2n/10.
2-SAT et résolution
Une 2-FNC est une formule FNC où
toutes les clauses sont des 2-clauses, ie, elles contiennent deux
littéraux.
(x∨y) ∧ (¬x∨z) ∧ (y∨¬z)
- La résolvante de deux 2-clauses
contient au plus deux littéraux.
- DP(F,x)
ne peut donc pas contenir plus de 4n(n−1) clauses.
- Donc on peut décider si une 2-FNC
est satisfiable (ou trouver une réfutation) en temps polynomial.
SAT Solvers et Résolution
- Clauses apprises par les CDCL SAT Solvers sont dérivables
par résolution (étendue)
- Quand un CDCL SAT Solver retourne UNSAT, c’est qu’il a appris la
clause vide.
- On peut extraire une réfutation par résolution !
- En pratique, on utilise un format un peu plus compact (DRAT) mais qui est
équivalent.
- Une FNC qui n’a pas de petites preuves sera
difficile pour les SAT Solvers.
- On peut vérifier indépendemment une réfutation renvoyée par un SAT
Solver!
Aller plus loin
- Il existe de nombreux autres systèmes de preuves pour les FNC.
- La plupart sont plus puissants que la résolution
mais on ne sait pas les exploiter pour améliorer les SAT Solvers.
- On sait prouver des bornes inférieures exponentielles sur la plupart
de ces systèmes (lié à la question NP ≠ coNP).
- Quid de problème plus généraux ?
- Logiques plus puissantes
- QBF (FNC + ∀,∃)
- Problème d’agrégation / optimisation : MaxSAT, #SAT?