== 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”. Următoarea formulă: <tex> ((x_{1} \rightarrow x_{2}) \vee ((\bar{x_{1}} \leftrightarrow x_{3}) \wedge x_{4})) \wedge \bar{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>.

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

Utilizând următoarele 'echivalenţe logice':http://en.wikipedia.org/wiki/Logical_equivalence: 'regula dublei negaţii':http://en.wikipedia.org/wiki/Double_negative_elimination, 'legile lui De Morgan':http://en.wikipedia.org/wiki/De_Morgan%27s_laws şi 'legea distributivităţii':http://en.wikipedia.org/wiki/Distributivity, orice formulă booleană poate fi transformată în 'forma normal conjunctivă':http://en.wikipedia.org/wiki/Conjunctive_normal_form, o expresie scrisă ca o conjuncţie de propoziţii, iar fiecare propoziţie ca o disjuncţie de literali. Un exemplu de expresie în forma normal conjunctivă este: <tex> (x_{1} \vee x_{3}) \wedge (x_{2} \vee \bar{x_{1}}) \wedge (\bar{x_{4}} \vee x{3}) </tex>.

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

În consecinţă, va fi suficient să studiem 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.

Orice formulă booleană poate fi transformată în două forme:

Î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':http://en.wikipedia.org/wiki/Polynomial_time#Polynomial_time.

* î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;

h3. Cerinţă

* î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;

Dându-se o expresie 2SAT să se determine o atribuire satisfiabilă a acesteia.

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

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 minus în faţa unui număr reprezintă negarea termenului în expresie.

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 formata expresia. Pe fiecare dintre urmatoarele $M$ linii se vor afla cate 2 numere intregi, numerele de ordine ale termenilor prezenti in fiecare dintre propozitii. Semnul $-$ in fata unui numar reprezinta ca termenul respectiv apare negat in expresie.

h2. Date de ieşire

În fişierul de ieşire $2sat.out$ se vor afişa $N$ numere naturale, $0$ sau $1$, reprezentând o atribuire satisfiabilă pentru expresia dată în fişierul de intrare, sau valoarea $-1$ în caz că expresia nu admite soluţie.

În fişierul de ieşire $2sat.out$ se vor afisa $N$ numere naturale, $0$ sau $1$, reprezentand o atribuire satisfiabila pentru expresia data in fisierul de intrare.

h2. Restricţii

* $1 ≤ N ≤ 100 000$.
* $1 ≤ M ≤ 200 000$.

* $1 ≤ N ≤ 100000$
* $1 ≤ M ≤ 100000$

h2. Exemplu
table(example). |_. 2sat.in |_. 2sat.out |
| 4 5

-1 -2
2 -3
2 3
-2 -4
3 4
| 0 1 1 0

1 -2
-1 -3
1 2
4 -3
4 -1
| 1 0 0 1

|

h3. Explicaţie
 
Datele de intrare corespund următoarei expresii: <tex> (\bar{x_{1}} \vee \bar{x_{2}}) \wedge (x_{2} \vee \bar{x_{3}}) \wedge (x_{2} \vee x_{3}) \wedge (\bar{x_{2}} \vee \bar{x_{4}}) \wedge (x_{3} \vee x_{4}) </tex>. O atribuire satisfiabilă este: <tex> \langle x_{1} = 0, x_{2} = 1, x_{3} = 1, x_{4} = 0 \rangle </tex>.
 
h2. Indicaţii de rezolvare
 
Articolul 'Problema 2-satisfiabilităţii':http://infoarena.ro/2-sat prezintă fiecare dintre soluţiile de mai jos în detaliu. Iată o schiţă...
 
O soluţie evidentă este încercarea celor $2^N^$ configuraţii posibile pentru termenii expresiei şi verificarea lor. Această abordare duce însă la o complexitate cu ordinul de excuţie $O(2^N^ * M)$. Cu această soluţie se obţin '$20$ de puncte':job_detail/382683?action=view-source.
 
O altă soluţie se conturează dacă fixăm o variabilă $p$ dintr-o propoziţie. În cazul acesta suntem obligaţi să îi dăm o anumită valoare celeilalte variabile din acea propoziţie, $q$, ceea ce ne obligă să propagăm atribuiri de valori şi variabilelor care se găsesc în alte propoziţii care îl conţin pe $q$, şi aşa mai departe. Astfel, dacă problema admite soluţie vom ajunge la ea. Complexitatea finală este $O(N * M)$. Acest algoritm obţine '$70$ de puncte':job_detail/382685?action=view-source.
 
O alta soluţie neliniară, în complexitatea $O(N^2^ * M)$, se bazează pe un algoritm randomizat. Iniţial, se atribuie valori arbitrare variabilelor, după care, cât timp expresia nu este satisfăcută, se găseşte o propoziţie cu valoarea de adevăr $0$ şi se schimbă valoarea unuia dintre cei doi termeni componenţi ai propoziţiei. Precizăm că această abordare se comportă foarte bine în practică, aşa că ar trebui să obţină 'circa $70$ de puncte':job_detail/382684?action=view-source.
 
Soluţia optimă foloseşte 'relaţia de implicaţie':http://en.wikipedia.org/wiki/Logical_implication pentru a transforma expresia într-un graf după cum urmează: orice disjuncţie de literali <tex> x_{i} \vee x_{j} </tex> este echivalentă cu următoarele implicaţii <tex> \bar{x_{i}} \to x_{j} </tex> şi <tex> \bar{x_{j}} \to x_{i} </tex>. Vom construi un graf cu noduri din mulţimea <tex> \{x_{1}, x_{2}, .., x_{n}, \bar{x_{1}}, \bar{x_{2}}, .., \bar{x_{n}}\} </tex> astfel: pentru orice propoziţie <tex> x_{i} \vee x_{j} </tex> va exista muchie de la <tex> \bar{x_{i}} </tex> la <tex> x_{j} </tex> şi de la <tex> \bar{x_{j}} </tex> la <tex> x_{i} </tex>, după cum arată relaţiile de implicaţie echivalente.
 
În continuare, vom demonstra o modalitate de a atribui valori nodurilor din graf, şi, astfel, implicit variabilelor pentru a rezolva 2SAT. Legătura dintre rezolvarea acestei probleme şi valorile nodurilor este o relaţie de echivalenţă, după cum se demonstrează...

h3. Indicatii pentru rezolvare

_Necesitatea_
Dacă avem soluţie pentru expresia 2SAT, va trebui să demonstrăm că pentru toate muchiile din graf nu întâlnim situaţii în care avem muchie de la un nod „true” la un nod „false”. Dacă presupunem prin absurd că există o astfel de muchie, între un nod <tex> \bar{x_{i}} </tex> „true” (deci <tex> x_{i} </tex> „false”) şi <tex> x_{j} </tex> „false”, atunci muchia de la <tex> \bar{x_{i}} </tex> la <tex> x_{j} </tex> există în graf dacă şi numai dacă în forma normal conjunctivă apare disjuncţia <tex> x_{i} \vee x_{j} </tex>. Însă, <tex> x_{i} \vee x_{j} </tex> este „false” dacă ambele valori sunt „false”. Contradicţie!

O solutie evidenta este incercarea celor $2^N^$ configuratii posibile pentru termenii expresiei si apoi verificarea lor, aceasta abordare ducand la o complexitate de $O(2^N^ * M)$. Cu aceasta complexitate se obtin 20 de puncte, iar o sursa demonstrativa se gaseste aici.

_Suficienţa_
Dacă fiecărei propoziţii <tex> x_{i} \vee x_{j} </tex> îi corespund două muchii <tex> \bar{x_{i}} \to x_{j} </tex> şi <tex> \bar{x_{j}} \to x_{i} </tex>, atunci, cum nu putem avea <tex> \bar{x_{i}} </tex> „true”, <tex> x_{j} </tex> „false” sau <tex> \bar{x_{j}} </tex> „true”, <tex> x_{i} </tex> „false”, nu vom avea nici <tex> x_{i} </tex> şi <tex> x_{j} </tex> simultan egale cu „false”. Astfel, propoziţia <tex> x_{i} \vee x_{j} </tex> este adevărată.

Următoarea soluţie pare trivială, dar găsirea acestui algoritm şi realizarea faptului că el rezolvă corect problema sunt mai grele decât impresia lăsată după citirea ei. Considerăm o propoziţie oarecare cu două variabile $p$ şi $q$, apoi una dintre ele, de exemplu $p$. Ii atribuim lui $p$ valoarea $0$. Pentru ca propoziţia respectivă să aibă $1$ valoarea de adevăr, atunci valoarea lui q trebuie fixată. Fixând si valoarea lui $q$, probabil si alte propoziţii ce conţin literalul $q$ vor avea celălalt literal fixat. Propagăm astfel o serie de schimbări. După ce toate schimbările forţate au fost făcute, propoziţiile rezultate vor fi de următoarele tipuri: $A SAU B$, $1 SAU 0$, $1 SAU 1$, $1 SAU B$. Propozitii de tipul $0 SAU B$ nu pot aparea, pentru ca toate schimbarile fortate au fost deja propagate. Dacă apare o propoziţie $0 SAU 0$ atunci alegerea făcută pentru valoarea lui p este greşită. Vom încerca şi alegerea opusă pentru p. Dacă ambele duc la o propoziţie de tip  atunci expresia nu poate fi satisfăcută. Propoziţiile de forma $1 SAU 0$, $1 SAU 1$, $1 SAU B$  pot fi ignorate. În acest fel am eliminat cel puţin o variabilă şi o propoziţie din expresie. Dacă expresia iniţială era satisfiabilă, atunci şi expresia din care s-au eliminat câteva propoziţii a rămas satisfiabilă. Continuând pe această idee obţinem un algoritm de complexitate $O(N * M)$, pentru că la fiecare atribuire de valoare pentru o variabilă parcurgem şirul de propoziţii o dată. Aceasta solutie trebuie sa obtina $40$ de puncte, sursa se gaseste aici.

În articolul de mai sus se arată cum se ajunge la soluţie. Iată pe scurt cum se procedează. În primul rând, graful va fi împărţit în 'componente tare-conexe':problema/ctc. O proprietate importantă a componentelor conexe este că în fiecare componentă există un ciclu ce conţine toate vârfurile sale. Astfel, toate nodurile dintr-o componentă tare conexă vor avea, în mod necesar, aceeaşi valoare de adevăr. Dacă nu ar fi astfel, ar exista pe ciclu o valoare „true” ce ar implica o valoare „false”. Observăm că dacă un nod şi negaţia sa se găsesc în aceeaşi componentă tare conexă atunci nu există soluţie. Din câteva proprietăţi de simetrie, pe care le puteţi găsi în articol, se deduce că pentru o componentă <tex> c </tex> în care se găseşte o implicaţie <tex> x_{i} \rightarrow x_{j} </tex>, va exista o componentă <tex> \bar{c} </tex> ce va conţine implicaţia echivalentă <tex> \bar{x_{j}} \rightarrow \bar{x_{i}} </tex>. În continuare, vom contracta componentele tare-conexe într-un nod, rezultând un graf orientat aciclic. Prin gradul unei componente tare-conexe vom înţelege gradul nodului asociat din acest graf orientat aciclic. Utilizând o 'sortare topologică':problema/sortaret vom împerechea succesiv componentele după cum urmează. Se va alege o componentă cu gradul de intrare zero. Din componenta sa pereche, datorită simetriei de care aminteam, nu va ieşi nicio muchie. Astfel, toate nodurile din componenta tare-conexă cu gradul de intrare zero vor avea valoarea de adevăr „false”, pentru a nu impune restricţii asupra celorlalte noduri, iar toate nodurile din componenta pereche vor primi valoarea de adevăr „true”, întrucât din aceasta nu mai iese nicio muchie şi astfel nu va influenţa alte valori. Ulterior, se vor elimina cele două noduri şi se va relua procedeul.

O alta solutie neoptima, in complexitatea $O(N^2^)$ se bazeaza pe un algoritm randomizat. Initial se atribuie valori arbitrare variabilelor, iar apoi cat timp expresia nu este satisfacuta se gaseste o propozitie cu valoarea de adevar $0$ si se schimba valoarea unuia dintre cei 2 termeni componenti ai propozitiei. Pentru o demonstratie a functionalitatii acestui algoritm consultati 'articolul':/2-sat#solutie-3

A se preciza ca in general sortarea topologica nu mai trebuie implementata. Algoritmul lui Tarjan adauga componentele in ordinea inversa a sortarii topologice, iar algoritmul lui Kosaraju fie exact sortarea topologica, fie invera ei (depinde daca se inverseaza sau nu ordinea celor doua parcurgeri). Prin inversa a se intelege ca prima componenta e ultima,a doua penultima s.a.m.d.

//TODO: Solutia in O(M + N)

Soluţia de '100 de puncte':job_detail/382602?action=view-source are complexitatea $O(M + N)$.

*Marius* Cezar, scuze că îţi zic puţin târziu, dar, din punctul meu de vedere nu mai e nevoie să explici în detaliu soluţiile. Sunt deja prezentate în articolul lui Cosmin. Câte cuvinte despre fiecare (cum e la ultima cu algoritmul randomizat) şi o sursă beton sunt de ajuns. Dar să fie beton sursa. :)

h2. Aplicaţii

h3. Aplicatii

* 'Party':problema/party
* 'Aladdin':problema/aladdin

* 'Party':/problema/party
* 'Aladdin':/problema/aladdin

* 'Excursion':http://www.oi.edu.pl/download/boi-2001.pdf - Baltic Olympiad in Informatics, 2001
* 'Peaceful Commission':http://www.oi.edu.pl/php/show.php?ac=e100000&module=show&file=zadania/oi8/spokojna - Polish Olympiad in Informatics, 2001
* 'Gates':http://b08.oi.edu.pl/downloads/booklet.pdf - Baltic Olympiad in Informatics, 2008

4436