== include(page="template/taskheader" task_id="2sat") ==

Problema satisfiabilitatii, notata prescurtat cu $SAT$ cere determinarea existentei unei atribuiri satisfiabile pentru o formula booleana. O atribuire de valori booleene pentru variabilele acestei expresii se numeste atribuire satisfiabila daca evaluarea expresiei dupa atribuirea valorilor da rezultat ca valoare de adevar $"adevarat"$. Un exemplu de formula ar fi:
$((x{~1~} SAU x{~2~}) SI ((NOT x{~3~}) SI x{~1~}) SAU x{~4~})$
aceasta avand o atribuire satisfiabila $x{~1~}=1 x{~2~}=0 x{~3~}=0 x{~4~}=1$.
Orice formula booleana poate fi transformata in 2 forme: forma normal conjunctiva (expresia este scrisa ca o conjunctie de propozitii $P{~1~} SI P{~2~} SI ... SI P{~n~}$, unde $P{~i~}$ este de forma $T{~1~} SAU T{~2~} SAU ... SAU T{~k~}$, $T{~j~}$ fiind un termen care poate sau nu sa fie negat) si forma normal disjunctiva (expresia este scrisa ca o disjunctie de propozitii in interiorul carora exista doar conjunctii intre termeni). In rezolvarea acestei probleme ne intereseaza doar forma normal conjunctiva.
Problema $SAT$ este NP-completa, chiar si daca restrictionam expresiile la unele care in forma normal conjunctiva au doar 3 termeni in fiecare dintre propozitii. Problema satisfiabilitatii pentru asemenea expresii se numeste $3SAT$. Problema $2SAT$ (2 termeni in fiecare din propozitiile care alcatuiesc forma normal conjunctiva) este rezolvabila in timp polinomial.
Un exemplu de expresie $2SAT$ este:

Problema satisfiabilităţii, notată prescurtat cu '$SAT$':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT cere determinarea existenţei unei atribuiri satisfiabile pentru o formulă booleană. O atribuire de valori booleene pentru variabilele acestei expresii se numeşte $atribuire satisfiabilă$ dacă evaluarea expresiei după atribuirea valorilor are ca rezultat valoarea de adevăr $adevărat$.

$(x{~1~} SAU x{~3~}) SI (x{~2~} SAU (NOT x{~1~})) SI ((NOT x{~4~}) SAU x{~3~})$

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 având o atribuire satisfiabilă <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex>.

h2. Cerinta

Orice formulă booleană poate fi transformată în două forme:
 
* în '$forma normal conjunctivă$':http://en.wikipedia.org/wiki/Conjunctive_normal_form expresia este scrisă ca o conjuncţie de propoziţii, iar fiecare propoziţie este o disjuncţie de literali;
 
* în '$forma normal disjunctivă$':http://en.wikipedia.org/wiki/Disjunctive_normal_form expresia este scrisă ca o disjuncţie de propoziţii în interiorul cărora există doar conjuncţii de literali;
 
În rezolvarea acestei probleme ne interesează doar forma normal conjunctivă. Problema $SAT$ pe cazul general este '$NP-completă$':http://en.wikipedia.org/wiki/NP-complete, chiar şi dacă restricţionăm expresiile la unele care în forma normal conjunctivă au doar _trei_ literali în fiecare dintre propoziţii. Problema satisfiabilităţii pentru asemenea expresii se numeşte '$3SAT$':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability.
 
În continuare ne vom ocupa de problema '$2SAT$':http://en.wikipedia.org/wiki/2-satisfiability, ce are _doi_ literali în fiecare din propoziţiile ce alcătuiesc forma normal conjunctivă, $2SAT$ fiind rezolvabilă în timp polinomial. Un exemplu de o astfel de expresie: <tex> (x_{1} \vee x_{3}) \wedge (x_{2} \vee (\sim x_{1})) \wedge ((\sim x_{4}) \vee x{3}) </tex>.
 
h2. Cerinţă

Dandu-se o expresie $2SAT$ sa se determine o atribuire satisfiabila a acesteia.