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

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:

h2. Date de intrare

Fişierul de intrare $2sat.in$ va contine pe prima linie 2 numere naturale, $N$ - numarul de termeni care apar in expresie si $M$ - numarul de propozitii disjunctive din care este foramta expresia.

Fişierul de intrare $2sat.in$ va contine pe prima linie 2 numere naturale, $N$ - numarul de termeni care apar in expresie si $M$ - numarul de propozitii disjunctive din care este foramta expresia. Pe fiecare dintre urmatoarele $M$ linii se vor afla cate 2 numere intregi, numerele de ordine ale termenilor

h2. Date de ieşire