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

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