Problema satisfabilităţii formulelor logice de ordinul doi

Problema satisfiabilităţii formulelor logice de ordinul doi

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

(Categoria _Structuri de date_, Autor _Cosmin Negruşeri_)