** {'Excursion (Baltic Olympiad in Informatics, 2001)':2-sat#excursion}
** {'Orpath (Olimpiadă Rusia)':2-sat#orpath}
** {'Aladdin (Bursele Agora 2005/2006, Runda 1)':2-sat#aladdin}

* {'Bibliografie':2-sat#bibliografie}

h2(#introducere). Introducere

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

Alegem <tex> A[0][0] = 1 </tex>. Necunoscutele vor fi <tex> x_{1} </tex>, <tex> x_{2} </tex>, <tex> x_{3} </tex> şi <tex> y_{1} </tex>, <tex> y_{2} </tex>, <tex> y_{3} </tex>.
 
table{width: 90px; text-align: center}.
| <tex> 1 </tex> | <tex> x_{1} </tex> | <tex> x_{2} </tex> | <tex> x_{3} </tex> |
| <tex> y_{1} </tex> | <tex> A[1][1] </tex> | <tex> A[1][2] </tex> | <tex> A[1][3] </tex> |
| <tex> y_{2} </tex> | <tex> A[2][1] </tex> | <tex> A[2][2] </tex> | <tex> A[2][3] </tex> |
| <tex> y_{3} </tex> | <tex> A[3][1] </tex> | <tex> A[3][2] </tex> | <tex> A[3][3] </tex> |
 
Folosind recurenţa <tex> (*) </tex> obţinem că matricea <tex> b </tex> este:
 
table{width: 90px; text-align: center}.
| <tex> 1 </tex> | <tex> 0 </tex> | <tex> 0 </tex> | <tex> 0 </tex> |
| <tex> 0 </tex> | <tex> 2 </tex> | <tex> 0 </tex> | <tex> 3 </tex> |
| <tex> 0 </tex> | <tex> 0 </tex> | <tex> 1 </tex> | <tex> -1 </tex> |
| <tex> 0 </tex> | <tex> 1 </tex> | <tex> 0 </tex> | <tex> 1 </tex> |
 
De aici obţinem sistemul de inegalităţi:
 
<tex> 0 \le x_{1} \le 1,  0 \le x_{2} \le 1, 0 \le x_{3} \le 1, </tex>
<tex> 0 \le y_{1} \le 1, -2 \le -x_{1} - y_{1} \le -1, 0 \le -x_{2} + y_{1} \le 1, -3 \le -x_{3} - y_{1} \le -2, </tex>
<tex> 0 \le y_{2} \le 1,  0 \le  x_{1} - y_{2} \le  1,-1 \le  x_{2} + y_{2} \le 0,  1 \le  x_{3} - y_{2} \le  2, </tex>
<tex> 0 \le y_{3} \le 1, -1 \le -x_{1} - y_{3} \le  0, 0 \le -x_{2} + y_{3} \le 1, -1 \le -x_{3} - y_{3} \le  0 </tex>
 
Transformăm relaţiile astfel ca să nu apară nici o constantă negativă:
 
<tex> 0 \le x_{1} < = 1, 0 \le x_{2} \le 1, 0 \le x_{3} \le  1, </tex>
<tex> 0 \le y_{1} \le 1, 1 \le x_{1} + y_{1} \le 2, 0 \le -x_{2} + y_{1} \le 1, 2 \le x_{3} + y_{1} \le 3, </tex>
<tex> 0 \le y_{2} \le 1, 0 \le x_{1} - y_{2} \le 1, 0 \le -x_{2} - y_{2} \le 1, 1 \le x_{3} - y_{2} \le 2, </tex>
<tex> 0 \le y_{3} \le 1, 0 \le x_{1} + y_{3} \le 1, 0 \le -x_{2} + y_{3} \le 1, 0 \le x_{3} + y_{3} \le 1 </tex>
 
Acest sistem poate fi transformat într-o expresie booleană:
 
<tex> (x_{1} \vee y_{1}) \wedge (\sim x_{2} \vee y_{1}) \wedge (x_{3} \wedge y_{1}) \wedge </tex>
<tex> (x_{1} \vee \sim y_{2}) \wedge (\sim x_{2} \wedge \sim y_{2}) \wedge (x_{3} \wedge \sim y_{2}) \wedge </tex>
<tex> (\sim x_{1} \vee \sim y_{3}) \wedge (\sim x_{2} \vee y_{3}) \wedge (\sim x_{3} \vee \sim y_{3}) </tex>.
 
Acestă expresie e satisfăcută de valorile: <tex> \langle x_{1} = 1, x_{2} = 0, x_{3} = 1, y_{1} = 1, y_{2} = 0, y_{3} = 0 \rangle </tex>, iar de aici putem determina o soluţie a problemei noastre iniţiale ca fiind:
 
table{width: 90px; text-align: center}.
| <tex> 1 </tex> | <tex> 1 </tex> | <tex> 0 </tex> | <tex> 1 </tex> |
| <tex> 1 </tex> | <tex> 0 </tex> | <tex> 1 </tex> | <tex> 1 </tex> |
| <tex> 0 </tex> | <tex> 1 </tex> | <tex> 1 </tex> | <tex> 0 </tex> |
| <tex> 0 </tex> | <tex> 0 </tex> | <tex> 0 </tex> | <tex> 0 </tex> |
 
h2(#bibliografie). Bibliografie:
 
* [1] '"Introducere in algoritmi"':http://zhuzeyuan.hp.infoseek.co.jp/ita/toc.htm, T. H. Cormen, C. E. Leiserson, R. R. Rivest
* [2] 'Satisfiability':http://en.wikipedia.org/wiki/Satisfiability, Wikipedia
* [3] "BOI'01 Competition material":http://www.oi.edu.pl/download/boi-2001.pdf
* [4] "CEOI'02 Competition material":http://ics.upjs.sk/ceoi/