Problema satisfiabilităţii formulelor logice de ordinul doi

(Categoria Algoritmi, Autor Cosmin Negruşeri)

Introducere

Problema satisfiabiltăiţii, notată prescurtat cu SAT, cere determinarea existenţei pentru o formulă booleană a unei artibuiri satisfiabile. O formulă booleană este compusă din variabile logice , operatori logici ( şi,  sau, non, implicaţie şi 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 şi în loc de adevărat şi fals.

Un exemplu de formulă ar fi . Aceasta are atribuirea satisfiabilă pentru că .

Forme normale ale formulelor logice

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: care are pe ca primă propoziţie cu literalii , , .

• 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: .

SAT, 3-SAT, 2-SAT

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.

Soluţii pentru 2-SAT

Un exemplu de problemă 2SAT ar fi satisfiabilitatea formulei . Această formulă este satisfăcută de valorile . 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.

Soluţie O(M * 2^N)

O primă metodă de rezolvare ar fi să încercăm toate cele 2⁴ 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.

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: , , , . Propoziţii de tip nu pot apărea pentru că toate schimbările forţate au fost deja propagate. Dacă apare o propoziţie 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 atunci expresia nu poate fi satisfăcută. Propoziţiile de forma , , 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: . Considerăm propoziţia şi . Astfel, vom obţine mai departe . În propoziţia trebuie să fie egal cu . Acum, expresia devine: . Din propoziţia obţinem , iar din obţinem . Deci, atribuirea satisfiabilă este .

Soluţie O(N²)

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

atribuim valori booleene arbitrare variabilelor;
cât timp expresia nu este satisfăcută execută
    găsim o propoziţie cu valoarea de adevăr 0;
    schimbăm valoarea de adevăr a oricăreia dintre cele două variabile prezente în propoziţie;  // ceea ce va face ca acea propoziţie să aibă noua valoare de adevăr 1;
sfcâttimp

De ce ar merge acest algoritm? Să presupunem că există o soluţie a problemei, o notăm cu S, iar cu X notăm şirul valorilor curente ale variabilelor. Ne uităm la fiecare pas al algoritmului la numărul de variabile care au valori diferite în soluţie faţă de cele din X (acest număr de diferenţe între elementele de acelaşi index pentru două şiruri se mai numeşte şi distanţă Hamming între şiruri). Fie această valoare la pasul current K. Noi am vrea să avem K = 0. Cum va evolua K pe parcursul algoritmului? La un moment dat noi schimbăm valoarea unei variabile luate aleator dintr-o propoziţie nesatisfăcută. Pentru că în S propoziţia este satisfăcută, înseamnă că cel puţin una dintre cele două variabile ale propoziţiei are valori diferite în X faţă de S. Astfel, operaţia făcută de noi are probabilitate de cel puţin 0.5 să ne aducă mai aproape de soluţie. Vom nota cu numărul probabil de paşi în care un şir X aflat la distanţa Hamming egală cu i faţă de S, va fi transformat în S. Evident:

.

Se pune semnul de inegalitate pentru că ambele variabile pot avea valori diferite faţă de cele din soluţie, deci schimbarea valorii oricăreia ar putea să ne aducă mai aproape de soluţie.

Pentru că dacă toate variabilele diferă de soluţie, orice schimbare ne aduce mai aproape de soluţie:

Ne interesează numai limitele superioare, deci folosim doar egalităţi în loc de inegalităţi:

Dacă adunăm toate ecuaţiile obţinem:

De aici avem că , din avem . Mai departe avem că de unde, când avem că .

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