Problema satisfiabilităţii formulelor logice de ordinul doi

Problema satisfabilităţii formulelor logice de ordinul doi

h1. Problema satisfiabilităţii formulelor logice de ordinul doi
 
(Categoria _Algoritmi_, Autor _Cosmin Negruşeri_)
 
Problema satisfiabiltăiţii notată prescurtat cu $SAT$ cere determinarea existenţei pentru o formulă booleană <tex> \phi </tex> a unei artibuiri satisfiabile. O formulă booleană <tex> \phi </tex> este compusă din $variabile$ logice ( $x{~1~}$, $x{~2~}$,… ), $operatori$ logici ( <tex> \wedge </tex> şi,  <tex> \vee </tex> sau, <tex> \sim </tex> non, <tex> \rightarrow </tex> implicaţie şi <tex> \leftrightarrow </tex> echivalenţă), şi $paranteze$. O atribuire de valori booleene pentru variabilele acestei expresii se numeşte $atribuire satisfiabilă$ dacă evaluarea expresiei după atribuirea valorilor dă ca rezultat valoarea de adevăr $adevărat$. De acum încolo vom folosi pentru simplitate valorile $1$ şi $0$ în loc de $adevărat$ şi $fals$.
 
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 are atribuirea satisfiabilă <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex> pentru că <tex> \phi = ((0 \rightarrow 0) \vee \sim((\sim 0 \leftrightarrow 1) \vee 1)) \wedge \sim 0 = (1 \vee \sim (1 \vee 1)) \wedge 1 = (1 \vee 0) \wedge 1 = 1</tex>.
 
Orice formulă booleană poate fi transformată în două forme:
 
* $Forma normal conjunctivă$ în care expresia este exprimată ca o conjuncţie de propoziţii, iar fiecare propoziţie este formată din o disjuncţie de $literali$. Un $literal$ este o variabilă care poate fi sau nu negată. Un exemplu de expresie în forma normal conjunctivă ar fi: <tex> (x_{1} \vee \sim x_{1} \vee \sim x_{2}) \wedge (x_{3} \vee x_{2} \vee x_{4}) \wedge (\sim x_{1} \vee \sim x_{3} \vee \sim x_{4}) </tex> care are pe <tex> (x_{1} \vee \sim x_{1} \vee \sim x_{2}) </tex> ca primă propoziţie cu literalii <tex> x_{1} </tex>, <tex> \sim x_{1} </tex>, <tex> \sim x_{2} </tex>.
 
* $Forma normal disjunctivă$ este formată ca o disjuncţie de propoziţii, fiecare dintre aceste propoziţii fiind o conjuncţie de literali. Un exemplu de o asemenea formulă ar fi următoarea: <tex> (x_{1} \wedge x_{2} \wedge x_{3}) \vee (x_{1} \wedge \sim x_{2} \wedge x_{3}) \vee (x_{1} \wedge \sim x_{2} \wedge \sim x_{3}) \vee (\sim x_{1} \wedge x_{2} \wedge \sim x_{2}) </tex>.
 
Problema $SAT$ este $NP-completă$. Defapt, este prima problemă $NP-completă$ găsită. Stephen Cook a demonstrat $NP-completitudinea$ ei în 1971. Pe vremea aceea nu se ştia nici măcar că problemele $NP-complete$ există. Această problemă rămâne $NP-completă$ chiar dacă restricţionăm expresiile la unele care în forma normal conjunctivă au doar trei literali. Problema satisfiabilităţii pentru asemenea expresii se numeşte $3SAT$, şi multe probleme pot fi demonstrate a fi $NP-complete$ prin reducerea la această problemă. Din fericire, problema $2SAT$, adică cea pentru care în fiecare propoziţie există doar $2$ literali se poate rezolva eficient. Restul articolului va prezenta trei metode de rezolvare a problemei $2SAT$ şi câteva aplicaţii ale acesteia la concursuri de programare.
Un exemplu de problemă $2SAT$ 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 $1$.

h1. Problema satisfabilităţii formulelor logice de ordinul doi
(Categoria _Structuri de date_, Autor _Cosmin Negruşeri_)