Logique propositionnelle

Principe générale

Soit F = C₁ ∧ … ∧ C_m 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 ∨ C₀ et D = ¬x ∨ D₀.

C ∧ D ⊨ C₀ ∨ D₀

C’est un IF-THEN-ELSE!

C ∧ D peut se lire comme : IF x THEN D₀ ELSE C₀.
En particulier, quelque soit la valeur de x, soit C₀ soit D₀ doit être vrai, ie C₀ ∨ D₀ !

Remarques :

C₀ ∨ D₀ s’appelle le résolvant de C et D.
Si F contient C et D alors on a bien F ⊨ C₀ ∨ D₀.

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 D₁, …, D_k de clauses telles que :

Pour i < k, D_i + 1 est le résolvant de deux clauses de F ∪ {D₁, …, D_i}.
D_k = ∅.

Exemple: (x∨y∨z) ∧ (x∨¬y) ∨ (¬z∨x∨y) ∨ (¬x∨z∨y) ∧ (¬y∨¬x∨z) ∧ (¬z∨¬x)

D₁ = (x∨y) par résolution de (x∨y∨z) et (¬x∨z∨y).
D₂ = x par résolution de D₁ et (x∨¬y)
D₃ = ¬x ∨ z par résolution de (¬x∨z∨y) ∧ (¬y∨¬x∨z)
D₄ = ¬x par résolution de D₃ et (¬z∨¬x)
D₅ = ∅ par résolution de D₂ et D₄ !

Correction et Efficacité

La résolution est correcte, ie, si F admet une réfutation {D₁, …, D_k} par résolution, alors F est contradictoire :

On a F ⊨ D_i pour tout i ≤ k par récurrence
En particulier F ⊨ D_k + 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∨C₁) ∧ … ∧ (x∨C_p) ∧ (¬x∨D₁) ∧ … ∧ (¬x∨D_q) ∧ E₁ ∧ … ∧ E_r

Alors DP(F,x) = ⋀_i ≤ p⋀_j ≤ q(C_i∨D_j) ∧ E₁ ∧ … ∧ E_r

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∨C₁) ∧ … ∧ (x∨C_p) ∧ (¬x∨D₁) ∧ … ∧ (¬x∨D_q) ∧ E₁ ∧ … ∧ E_r

DP(F,x) = ⋀_i ≤ p⋀_j ≤ q(C_i∨D_j) ∧ E₁ ∧ … ∧ E_r

Si DP(F,x) est satisfiable alors F est satisfiable !

Preuve : soit ω un modèle de F, alors :

ω satisfait E₁ ∧ … ∧ E_r évidemment. Si ω satisfait C_i, D_j pour tous i ≤ p et j ≤ q alors ω satisfait x ∨ C_i et ¬x ∨ D_j aussi, donc ω satisfait F.
Sinon, supposons que ω ne satisfait pas C_i pour un certain i ≤ p.
1. Comme ω ⊨ DP(F,x), ω satisfait (C_i∨D₁), …, (C_i∨D_q)?
2. En particulier, ω satisfait D₁, …, D_q. Donc ω ∪ {x ↦ 1} satisfait ¬x ∨ D₁, …, ¬x ∨ D_q.
3. Évidemment ω ∪ {x ↦ 1} satisfait x ∨ C₁, …, x ∨ C_p.
4. Donc ω ∪ {x ↦ 1} satisfait F!
On raisonne symétriquement si ω ne satisfait pas D_j 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 F_i + 1 := DP(F_i,x_i) jusqu’à ne plus avoir de variables :
- si F_n n’a pas de clauses alors F est satisfiable
- sinon F_n 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 PHP_n, m: avec n pigeons et m boîtes.

Proposition atomique p_i, 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 p_i, j
“Chaque boîte contient au plus un pigeon”. Pour tout j et i < i′ : ¬p_i, j ∨ ¬p_i′, j

PHP_{n, n − 1} n’a pas de réfutation en résolution plus petite que 2^n/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?