== include(page="template/taskheader" task_id="2sat") ==
Problema satisfiabilităţii, notată prescurtat cu '$SAT$':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions.2C_terminology_and_applications 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$.
Problema satisfiabilităţii, notată prescurtat cu 'SAT':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions.2C_terminology_and_applications, 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$.
Următoarea formulă: <tex> \phi = ((x_{1} \rightarrow x_{2}) \vee \sim((\sim x_{1} \leftrightarrow x_{3}) \vee x_{4})) \wedge \sim x_{2} </tex>, are o atribuire satisfiabilă dată de: <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex>.
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 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 '_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 rezolvarea acestei probleme ne interesează doar forma normal conjunctivă, întrucât cealaltă formă se poate reduce la aceasta. 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>.
Î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 expresie în forma normal conjunctivă cu propoziţii ca disjuncţie de doi literali: <tex> (x_{1} \vee x_{3}) \wedge (x_{2} \vee (\sim x_{1})) \wedge ((\sim x_{4}) \vee x{3}) </tex>.
h2. Cerinţă
Dându-se o expresie $2SAT$ să se determine o atribuire satisfiabilă a acesteia.
Dându-se o expresie 2SAT să se determine o atribuire satisfiabilă a acesteia.
h2. Date de intrare
Fişierul de intrare $2sat.in$ va conţine pe prima linie două numere naturale, $N$, numărul de termeni care apar în expresie, şi $M$, numărul de propoziţii disjunctive din care este formată expresia. Pe fiecare dintre urmatoarele $M$ linii se vor afla câte două numere întregi, numerele de ordine ale termenilor prezenţi în fiecare dintre propoziţii. Semnul $-$ în faţa unui număr reprezintă negarea termenului în expresie.
Fişierul de intrare $2sat.in$ va conţine pe prima linie două numere naturale, $N$, numărul de termeni care apar în expresie, şi $M$, numărul de propoziţii disjunctive din care este formată expresia. Pe fiecare dintre urmatoarele $M$ linii se vor afla câte două numere întregi, numerele de ordine ale termenilor prezenţi în fiecare dintre propoziţii. Semnul minus în faţa unui număr reprezintă negarea termenului în expresie.
h2. Date de ieşire
