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

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

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 (\sim x_{1})) \wedge ((\sim x_{4}) \vee x{3}) </tex>.

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

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

* î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 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 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ă, î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 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ţă

h3. Cerinţă

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

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

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

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

|

h2. Explicaţie

h3. Explicaţie

_(Cum s-a ajuns la soluţie, cum au fost mapaţi termenii cu numerele întregi [să zicem că reprezintă indexul variabilei $x$?])_.

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

h3. Indicaţii pentru rezolvare

h2. Indicaţii de rezolvare

Articolul '_Problema 2-satisfiabilităţii_':/2-sat prezintă fiecare dintre soluţiile de mai jos în detaliu. Iată o schiţă...

Articolul 'Problema 2-satisfiabilităţii':/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 de $O(2^N^ * M)$. Cu această complexitate se obţin $20$ de puncte, iar o sursă demonstrativă se găseşte 'aici':/job_detail/372167?action=view-source.

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/372167?action=view-source.

'O altă soluţie':/job_detail/372174?action=view-source 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ă fiind $O(N * M)$. Acest algoritm obţine $70$ de puncte.

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/372174?action=view-source.

'O alta soluţie neliniară':/job_detail/372176?action=view-source, î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ă aproximativ $70$ de puncte.

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/372176?action=view-source.

'Soluţia optimă':/job_detail/372206?action=view-source, în complexitatea $O(M + N)$, se foloseşte de 'relaţia de implicaţie':http://en.wikipedia.org/wiki/Logical_implication ce transformă expresia într-un graf, care se poate rezolva determinând 'componentele tare-conexe':/problema/ctc.

'Soluţia optimă':/job_detail/372206?action=view-source, în complexitatea $O(M + N)$, se foloseşte de 'relaţia de implicaţie':http://en.wikipedia.org/wiki/Logical_implication ce transformă expresia într-un graf, care se poate rezolva determinând 'componentele tare-conexe':/problema/ctc şi o 'sortare topologică':problema/sortaret.

h3. Aplicatii