SAT Solvers
Florent Capelli
28 Janvier 2025
Pour utiliser des solvers optimisés !
Le problème SAT : étant donné un formule F en FNC, trouver un modèle τ de F ou répondre UNSAT si la formule est contradictoire.
def sat(F):
n = len(var(F))
for t in range(2**n):
if all(satClause(t,C) for C in F):
return t
raise UNSATC’est un problème NP-complet, on ne connaît pas d’algorithme meilleur que O(2|var(F)|) dans le pire cas (bruteforce).
def sat(F):
n = len(var(F))
for t in range(2**n):
if all(satClause(t,C) for C in F):
return t
raise UNSATAlgorithme naïf, complexité O(2n) pour toute formule UNSAT, même :
F ≡ x1 ∧ ¬x1 ∧ G(x2,…,xn)
Un SAT solver résoud efficacement SAT dans de nombreux cas pratique en bruteforçant plus intelligemment.
F ≡ F[x←0] ∨ F[x←1]
Soit C = ⋁iℓi une clause. C[x←b] est :
Exemple: C = x ∨ ¬y ∨ z
Quelle variable/valeur choisir pour la formule suivante ?
(x) ∧ (¬x∨z∨y) ∧ (x∨¬z∨¬y) ∧ ...
x = 1 bien sûr !
F ≡ (x) ∧ (¬x∨¬z) ∧ (¬x∨z∨¬y) ∧ G
def sat(F, l): # F est une FNC, l une assignation d'une partie de ses variables
# Cas d'arrêt : plus de clauses, tout est satisfait par l
if F is empty:
return True
# Propagation unitaire
while units(F):
F = F[units(F)]
l = l + units(F)
# Cas d'arrêt : une clause n'est plus satisfiable !
if ∅ in F:
return False
# Branchement
x = pickvar(F,l)
b = pickval()
l[x] = b
if sat(F[x=b], l):
return True
else:
l[x] = b-1
return sat(F[x=1-b], l)Comment satisfaire : F ≡ (x∨z∨¬y) ∧ (x∨¬z∨y) ∧ (¬y∨¬z) ∧ (z∨¬y)
Si un litéral ℓ apparaît dans F mais ¬ℓ n’apparaît pas, on peut forcer ℓ à 1: on ne peut que enlever des clauses.
On dit que ℓ est pur et on fait une propagation de littéral pur.
Si le but est de trouver tous les modèles, alors on ne peut pas faire d’élimination de littéraux purs.
# F est une FNC,
# l une assignation d'une partie de ses variables
def sat(F, l):
# Cas d'arrêt : plus de clauses, tout est satisfait par l
if F is empty:
return True
# Propagation des littéraux unitaires et purs
while units(F) != [] and purs(F) !=[]:
F = F[units(F)][purs(F)]
l = l + units(F) + purs(F)
# Cas d'arrêt : une clause n'est plus satisfiable !
if ∅ in F:
return False
# Branchement
x = pickvar(F,l)
b = pickval()
l[x] = b
if sat(F[x=b], l):
return True
else:
l[x] = b-1
return sat(F[x=1-b], l)watched literal de C, rien à faireOn maintient F de façon la plus paresseuse possible.
On sait que ¬z peut être propagé !
Comment bien choisir x et b pour essayer de trouver rapidement une solution ? on utilise une heuristique !
Une heuristique peut être vue comme une fonction h(ℓ,F) ∈ ℚ+ qui donne un score à chaque litéral non assigné de F.
On choisira le litéral qui a le plus grand score.
Idée générale : quand on trouve un conflit, on apprend une nouvelle clause permettant de détecter le conflit plus tôt.
(x1∨x4)∧
(x1∨¬x3∨¬x8)∧
(x1∨x8∨x12)∧
(x2∨x11)∧
(¬x7∨¬x3∨x9)∧
(¬x7∨x8∨¬x9)∧
(x7∨x8∨¬x10)∧
(x7∨x10∨¬x12)
Analyse du conflit: il suffit de mettre x7 ← 1, x3 ← 1, x8 ← 0 pour dériver ce conflit !
Cela veut dire que la clause ¬x7 ∨ ¬x3 ∨ x8 est satisfaite par tous les modèles de F. On peut l’ajouter et backtracker au choix 2 !
Clauses apprises par conflit :
La recherche concernant les SAT solvers est encore très active et se concentre sur :
Tous ces outils prennent en entrée un fichier au format DIMACS (ou une variation) décrivant textuellement une FNC : ∧ ¬∨
c ceci est un commentaire
c en-tête, on déclare une cnf avec trois variables et deux clauses
p cnf 3 2
c première clause: x1 ∨ x2 ∨ ¬x3
1 2 -3 0
c deuxième clause : ¬x2 ∨ x3
-2 3 0Pour une construction plus programmatique, on peut utiliser PySAT.