Atenţie! Aceasta este o versiune veche a paginii, scrisă la 2008-12-09 16:50:10.
Revizia anterioară   Revizia următoare  

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ă \phi a unei artibuiri satisfiabile. O formulă booleană \phi este compusă din variabile logice ( x1, x2,… ), operatori logici ( \wedge şi,  \vee sau, \sim non, \rightarrow implicaţie şi \leftrightarrow 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 \phi = ((x_{1} \rightarrow x_{2}) \vee \sim((\sim x_{1} \leftrightarrow x_{3}) \vee x_{4})) \wedge \sim x_{2} . Aceasta are atribuirea satisfiabilă \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle pentru că \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.

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: (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}) care are pe (x_{1} \vee \sim x_{1} \vee \sim x_{2}) ca primă propoziţie cu literalii x_{1} , \sim x_{1} , \sim x_{2} .
  • 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: (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}) .

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 (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}) . Această formulă este satisfăcută de valorile \langle x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = 1 \rangle . 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.