Problema SAT și rezolvitoarele SAT

Problema SAT (Satisfiability) constă în determinarea dacă există o atribuire de valori de adevăr variabilelor booleene care face ca o formulă logică dată să fie adevărată. Este considerată prima problemă demonstrată NP-completă, fiind fundamentală în informatică teoretică și practică. Rezolvatoarele SAT sunt algoritmi specializați capabili să verifice satisfacibilitatea acestor formule complexe, având aplicații critice în verificarea hardware, planificare automată și inteligența artificială.

Ce trebuie să știi

• Forma CNF: Majoritatea rezolvatoarelor moderne funcționează eficient când formula este în Conjunctive Normal Form (CNF), adică o conjuncție de disjuncții de clauze.
• Complexitate NP-completă: Nu există un algoritm cunoscut care să rezolve orice instanță SAT în timp polinomial. Totuși, în practică, multe instanțe reale sunt rezolvate rapid.
• Algoritmul DPLL: Baza multor rezolvatoare este algoritmul Davis-Putnam-Logemann-Loveland, care combină backtracking-ul cu simplificarea clauzelor și unit propagation.
• Conflict-Driven Clause Learning (CDCL): Tehnica modernă standard care învață din erori (conflicte) pentru a evita repetarea aceleiași căi de explorare, accelerând semnificativ procesul.
• Format DIMACS: Standardul de facto pentru input-ul rezolvatoarelor, folosind un format textual simplu bazat pe numere întregi pentru literali și clauze.

Exemplu concret: Considerăm formula $(x_1 \lor x_2) \land (\neg x_1 \lor x_3)$. Un rezolvator va testa rapid combinații. Dacă alegem $x_1 = \text{True}$, prima clauză este satisfăcută. A doua devine $(\text{False} \lor x_3)$, deci $x_3$ trebuie să fie True. Soluția $(T, ?, T)$ satisface formula, indiferent de $x_2$.

Cum să înveți

1. Implementează un solver simplu: Scrie un mini-solver care aplică doar unit propagation și backtracking basic pentru a înțelege mecanismul de bază înainte de a studia optimizările CDCL.
2. Experimentează cu tool-uri open-source: Folosește rezolvatoare precum MiniSat sau Z3 (de la Microsoft Research) pentru a transforma probleme reale de constrângeri în format SAT și a observa timpul de execuție.
3. Studiază reducerea problemelor: Exersează transformarea problemelor de tip "colorare graf" sau "puzzle logic" în CNF, deoarece abilitatea de modelare este mai valoroasă decât implementarea algoritmului de la zero.