Logique propositionnelle

SAT vs UNSAT

Soit F une formule logique :

• Trouver cette assignation est difficile: NP-complet.
• Vérifier si une interprétation τ ⊨ F est facile (complexité ?)
• Décider si F est contradictoire est aussi difficile: coNP-complet.

Système de preuve

Formellement, un système de preuve est un algorithme f qui prend une formule F et un mot p ∈ Σ^*, la preuve de F en entrée et :

• Toute formule contradictoire admet une preuve valide (complétude)
• f(F,p) renvoie True si F est contradictoire et que p est une preuve valide du fait que F soit contradictoire (correction).
• f(F,p) renvoie False sinon (ie, p n’est pas une preuve valide de F).
• Idéalement, f est en temps polynomial en |F| + |p|.

De nombreux systèmes de preuves

• Systèmes de preuves généraux (toute formule, même dans des logiques plus complexes) :
  • Déduction Naturelle (Gentzen, 1933)
  • Système(s) de Hilbert
  • Calcul des séquents (on verra en Logique du Premier Ordre)
• Systèmes de preuves pour les FNC :
  • Résolution
  • Cutting planes (utilise des propriétés géométriques)
  • Polynomial Calculus etc. (utilise des propriétés algébriques)

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’est un IF-THEN-ELSE!

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 = ∅.

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

É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

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

Bornes inférieures

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

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.

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?