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ă 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ă .
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: .
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 . 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.
O primă metodă de rezolvare ar fi să încercăm toate cele 24 posibilităţi de atribuire posibilă, dar această metodă are ordinul de complexitate O(M * 2N) şi este eficientă doar pentru instanţe mici ale problemei.
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 .
O altă soluţie elegantă se bazează pe o metodă randomizată:
- pornim întâi cu o atribuire de valori booleene oarecare variabilelor;
- găsim o propoziţie cu valoarea de adevăr ;
- vom schimba 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 ;
- cât timp expresia nu este satisfăcută repetăm acest procedeu de schimbare a valorii unei variabile dintr-o propoziţie nesatisfăcută, deci revenim la pasul 2.