(Categoria _Algoritmi_, Autor _Cosmin Negruşeri_)

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 ( $x{~1~}$, $x{~2~}$,… ), $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 $1$ şi $0$ în loc de $adevărat$ şi $fals$.

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

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

O altă soluţie elegantă se bazează pe o metodă randomizată:

# pornim întâi cu o atribuire de valori booleene oarecare variabilelor;
# găsim o propoziţie cu valoarea de adevăr <tex> 0 </tex>;
# vom schimba valoarea de adevăr a oricăreia dintre cele două variabile prezente în propoziţie, ceea ce va face ca acea propoziţie să aibă noua valoare de adevăr <tex> 1 </tex>;
# cât timp expresia nu este satisfăcută repetăm acest procedeu de schimbare a valorii unei variabile dintr-o propoziţie nesatisfăcută, deci revenim la pasul $2$.