(Categoria _Algoritmi_, Autor _Cosmin Negruşeri_)

h2. Introducere
 

Problema satisfiabiltăiţii, notată prescurtat cu $SAT$, cere determinarea existenţei pentru o formulă booleană <tex> \phi </tex> a unei artibuiri satisfiabile. O formulă booleană <tex> \phi </tex> este compusă din $variabile$ logice <tex> (x_{1}, x_{2}, ...) </tex>, $operatori$ logici ( <tex> \wedge </tex> şi,  <tex> \vee </tex> sau, <tex> \sim </tex> non, <tex> \rightarrow </tex> implicaţie şi <tex> \leftrightarrow </tex> echivalenţă), şi $paranteze$. O atribuire de valori booleene pentru variabilele acestei expresii se numeşte $atribuire satisfiabilă$ dacă evaluarea expresiei după atribuirea valorilor dă ca rezultat valoarea de adevăr $adevărat$. De acum încolo vom folosi pentru simplitate valorile <tex> 1 </tex> şi <tex> 0 </tex> în loc de $adevărat$ şi $fals$.
Un exemplu de formulă ar fi <tex> \phi = ((x_{1} \rightarrow x_{2}) \vee \sim((\sim x_{1} \leftrightarrow x_{3}) \vee x_{4})) \wedge \sim x_{2} </tex>. Aceasta are atribuirea satisfiabilă <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex> pentru că <tex> \phi = ((0 \rightarrow 0) \vee \sim((\sim 0 \leftrightarrow 1) \vee 1)) \wedge \sim 0 = (1 \vee \sim (1 \vee 1)) \wedge 1 = (1 \vee 0) \wedge 1 = 1</tex>.

h2. Forme normale ale formulelor logice
 

Orice formulă booleană poate fi transformată în două forme:
* $Forma normal conjunctivă$ în care expresia este exprimată ca o conjuncţie de propoziţii, iar fiecare propoziţie este formată din o disjuncţie de $literali$. Un $literal$ este o variabilă care poate fi sau nu negată. Un exemplu de expresie în forma normal conjunctivă ar fi: <tex> (x_{1} \vee \sim x_{1} \vee \sim x_{2}) \wedge (x_{3} \vee x_{2} \vee x_{4}) \wedge (\sim x_{1} \vee \sim x_{3} \vee \sim x_{4}) </tex> care are pe <tex> (x_{1} \vee \sim x_{1} \vee \sim x_{2}) </tex> ca primă propoziţie cu literalii <tex> x_{1} </tex>, <tex> \sim x_{1} </tex>, <tex> \sim x_{2} </tex>.
* $Forma normal disjunctivă$ este formată ca o disjuncţie de propoziţii, fiecare dintre aceste propoziţii fiind o conjuncţie de literali. Un exemplu de o asemenea formulă ar fi următoarea: <tex> (x_{1} \wedge x_{2} \wedge x_{3}) \vee (x_{1} \wedge \sim x_{2} \wedge x_{3}) \vee (x_{1} \wedge \sim x_{2} \wedge \sim x_{3}) \vee (\sim x_{1} \wedge x_{2} \wedge \sim x_{2}) </tex>.

h2. SAT, 3-SAT, 2-SAT
 

Problema $SAT$ este $NP-completă$. Defapt, este prima problemă $NP-completă$ găsită. Stephen Cook a demonstrat $NP-completitudinea$ ei în 1971. Pe vremea aceea nu se ştia nici măcar că problemele $NP-complete$ există. Această problemă rămâne $NP-completă$ chiar dacă restricţionăm expresiile la unele care în forma normal conjunctivă au doar trei literali. Problema satisfiabilităţii pentru asemenea expresii se numeşte $3SAT$, şi multe probleme pot fi demonstrate a fi $NP-complete$ prin reducerea la această problemă. Din fericire, problema $2SAT$, adică cea pentru care în fiecare propoziţie există doar $2$ literali se poate rezolva eficient. Restul articolului va prezenta trei metode de rezolvare a problemei $2SAT$ şi câteva aplicaţii ale acesteia la concursuri de programare.

Un exemplu de problemă $2SAT$ ar fi satisfiabilitatea formulei <tex> (x_{1} \vee \sim x_{2}) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee x_{2}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. Această formulă este satisfăcută de valorile <tex> \langle x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = 1 \rangle </tex>. Pentru a satisface întreaga expresie trebuie ca în fiecare propoziţie cel puţin unul din cei doi literali să aibă valoarea de adevăr $1$.

h3. Soluţie $O(M * 2^N^)$
 

O primă metodă de rezolvare ar fi să încercăm toate cele $2^4^$ posibilităţi de atribuire posibilă, dar această metodă are ordinul de complexitate $O(M * 2^N^)$ şi este eficientă doar pentru instanţe mici ale problemei.

h3. Soluţie $O(N * M)$
 

Următoarea soluţie pare trivială, dar găsirea acestui algoritm şi realizarea faptului că el rezolvă corect problema este mai grea decât impresia lăsată după citirea ei. Considerăm o propoziţie oarecare cu două variabile $p$ şi $q$, apoi una dintre ele, de exemplu $p$. Dacă literalul în care apare $p$ este negat atunci îi atribuim valoarea $1$. Pentru ca propoziţia respectivă să aibă $1$ valoarea de adevăr atunci valoarea lui $q$ este fixată. Fixând şi valoarea lui $q$, probabil şi alte propoziţii ce conţin literalul $q$ vor avea celălalt literal fixat. Propagăm astfel o serie de schimbări. După ce toate schimbările forţate au fost făcute propoziţiile rezultate vor fi de următoarele tipuri: <tex> a \vee b </tex>, <tex> 1 \vee 0 </tex>, <tex> 1 \vee 1 </tex>, <tex> 1 \vee b </tex>. Propoziţii de tip <tex> 0 \vee b </tex> nu pot apărea pentru că toate schimbările forţate au fost deja propagate. Dacă apare o propoziţie <tex> 0 \vee 0 </tex> atunci alegerea făcută pentru valoarea lui $p$ este greşită. Vom încerca şi alegerea opusă. Dacă ambele duc la o propoziţie de tip <tex> 0 \vee 0 </tex> atunci expresia nu poate fi satisfăcută. Propoziţiile de forma <tex> 1 \vee 0 </tex>, <tex> 1 \vee 1 </tex>, <tex> 1 \vee b </tex> pot fi ignorate. În acest fel am eliminat cel puţin o variabilă şi o propoziţie din expresie. Dacă expresia iniţială era satisfiabilă, atunci şi expresia din care s-au eliminate câteva propoziţii a rămas satisfiabilă. Continuând pe această idee obţinem un algoritm de complexitate $O(N * M)$, pentru că la fiecare atribuire de valoare pentru o variabilă parcurgem şirul de propoziţii o dată.
Să vedem cum funcţionează algoritmul pentru expresia: <tex> (x_{1} \vee \sim x_{2}) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee x_{2}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. Considerăm propoziţia <tex> (x_{1} \vee \sim x_{2}) </tex> şi <tex> \langle x_{2} = 1 \rangle </tex>. Astfel, vom obţine mai departe <tex> (x_{1} \vee 0) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee 1) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. În propoziţia <tex> (x_{1} \vee 0) </tex> <tex> x_{1} </tex> trebuie să fie egal cu <tex> 1 </tex>. Acum, expresia devine: <tex> (0 \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee 0) </tex>. Din propoziţia <tex> (0 \vee \sim x_{3}) </tex> obţinem <tex> \langle x_{3} = 0 \rangle </tex>, iar din <tex> (x_{4} \vee 0) </tex> obţinem <tex> \langle x_{4} = 1 \rangle </tex>. Deci, atribuirea satisfiabilă este <tex> \langle x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = 1 \rangle </tex>.

h3. Soluţie randomizată
 

O altă soluţie elegantă se bazează pe o metodă randomizată:
# pornim întâi cu o atribuire de valori booleene oarecare variabilelor;