SAT și SMT — De la satisfiabilitatea booleană la verificarea automată a programelor

De ce SAT și SMT?

În informatică, o întrebare revine constant: există o soluție care satisface toate condițiile mele?

• Există o asignare de variabile care face un circuit să funcționeze corect?
• Poate un program să ajungă într-o stare greșită?
• E sigură o configurație de rețea?

SAT și SMT sunt cele două răspunsuri fundamentale la această întrebare — unul clasic (SAT), celălalt modern și practic (SMT).

Partea 1: SAT — Satisfiabilitatea booleană

1.1 Problema SAT

Problema SAT (Boolean Satisfiability Problem) e prima problemă demonstrată NP-completă (Cook, 1971).

Definiție: Fiind dată o formulă booleană, există o asignare de valori true/false pentru variabile care o face adevărată?

Exemplu:

$$(x \lor y) \land (\lnot x \lor z) \land (\lnot y \lor \lnot z)$$

O soluție: $x = true, y = false, z = false$.

Verificare:

• $(true \lor false) = true$ ✅
• $(\lnot true \lor false) = (false \lor false) = false$ ❌

Nu funcționează. Să încercăm $x = true, y = true, z = false$:

• $(true \lor true) = true$ ✅
• $(\lnot true \lor false) = (false \lor false) = false$ ❌

De fapt, soluția e $x = false, y = true, z = true$:

• $(false \lor true) = true$ ✅
• $(\lnot false \lor true) = (true \lor true) = true$ ✅
• $(\lnot true \lor \lnot true) = (false \lor false) = false$ ❌

Hm, nici asta. Un SAT solver ar găsi rapid că de fapt soluția e $x = true, y = false, z = true$:

• $(true \lor false) = true$ ✅
• $(\lnot true \lor true) = (false \lor true) = true$ ✅
• $(\lnot false \lor \lnot true) = (true \lor false) = true$ ✅

1.2 De ce contează SAT?

SAT e omniprezent pentru că orice problemă NP poate fi redusă la SAT — deci un solver SAT rapid rezolvă orice problemă din NP.

1.3 Algoritmul CDCL

SAT solverele moderne (MiniSAT, Glucose, CryptoMiniSAT) folosesc CDCL — Conflict-Driven Clause Learning.

Pașii algoritmului:

1. Alege o variabilă neasignată → îi atribuie o valoare
2. Propagă — aplică regula: dacă o clauză are toate variabilele false
   în afară de una, aceea trebuie să fie true (unit propagation)
3. Dacă toate variabilele sunt asignate → SAT
4. Dacă apare un CONFLICT (o clauză e falsă):
   a) Analizează conflictul → învață o nouă clauză
   b) Backtrack la punctul de decizie corect
   c) Adaugă clauza învățată (împiedică același conflict)
5. Dacă nu mai sunt variabile de încercat → UNSAT

De ce e revoluționar CDCL:

Învață din greșeli. Dacă solver-ul explorează o ramură care duce la conflict, învață o clauză nouă care previne explorarea aceleiași ramuri în viitor.

Exemplu de învățare:

Să zicem că am asignat x=true, y=false și asta duce la conflict.
Solver-ul învață: (¬x ∨ y) — "nu mai face x=true ȘI y=false simultan"
Data viitoare, dacă x=true, propagă automat y=true.

1.4 Forma CNF (Conjunctive Normal Form)

SAT solverele lucrează cu formule în CNF — conjuncție de clauze, fiecare clauză fiind o disjuncție de literali:

$$(x_1 \lor \lnot x_2 \lor x_3) \land (x_2 \lor x_4) \land (\lnot x_1 \lor \lnot x_4)$$

Transformarea Tseitin: Orice formulă booleană poate fi transformată în CNF în timp polinomial, introducând variabile auxiliare.

Partea 2: SMT — Satisfiabilitatea cu teorii

2.1 De ce nu ajunge SAT?

Lumea reală nu e doar true/false. Un program are:

• Întregi: $x + y > 10$
• Șiruri: $s_1 \cdot s_2 = \text{"hello"}$
• Vectori: $a[i] = 5$
• Operații pe biți: $x & 0xFF = 0$

În SAT, ai putea reprezenta un întreg pe 32 de biți ca 32 de variabile booleene, dar ar fi ineficient — ai avea nevoie de circuite aritmetice cu sute de porți.

SMT (Satisfiability Modulo Theories) extinde SAT cu teorii de fond — teorii matematice specializate care știu să lucreze direct cu domeniul respectiv.

2.2 Teorii de fond

Cuantificatorul QF: "Quantifier-Free" — fără cuantificatori ($\forall, \exists$), doar constrângeri.

2.3 Cum funcționează un SMT solver

Arhitectura clasică DPLL(T) — un SAT solver care deleagă teorii la solvere specializate:

Problema SMT (ex: x > 5 ∧ y < 10 ∧ x + y = 20)
        ↓
   Abstractizare booleană (înlocuiesc constrângerile cu variabile booleene)
        ↓
   SAT solver (CDCL) — alege o combinație booleană
        ↓
   Theory solver — verifică dacă combinația e consistentă
        ↓
   Dacă DA → SAT (găsită soluția)
   Dacă NU → învață o clauză nouă → reia

Exemplu concret:

Constrângeri:
   C1: x > 5
   C2: y < 10
   C3: x + y = 20

Pas 1: Abstragem boolean: C1=true, C2=true, C3=true
Pas 2: Theory solver (aritmetic):
   - x > 5, y < 10, x + y = 20
   - Din x + y = 20 ⇒ x = 20 - y
   - 20 - y > 5 ⇒ y < 15
   - Combinat cu y < 10 ⇒ y ∈ (-∞, 10)
   - x = 20 - y > 10
   - Soluție posibilă: x = 14, y = 6  (sau x = 12, y = 8, etc.)
Pas 3: SAT! ✅

2.4 Solvere SMT cunoscute

2.5 Aplicații practice ale SMT

Verificare securitate (AWS Zelkova)

Amazon verifică politicile IAM cu Z3:

Permite accesul la resursa S3:bucket/secrete?
Politica: Allow DACĂ (user = "admin" SAU IP-range = 10.0.0.0/8)
User = "guest", IP = 10.0.1.5

Z3 verifică: există vreo cale de acces neautorizat?
→ Dacă UNSAT, configurația e sigură

Testare simbolică (Symbolic Execution)

În loc să rulezi programul cu valori concrete, rulezi cu simboluri:

def f(x):
    if x > 10:
        return x * 2
    else:
        return x + 5

Cu SMT, poți întreba: "Există un $x$ astfel încât $f(x) > 100$?"

SMT răspunde: $x > 50$ (cazul $x > 10$) sau $x > 95$ (cazul $x \le 10$). Deci $x > 50$ e condiția suficientă.

Planificare și optimizare

De la orar școlar la rutare în rețele — SMT poate găsi soluții cu mii de variabile.

Partea 3: SAT vs SMT — comparație

Când folosești SAT?

• Verificare de circuite hardware
• Probleme pur combinaționale
• Când ai nevoie de viteză maximă
• Când problema poate fi reprezentată eficient în booleeni

Când folosești SMT?

• Verificare de programe (cu variabile, array-uri, string-uri)
• Securitate și control acces
• Optimizare cu constrângeri mixte
• Când ai nevoie de expresivitate mare

Partea 4: Exemple practice

4.1 Problemă SAT în format DIMACS (CNF)

c Exemplu: (x1 OR NOT x2) AND (x2 OR x3) AND (NOT x1 OR NOT x3)
p cnf 3 3
1 -2 0
2 3 0
-1 -3 0

Un SAT solver (ex: glucose -model) răspunde:

SAT
-1 -2 3 0

($x_1 = false, x_2 = false, x_3 = true$)

4.2 Problemă SMT în format SMT-LIB

(set-logic QF_LIA)
(declare-const x Int)
(declare-const y Int)
(assert (> x 5))
(assert (< y 10))
(assert (= (+ x y) 20))
(check-sat)
(get-model)

Z3 răspunde:

sat
(model
  (define-fun x () Int 14)
  (define-fun y () Int 6)
)

4.3 Problemă în Python cu Z3

from z3 import *

x = Int('x')
y = Int('y')

solver = Solver()
solver.add(x > 5)
solver.add(y < 10)
solver.add(x + y == 20)

if solver.check() == sat:
    print(solver.model())  # [x = 14, y = 6]
else:
    print("unsat")

Partea 5: Limitări teoretice

5.1 NP-completitudinea SAT

Problema SAT e NP-completă — nu se cunoaște un algoritm polinomial. În cel mai rău caz, timpul de execuție crește exponențial cu numărul de variabile.

În practică însă, SAT solverele moderne rezolvă probleme cu milioane de variabile datorită CDCL și euristicilor inteligente.

5.2 Indecidabilitatea SMT

Pentru teorii cu cuantificatori peste întregi, problema devine indecidabilă (Teorema lui Gödel — nu există un algoritm care să răspundă corect "da" sau "nu" pentru orice formulă).

SMT solverele pot răspunde și unknown.

5.3 Explozia exponențială

O problemă cu 100 de variabile booleene are $2^{100} \approx 10^{30}$ combinații. Solverele moderne nu explorează toate combinațiile — folosesc CDCL, propagare, euristici — dar în cel mai rău caz, timpul e exponențial.

Concluzie

SAT și SMT sunt unele dintre cele mai practice instrumente de verificare formală. SAT e fundația teoretică; SMT e extensia care face verificarea utilă pentru programe reale.

Pentru aprofundare, vezi articolele despre Z3 (implementarea concretă a unui SMT solver) și Verificarea Matematică a Software-ului (contextul mai larg).

Referințe

• Cook, S. The Complexity of Theorem-Proving Procedures. STOC, 1971.
• Davis, M., Logemann, G., & Loveland, D. A Machine Program for Theorem Proving. CACM, 1962.
• Marques-Silva, J. & Sakallah, K. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE TCAD, 1999.
• De Moura, L. & Bjørner, N. Z3: An Efficient SMT Solver. TACAS, 2008.
• Barrett, C. et al. The SMT-LIB Standard: Version 2.7. 2024.
• Biere, A. et al. Handbook of Satisfiability. IOS Press, 2021.