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

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

(Categoria _Algoritmi_, Autor _Cosmin Negruşeri_)

(toc){width: 37em}*{text-align:center} *Conţinut:*

(toc){width: 30em}*{text-align:center} *Conţinut:*

* {'Introducere':2-sat#introducere}
* {'Forme normale ale formulelor logice':2-sat#forme-normale}
* {'SAT, 3-SAT, 2-SAT':2-sat#overview-sat}
* {'Soluţii pentru 2-SAT':2-sat#solutii-2-sat}

** {'Soluţie $O(M * 2^N^)$':2-sat#solutie1}
** {'Soluţie $O(N * M)$':2-sat#solutie2}
** {'Soluţie $O(N^2^)$':2-sat#solutie3}
** {'Soluţie $O(M + N)$':2-sat#solutie4}

** {'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(M + N)$':2-sat#solutie-4}

* {'Aplicaţii':2-sat#aplicatii}
** {'Party (preOni 2003/2004)':2-sat#party}
** {'Cigraf':2-sat#cigraf}

Un exemplu de problemă $2-SAT$ ar fi satisfiabilitatea formulei <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>. Această formulă este satisfăcută de valorile <tex> \langle x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = 1 \rangle </tex>. Pentru a satisface întreaga expresie trebuie ca în fiecare propoziţie cel puţin unul din cei doi literali să aibă valoarea de adevăr <tex> 1 </tex>.

h3(#solutie1). Soluţie $O(M * 2^N^)$

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

O primă metodă de rezolvare ar fi să încercăm toate cele $2^N^$ posibilităţi de atribuire posibilă, dar această metodă are ordinul de complexitate $O(M * 2^N^)$ şi este eficientă doar pentru instanţe mici ale problemei.

h3(#solutie2). Soluţie $O(N * M)$

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

Următoarea soluţie pare trivială, dar găsirea acestui algoritm şi realizarea faptului că el rezolvă corect problema este mai grea 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$. Dacă literalul în care apare $p$ este negat atunci îi atribuim valoarea $1$. Pentru ca propoziţia respectivă să aibă $1$ valoarea de adevăr atunci valoarea lui $q$ este 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ă. 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 eliminate 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>.

h3(#solutie3). Soluţie $O(N^2^)$

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

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

Astfel, numărul mediu de paşi ai algoritmului este $2N^2^ - N$ iar dacă aplicăm algoritmul în mod aleator de mai multe ori avem o probabilitate foarte mare să ajungem la rezultat.

h3(#solutie4). Soluţie $O(M + N)$

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:

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/
* [5] 'Componente tare conexe':problema/ctc

* [1] T. H. Cormen, C. E. Leiserson, R. R. Rivest - '_Introducere in Algoritmi_':http://zhuzeyuan.hp.infoseek.co.jp/ita/toc.htm
* [2] '_Satisfiability_':http://en.wikipedia.org/wiki/Satisfiability, Wikipedia
* [3] 'BOI 2001 Competition Material':http://www.oi.edu.pl/download/boi-2001.pdf
* [4] 'CEOI 2002 Competition Material':http://ics.upjs.sk/ceoi/Documents.html