Problema satisfiabilității formulelor logice de ordinul doi

Problema 2-satisfiabilității

h1. Problema satisfiabilităţii formulelor logice de ordinul doi

h1. Problema 2-satisfiabilităţii

== include(page="template/implica-te/scrie-articole" user_id="marius") ==

* {'Soluţii pentru 2-SAT':2-sat#solutii-2-sat}
** {'Soluţie $O(M * 2^N^)$':2-sat#solutie-1}
** {'Soluţie $O(N * M)$':2-sat#solutie-2}

** {'Soluţie $O(N^2^)$':2-sat#solutie-3}

** {'Soluţie $O(N^2^ * M)$':2-sat#solutie-3}

** {'Soluţie $O(M + N)$':2-sat#solutie-4}
* {'Aplicaţii':2-sat#aplicatii}
** {'Party (preONI 2003/2004)':2-sat#party}

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$. Îi atribuim literalului în care apare $p$ valoarea $0$. Pentru ca propoziţia respectivă să aibă $1$ valoarea de adevăr, atunci valoarea lui $q$ trebuie fixată. Fixând şi valoarea lui $q$, probabil şi 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: <tex> a \vee b </tex>, <tex> 1 \vee 0 </tex>, <tex> 1 \vee 1 </tex>, <tex> 1 \vee b </tex>. Propoziţii de tip <tex> 0 \vee b </tex> nu pot apărea pentru că toate schimbările forţate au fost deja propagate. Dacă apare o propoziţie <tex> 0 \vee 0 </tex> 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 <tex> 0 \vee 0 </tex> atunci expresia nu poate fi satisfăcută. Propoziţiile de forma <tex> 1 \vee 0 </tex>, <tex> 1 \vee 1 </tex>, <tex> 1 \vee b </tex> 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ă.

Să vedem cum funcţionează algoritmul pentru expresia: <tex> (x_{1} \vee \sim x_{2}) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee x_{2}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. Considerăm propoziţia <tex> (x_{1} \vee \sim x_{2}) </tex> şi <tex> \langle x_{2} = 1 \rangle </tex>. Astfel, vom obţine mai departe <tex> (x_{1} \vee 0) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee 1) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. În propoziţia <tex> (x_{1} \vee 0) </tex>, <tex> x_{1} </tex> trebuie să fie egal cu <tex> 1 </tex>. Acum, expresia devine: <tex> (0\ \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee 0) </tex>. Din propoziţia <tex> (0\ \vee \sim x_{3}) </tex> obţinem <tex> \langle x_{3} = 0 \rangle </tex>, iar din <tex> (x_{4} \vee 0) </tex> obţinem <tex> \langle x_{4} = 1 \rangle </tex>. Deci, atribuirea satisfiabilă este <tex> \langle x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = 1 \rangle </tex>.

Să vedem cum funcţionează algoritmul pentru expresia: <tex> (x_{1} \vee \sim x_{2}) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee x_{2}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. Considerăm propoziţia <tex> (x_{1} \vee \sim x_{2}) </tex> şi <tex> \langle x_{2} = 1 \rangle </tex>. Astfel, vom obţine mai departe <tex> (x_{1} \vee 0) \wedge (\sim x_{1} \vee \sim x_{3}) \wedge (x_{1} \vee 1) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{1}) </tex>. În propoziţia <tex> (x_{1} \vee 0) </tex>, <tex> x_{1} </tex> trebuie să fie egal cu <tex> 1 </tex>. Acum, expresia devine: <tex> (0\ \vee \sim x_{3}) \wedge (x_{4} \vee \sim x_{3}) \wedge (x_{4} \vee 0) </tex>. Din propoziţia <tex> (0\ \vee \sim x_{3}) </tex> obţinem <tex> \langle x_{3} = 0 \rangle </tex>, iar din <tex> (x_{4} \vee 0) </tex> obţinem <tex> \langle x_{4} = 1 \rangle </tex>. Deci, atribuirea satisfiabilă este <tex> \langle x_{1} = 1, x_{2} = 1, x_{3} = 0, x_{4} = 1 \rangle </tex>.

h3(#solutie-3). Soluţie $O(N^2^)$

h3(#solutie-3). Soluţie $O(N^2^ * M)$

O altă soluţie elegantă se bazează pe o metodă randomizată:

h3(#solutie-4). Soluţie $O(M + N)$

O a treia soluţie se bazează pe relaţia de implicaţie. Relaţia <tex> \rightarrow </tex> are următoarea tabelă de adevăr:

O a treia soluţie se bazează pe relaţia de implicaţie. Aceasta are următoarea tabelă de adevăr:

table{width: 90px; text-align: center}. | <tex> A </tex> | <tex> B </tex> | <tex> A \rightarrow B </tex> |
| <tex> 0 </tex> | <tex> 0 </tex> | <tex> 1 </tex>  |

| <tex> 1 </tex> | <tex> 0 </tex> | <tex> 0 </tex> |
| <tex> 1 </tex> | <tex> 1 </tex> | <tex> 1 </tex> |

Fiecare clauză <tex> A \vee B </tex> poate fi scrisă ca două implicaţii <tex> \sim A \rightarrow B </tex> şi <tex> \sim B \rightarrow A </tex>. Realizăm un graf al implicaţiilor. Astfel, nodurile grafului vor fi variabilele <tex> A </tex>, <tex> B </tex> <tex> ... </tex> şi negaţiile lor <tex> \sim A </tex>, <tex> \sim B </tex> <tex> ... </tex> iar muchiile acestui graf vor fi implicaţiile echivalente cu propoziţiile din expresie. Deci, dacă expresia are $M$ propoziţii, graful va avea $2M$ muchii. Acestea fiind zise, expresiei <tex> (\sim A \vee \sim B) \wedge (B \vee \sim C) \wedge (B \vee C) \wedge (\sim B \vee \sim D) \wedge (C \vee D) </tex> îi corespunde graful:

Fiecare clauză <tex> A \vee B </tex> poate fi scrisă ca două implicaţii <tex> (\sim A \rightarrow B) </tex> şi <tex> (\sim B \rightarrow A) </tex>. Realizăm un graf al implicaţiilor. Astfel, nodurile grafului vor fi variabilele <tex> A </tex>, <tex> B </tex> <tex> ... </tex> şi negaţiile lor <tex> \sim A </tex>, <tex> \sim B </tex> <tex> ... </tex> iar muchiile acestui graf vor fi implicaţiile echivalente cu propoziţiile din expresie. Deci, dacă expresia are $M$ propoziţii, graful va avea $2M$ muchii. Acestea fiind zise, expresiei <tex> (\sim A \vee \sim B) \wedge (B \vee \sim C) \wedge (B \vee C) \wedge (\sim B \vee \sim D) \wedge (C \vee D) </tex> îi corespunde graful:

p=. !2-sat?Graf.png!

Dacă avem <tex> A \longrightarrow B </tex> o muchie în graful nostru şi literalul <tex> A </tex> este adevărat, atunci şi literalul <tex> B </tex> trebuie să fie adevărat pentru ca propoziţia reprezentată de muchie să fie satisfăcută. Putem demonstra prin inducţie că dacă există un drum în graf de la literalul <tex> A </tex> la literalul <tex> B </tex>, atunci dacă <tex> A </tex> este adevărat şi <tex> B </tex> trebuie să fie adevărat. Dacă există un drum de la un literal <tex> X </tex> la <tex> \sim X </tex>, precum şi un drum invers, atunci nu va exista soluţie pentru că nu putem seta în acelaşi timp o variabilă şi valoarea ei negată la valoarea adevărat. De aici rezultă că dacă în graful asociat expresiei există o variabilă <tex> X </tex> în aceeaşi componentă tare conexă cu <tex> \sim X </tex> atunci instanţa problemei satisfiabilităţii nu poate fi satisfăcută. Dacă nu există o asemenea variabilă, vom vedea în continuare cum putem rezolva problema. Întâi, facem observaţia că dacă în graf există muchia <tex> A \longrightarrow B </tex> atunci există şi muchia <tex> \sim B \longrightarrow \sim A </tex>. Astfel, dacă există un drum de la <tex> A </tex> la <tex> B </tex> în graf, aplicând proprietatea menţionată pentru fiecare muchie a drumului, vom găsi un drum de la <tex> \sim B </tex> la <tex> \sim A </tex>. Evident, afirmaţia este valabilă şi reciproc: dacă există drum de la <tex> B </tex> la <tex> A </tex> atunci vom avea un drum de la nodul <tex> \sim A </tex> la <tex> \sim B </tex>. Astfel, dacă avem că <tex> A </tex> şi <tex> B </tex> sunt în aceeaşi componentă tare conexă atunci şi nodurile <tex> \sim A </tex> şi <tex> \sim B </tex> sunt în aceeaşi componentă tare conexă. Deci, dacă nu există doi literali <tex> X </tex> şi <tex> \sim X </tex> în aceeaşi componentă tare conexă, putem să împărţim graful în componente tare conexe şi să împerechem componentele câte două astfel ca în fiecare pereche să apară o componentă <tex> U </tex> cu nişte literali şi altă componentă <tex> \sim U </tex> cu aceiaşi literali negaţi. Pentru a găsi o soluţie vom determina mai întâi componentele tare conexe ale grafului. Apoi putem contracta fiecare componentă într-un nod. Graful obţinut va fi aciclic. Alegem un nod <tex> u </tex> în care nu intră nicio muchie (un asemenea nod trebuie să existe pentru a nu exista cicluri). Din considerente de simetrie, din nodul lui pereche <tex> \sim u </tex> nu va ieşi nicio muchie. Literalilor componentei <tex> U </tex> putem să le dăm valoarea de adevăr <tex> 0 </tex>, iar literalilor din componenta pereche <tex> \sim U </tex>  putem să le dăm valoarea de adevăr <tex> 1 </tex>. Această alegere nu impune restricţii asupra celorlalţi literali şi elimină câteva variabile din problemă. Repetarea recursivă a acestui pas pe graful rămas va duce la rezolvarea problemei. Determinarea componentelor tare conexe se poate face în complexitatea $O(N + M)$. Pentru a vedea acest algoritm puteţi consulta 'secţiunea $23.5$':http://zhuzeyuan.hp.infoseek.co.jp/ita/chap23.htm din {'[1]':2-sat#bibliografie}. Iar eliminarea nodurilor de care vorbeam mai sus se poate face în $O(N + M)$ folosind o sortare topologică.

Dacă avem <tex> A \longrightarrow B </tex> o muchie în graful nostru şi literalul <tex> A </tex> este adevărat, atunci şi literalul <tex> B </tex> trebuie să fie adevărat pentru ca propoziţia reprezentată de muchie să fie satisfăcută. Putem demonstra prin inducţie că dacă există un drum în graf de la literalul <tex> A </tex> la literalul <tex> B </tex>, atunci dacă <tex> A </tex> este adevărat şi <tex> B </tex> trebuie să fie adevărat. Dacă există un drum de la un literal <tex> X </tex> la <tex> \sim X </tex>, precum şi un drum invers, atunci nu va exista soluţie pentru că nu putem seta în acelaşi timp o variabilă şi valoarea ei negată la valoarea adevărat. De aici rezultă că dacă în graful asociat expresiei există o variabilă <tex> X </tex> în aceeaşi componentă tare conexă cu <tex> \sim X </tex> atunci instanţa problemei satisfiabilităţii nu poate fi satisfăcută. Dacă nu există o asemenea variabilă, vom vedea în continuare cum putem rezolva problema. Întâi, facem observaţia că dacă în graf există muchia <tex> A \longrightarrow B </tex> atunci există şi muchia <tex> \sim B \longrightarrow \sim A </tex>. Astfel, dacă există un drum de la <tex> A </tex> la <tex> B </tex> în graf, aplicând proprietatea menţionată pentru fiecare muchie a drumului, vom găsi un drum de la <tex> \sim B </tex> la <tex> \sim A </tex>. Evident, afirmaţia este valabilă şi reciproc: dacă există drum de la <tex> B </tex> la <tex> A </tex> atunci vom avea un drum de la nodul <tex> \sim A </tex> la <tex> \sim B </tex>. Astfel, dacă avem că <tex> A </tex> şi <tex> B </tex> sunt în aceeaşi componentă tare conexă atunci şi nodurile <tex> \sim A </tex> şi <tex> \sim B </tex> sunt în aceeaşi componentă tare conexă. Deci, dacă nu există doi literali <tex> X </tex> şi <tex> \sim X </tex> în aceeaşi componentă tare conexă, putem să împărţim graful în componente tare conexe şi să împerechem componentele câte două astfel ca în fiecare pereche să apară o componentă <tex> U </tex> cu nişte literali şi altă componentă <tex> \sim U </tex> cu aceiaşi literali negaţi. Pentru a găsi o soluţie vom determina mai întâi componentele tare conexe ale grafului. Apoi putem contracta fiecare componentă într-un nod. Graful obţinut va fi aciclic. Alegem un nod <tex> u </tex> în care nu intră nicio muchie (un asemenea nod trebuie să existe pentru a nu exista cicluri). Din considerente de simetrie, din nodul lui pereche <tex> \sim u </tex> nu va ieşi nicio muchie. Literalilor componentei <tex> U </tex> putem să le dăm valoarea de adevăr <tex> 0 </tex>, iar literalilor din componenta pereche <tex> \sim U </tex>  putem să le dăm valoarea de adevăr <tex> 1 </tex>. Această alegere nu impune restricţii asupra celorlalţi literali şi elimină câteva variabile din problemă. Repetarea recursivă a acestui pas pe graful rămas va duce la rezolvarea problemei. Determinarea 'componentelor tare conexe':problema/ctc se poate face în complexitatea $O(N + M)$. Pentru a vedea acest algoritm puteţi consulta 'secţiunea $23.5$':http://zhuzeyuan.hp.infoseek.co.jp/ita/chap23.htm din {'[1]':2-sat#bibliografie}. Iar eliminarea nodurilor de care vorbeam mai sus se poate face în $O(N + M)$ folosind o 'sortare topologică':problema/sortaret.

Să urmărim cum merge algoritmul nostru pe exemplul de mai sus. Componentele tare conexe sunt următoarele: <tex> \{A\} </tex>, <tex> \{\sim A\} </tex>, <tex> \{B, C, \sim D\} </tex>, <tex> \{\sim B, \sim C, D\} </tex>. În nodul asociat componentei <tex> \{A\} </tex> nu intră nicio muchie. Astfel, putem să îi atribuim lui <tex> A </tex> valoarea <tex> 0 </tex>, iar după eliminarea lui <tex> \{A\} </tex> şi <tex> \{\sim A\} </tex>în nodul asociat componentei <tex> \{\sim B, \sim C, D\} </tex> nu intră nicio muchie, deci putem să îi atribuim lui <tex> B </tex> valoarea <tex> 1 </tex>, lui <tex> C </tex> valoarea <tex> 1 </tex> şi lui <tex> D </tex> valoarea <tex> 0 </tex>. Această atribuire este satisfiabilă după cum vedem în continuare:

h3. Soluţie

Pentru orice două autobuze vom găsi care sunt sensurile de mers pentru ele astfel ca cele două autobuze să nu se întâlnească şi să provoace un accident. Pentru un sens fixat putem afla pentru un autobuz pe ce interval de timp va fi pe o anumită stradă. El va fi în general pe o stradă $(i, j)$ pe un interval de tipul $[t1 + k*T … t2 + k*T]$ unde $t1$ este timpul din prima rută parcursă pentru a ajunge la $i$, $t2$ timpul pentru a ajunge la $j$ iar $T$ este durata totală a unei rute. Acum, pentru a determina dacă două autobuze se vor întâlni pe o rută $(i, j)$ trebuie ca ele să se deplaseze în sensuri opuse pe această rută, iar intervalele lor $[t1 + k*T1 .. t2 + k*T1]$ se intersectează cu intervalele $[tt1 + p*T2 … tt2 + p*T2]$. Este clar acum că putem transforma problema într-o instanţă de $2-SAT$ prin maparea autobuzelor în variabile logice, a sensurilor de mers în valorile $adevărat$ şi $fals$, iar pentru orice pereche de autobuze să fie o propoziţie logică ce ia valoarea $adevărat$ doar dacă sensurile de mers determinate de variabilele logice asociate autobuzelor sunt compatibile. Mai trebuie determinat într-un mod eficient dacă două clase de intervale de timp se intersectează. Aceasta rămâne ca temă cititorului.

Pentru orice două autobuze vom găsi care sunt sensurile de mers pentru ele astfel ca cele două autobuze să nu se întâlnească şi să provoace un accident. Pentru un sens fixat putem afla pentru un autobuz pe ce interval de timp va fi pe o anumită stradă. El va fi în general pe o stradă $(i, j)$ pe un interval de tipul $[t1 + k*T ... t2 + k*T]$ unde $t1$ este timpul din prima rută parcursă pentru a ajunge la $i$, $t2$ timpul pentru a ajunge la $j$, iar $T$ este durata totală a unei rute. Acum, pentru a determina dacă două autobuze se vor întâlni pe o rută $(i, j)$ trebuie ca ele să se deplaseze în sensuri opuse pe această rută, iar intervalele $[t1 + k*T1 ... t2 + k*T1]$ ale primului să se intersecteze cu intervalele $[tt1 + p*T2 ... tt2 + p*T2]$ ale celui de-al doilea. Este clar acum că putem transforma problema într-o instanţă de $2-SAT$ prin maparea autobuzelor în variabile logice, a sensurilor de mers în valorile $adevărat$ şi $fals$, iar pentru orice pereche de autobuze să fie o propoziţie logică ce ia valoarea $adevărat$ doar dacă sensurile de mers determinate de variabilele logice asociate autobuzelor sunt compatibile. Mai trebuie determinat într-un mod eficient dacă două clase de intervale de timp se intersectează. Aceasta rămâne ca temă cititorului.

h2(#aladdin). 'Aladdin':problema/aladdin (Bursele Agora 2005/2006, Runda 1)

| <tex> 0 </tex> | <tex> 1 </tex> | <tex> 1 </tex> | <tex> 0 </tex> |
| <tex> 0 </tex> | <tex> 0 </tex> | <tex> 0 </tex> | <tex> 0 </tex> |

Fie <tex> A </tex> o matrice soluţie a problemei noastre. Vom numerota rândurile matricii de la $0$ la $N - 1$ şi coloanele de la $0$ la $M - 1$. Matricea de intrare <tex> S </tex> reprezintă de fapt sumele din fiecare pătrat de câte $2 x 2$ elemente. Facem observaţia că dacă ştim într-un pătrat de $2 x 2$ valorile pentru trei dintre celule, atunci valoarea din a patra celulă este unic determinată pentru că ştim suma elementelor din pătrat. Vedem astfel, că dacă ştim valorile elementelor din prima linie a matricii <tex> A </tex> şi din prima coloană, restul valorilor sunt unic determinate.
Pentru a rezolva problema vom presupune <tex> A[0][0] </tex> cunoscut (de fapt, mai întâi vom rezolva problema presupunând că <tex> A[0][0] = 1 </tex>, iar dacă nu obţinem nicio soluţie vom încerca cu <tex> A[0][0] = 0 </tex>). Vom nota celulele <tex> A[0][1] </tex>, <tex> A[0][2]</tex>, … <tex> A[0][M - 1] </tex> cu <tex> x_{1} </tex>, <tex> x_{2} </tex>, … <tex> x_{M-1} </tex> iar celulele <tex> A[1][0] </tex>, <tex> A[2][0] </tex>, … <tex> A[N - 1][0] </tex> cu <tex> y_{1} </tex>, <tex> y_{2} </tex>, … <tex> y_{N-1} </tex>.

Fie <tex> A </tex> o matrice soluţie a problemei noastre. Vom numerota rândurile matricii de la $0$ la $N - 1$ şi coloanele de la $0$ la $M - 1$. Matricea de intrare <tex> S </tex> reprezintă de fapt sumele din fiecare pătrat de câte $2 x 2$ elemente. Facem observaţia că dacă ştim într-un pătrat de $2 x 2$ valorile pentru trei dintre celule, atunci valoarea din a patra celulă este unic determinată pentru că ştim suma elementelor din pătrat. Vedem astfel, că dacă ştim valorile elementelor din prima linie a matricii <tex> A </tex> şi din prima coloană, restul valorilor sunt unic determinate. Pentru a rezolva problema vom presupune <tex> A[0][0] </tex> cunoscut (de fapt, mai întâi vom rezolva problema presupunând că <tex> A[0][0] = 1 </tex>, iar dacă nu obţinem nicio soluţie vom încerca cu <tex> A[0][0] = 0 </tex>). Vom nota celulele <tex> A[0][1] </tex>, <tex> A[0][2]</tex>, <tex>...</tex>, <tex> A[0][M - 1] </tex> cu <tex> x_{1} </tex>, <tex> x_{2} </tex>, <tex>...</tex>, <tex> x_{M-1} </tex>, iar celulele <tex> A[1][0] </tex>, <tex> A[2][0] </tex>, <tex>...</tex>, <tex> A[N - 1][0] </tex> cu <tex> y_{1} </tex>, <tex> y_{2} </tex>, <tex>...</tex>, <tex> y_{N-1} </tex>.

table{width: 90px; text-align: center}.
| <tex> A[0][0] </tex> | <tex> x_{1} </tex> | <tex> x_{2} </tex> | <tex> ... </tex> | <tex> x_{M-1} </tex> |

| ... | ... | ... | ... | ... |
| <tex> y_{N-1} </tex> | <tex> 0 </tex> | <tex> 1 </tex> | ... | <tex> 1 </tex> |

Acum, pentru fiecare celulă putem demonstra prin inducţie că <tex> A[i][j] = (-1)^i x_{j} + (-1)^j y_{i} + b[i][j] </tex>. Unde <tex> b[i][j] </tex> sunt nişte constante ce sunt calculate în funcţie de matricea primită la intrare.
Este uşor de observat că dacă:
<tex> A[i-1][j] = (-1)^{(i-1)} x_{j} + (-1)^j y_{i-1} + b[i-1][j] </tex>,
<tex> A[i-1][j-1] = (-1)^{(i-1)} x_{j-1} + (-1)^{(j-1)} y_{i-1} + b[i-1][j-1] </tex>,
<tex> A[i][j-1] = (-1)^i x_{j-1} + (-1)^{(j-1)} y_{i} + b[i][j-1] </tex>,

Acum, pentru fiecare celulă putem demonstra prin inducţie că <tex> A[i][j] = (-1)^i x_{j} + (-1)^j y_{i} + b[i][j] </tex>. Unde <tex> b[i][j] </tex> sunt nişte constante ce sunt calculate în funcţie de matricea primită la intrare. Este uşor de observat că dacă:
 
<tex> A[i-1][j] = (-1)^{(i-1)} x_{j} + (-1)^j y_{i-1} + b[i-1][j] </tex>,
<tex> A[i-1][j-1] = (-1)^{(i-1)} x_{j-1} + (-1)^{(j-1)} y_{i-1} + b[i-1][j-1] </tex>,
<tex> A[i][j-1] = (-1)^i x_{j-1} + (-1)^{(j-1)} y_{i} + b[i][j-1] </tex>,

atunci:

<tex> A[i][j] = S[i-1][j-1] - A[i-1][j] - A[i][j-1] - A[i-1][j-1] = </tex>
<tex> = S[i-1][j-1] - ((-1)^{(i-1)} x_{j} + (-1)^j y_{i-1} + b[i-1][j]) - </tex> <tex> ((-1)^{(i-1)} x_{j-1} + (-1)^{(j-1)} y_{i-1} + b[i-1][j-1]) - ((-1)^i x_{j-1} + (-1)^{(j-1)} y_{i-1} + b[i][j-1]) = </tex>
<tex> = (-1)^i x_{j} - (-1)^j y_{i-1} + (-1)^i x_{j-1} + (-1)^j y_{i-1} - </tex> <tex> (-1)^i x_{j-1} + (-1)^j y_{i} + S[i-1][j-1] - b[i-1][j] - b[i][j-1] - b[i-1][j-1] = </tex>
<tex> = (-1)^i x_{j} + (-1)^j y_{i} + b[i][j] </tex>.

<tex> A[i][j] = </tex> <tex> S[i-1][j-1] - </tex> <tex> A[i-1][j] - </tex> <tex> A[i][j-1] - </tex> <tex> A[i-1][j-1] = </tex> <tex> S[i-1][j-1] - </tex> <tex> ((-1)^{(i-1)} x_{j} + </tex> <tex> (-1)^j y_{i-1} + </tex> <tex> b[i-1][j]) - </tex> <tex> ((-1)^{(i-1)} x_{j-1} + </tex> <tex> (-1)^{(j-1)} y_{i-1} + </tex> <tex> b[i-1][j-1]) - </tex> <tex> ((-1)^i x_{j-1} + </tex> <tex> (-1)^{(j-1)} y_{i-1} + </tex> <tex> b[i][j-1]) = </tex> <tex> (-1)^i x_{j} - </tex> <tex> (-1)^j y_{i-1} + </tex> <tex> (-1)^i x_{j-1} + </tex> <tex> (-1)^j y_{i-1} - </tex> <tex> (-1)^i x_{j-1} + </tex> <tex> (-1)^j y_{i} + </tex> <tex> S[i-1][j-1] - </tex> <tex> b[i-1][j] - </tex> <tex> b[i][j-1] - </tex> <tex> b[i-1][j-1] = </tex> <tex> (-1)^i x_{j} + </tex> <tex> (-1)^j y_{i} + </tex> <tex> b[i][j] </tex>.

De aici concluzionăm că <tex> b[i][j] = S[i-1][j-1] - b[i-1][j] - b[i][j-1] - b[i-1][j-1] \ (*)</tex>.

<tex> 0 \le y_{i} \le 1 </tex>
<tex> -b[i][j] \le (-1)^i x_{j} + (-1)^j y_{i} \le 1 - b[i][j] </tex>

Este uşor acum să transformăm acest sistem într-o formulă booleană în {'formă normal conjunctivă':2-sat#forme-normale} în care fiecare expresie are cel mult $2$ literali. Fiecare relaţie o putem înmulţi sau nu cu $-1$ astfel ca părţile constante ale relaţiei să fie pozitive. Observăm că <tex> | b[i][j] | \le 2 </tex>, altfel nu avem soluţie. Dacă <tex> | b[i][j] | = 2 </tex> atunci ambele variabile au valori fixe, iar dacă <tex> | b[i][j] | = 1 </tex> sau <tex> | b[i][j] | = 0 </tex> atunci relaţia o putem scrie ca o disjuncţie logică cu doi literali.
 
O relaţie precum <tex> 0 \le x + y \le 1 </tex> poate fi tansformată logic în <tex> \sim x \vee \sim y </tex>, astfel <tex> x </tex> şi <tex> y </tex> nu vor fi în acelaşi timp <tex> 1 </tex>, una de genul <tex> 1 \le x + y \le 2 </tex> va fi transformată în <tex> (x \vee y) </tex>, astfel cel puţin <tex> x </tex> sau <tex> y </tex> va fi egal cu <tex> 1 </tex>, alta de tipul <tex> 0 \le x - y \le 1 </tex> poate fi scrisă ca <tex> x \vee \sim y </tex>, una de tipul <tex> 2 \le x + y \le 3 </tex> în <tex> x \wedge y </tex>, iar una de tipul <tex> 0 \le -x -y \le 1 </tex> în <tex> \sim x \wedge \sim y </tex>, una de tipul <tex> 1 \le x - y  \le 2 </tex> în <tex> x \wedge \sim y </tex>.

Este uşor acum să transformăm acest sistem într-o formulă booleană în {'formă normal conjunctivă':2-sat#forme-normale} în care fiecare expresie are cel mult $2$ literali. Fiecare relaţie o putem înmulţi sau nu cu $-1$ astfel ca părţile constante ale relaţiei să fie pozitive. Observăm că <tex> -2 \le b[i][j] \le 3 </tex>, altfel nu avem soluţie. Dacă partea constantă minimă într-o relaţie este $2$ atunci ambele variabile au valori fixe, iar dacă este $1$ sau $0$ atunci relaţia o putem scrie ca o disjuncţie logică cu doi literali.

Astfel am redus problema la rezolvarea unei instanţe de $2-SAT$. Avem $N+M-1$ necunoscute şi {$(N-1)$}{$(M-1)$} propoziţii. Folosind a treia metodă de rezolvare vom obţine un algoritm de complexitate $O(N * M)$ care soluţionează problema noastră.

O relaţie precum <tex> 0 \le x + y \le 1 </tex> poate fi tansformată logic în <tex> \sim x \vee \sim y </tex>, astfel <tex> x </tex> şi <tex> y </tex> nu vor fi în acelaşi timp <tex> 1 </tex>, una de genul <tex> 1 \le x + y \le 2 </tex> va fi transformată în <tex> x \vee y </tex>, astfel cel puţin <tex> x </tex> sau <tex> y </tex> va fi egal cu <tex> 1 </tex>, alta de tipul <tex> 0 \le x - y \le 1 </tex> poate fi scrisă ca <tex> x \vee \sim y </tex>, una de tipul <tex> 2 \le x + y \le 3 </tex> în <tex> x \wedge y </tex>, iar una de tipul <tex> 0 \le -x -y \le 1 </tex> în <tex> \sim x \wedge \sim y </tex>, una de tipul <tex> 1 \le x - y  \le 2 </tex> în <tex> x \wedge \sim y </tex>. Astfel am redus problema la rezolvarea unei instanţe de $2-SAT$. Avem $N+M-1$ necunoscute şi @(N-1)*(M-1)@ propoziţii. Folosind {'a treia metodă de rezolvare':2-sat#solutie-3} vom obţine un algoritm de complexitate $O((M + N)^2^)$ care soluţionează problema noastră.

Să vedem cum merge acestă rezolvare pe exemplul din problemă:

h2(#probleme). Probleme propuse

Pentru a vă familiariza cu subiectul prezentat în acest articol, vă propunem să încercati să rezolvaţi următoarele probleme:
# 'Excursion':www.oi.edu.pl/download/boi-2001.pdf - Baltic Olympiad in Informatics, 2001
# 'Peace Commision':http://www.oi.edu.pl/php/show.php?ac=e100000&module=show&file=zadania/oi8/spokojna - Polish Olympiad in Informatics, 2001

Pentru a vă familiariza cu subiectul prezentat în acest articol, vă propunem să încercaţi să rezolvaţi următoarele probleme:
 
# '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

h2(#bibliografie). Bibliografie:

# T. H. Cormen, C. E. Leiserson, R. R. Rivest - '_Introducere in Algoritmi_':http://zhuzeyuan.hp.infoseek.co.jp/ita/toc.htm

# T. H. Cormen, C. E. Leiserson, R. R. Rivest - '_Introducere în Algoritmi_':http://zhuzeyuan.hp.infoseek.co.jp/ita/toc.htm

# '_Satisfiability_':http://en.wikipedia.org/wiki/Satisfiability, Wikipedia
# '_BOI 2001 Competition Material_':http://www.oi.edu.pl/download/boi-2001.pdf
# '_CEOI 2002 Competition Material_':http://ics.upjs.sk/ceoi/Documents.html

3704