2-satisfacție

2-satisfacibilitatea (sau 2-SAT ) este o problemă de satisfacție booleană cu clauze constând din perechi de literali . Este un caz particular (cel mai simplu) al problemei n-SAT și este singurul a cărui solvabilitate în timp polinomial și spațiu logaritmic a fost demonstrată. În schimb, probleme de satisfacție cu $n>2$ ${\ displaystyle n> 2}$ $n> 2$ toate sunt NP-complete , fiind atât SAT generic ( prin teorema lui Cook ), cât și 3-SAT (deoarece fiecare problemă n-SAT este reductibilă la 3-SAT în timp polinomial).

Graficul implicațiilor pentru exemplul 2-SAT prezentat opus

O problemă 2-SAT poate fi descrisă folosind o expresie booleană în formă conjunctivă normală , adică o conjuncție de disjuncții :

(x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land

{\ displaystyle (x_ {0} \ lor x_ {2}) \ land (x_ {0} \ lor \ lnot x_ {3}) \ land (x_ {1} \ lor \ lnot x_ {3}) \ land ( x_ {1} \ lor \ lnot x_ {4}) \ land}

{\ displaystyle (x_ {0} \ lor x_ {2}) \ land (x_ {0} \ lor \ lnot x_ {3}) \ land (x_ {1} \ lor \ lnot x_ {3}) \ land ( x_ {1} \ lor \ lnot x_ {4}) \ land}

(x_{2}\lor \lnot x_{4})\land {}(x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land

{\ displaystyle (x_ {2} \ lor \ lnot x_ {4}) \ land {} (x_ {0} \ lor \ lnot x_ {5}) \ land (x_ {1} \ lor \ lnot x_ {5} ) \ land (x_ {2} \ lor \ lnot x_ {5}) \ land}

{\ displaystyle (x_ {2} \ lor \ lnot x_ {4}) \ land {} (x_ {0} \ lor \ lnot x_ {5}) \ land (x_ {1} \ lor \ lnot x_ {5} ) \ land (x_ {2} \ lor \ lnot x_ {5}) \ land}

(x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).

{\ displaystyle (x_ {3} \ lor x_ {6}) \ land (x_ {4} \ lor x_ {6}) \ land (x_ {5} \ lor x_ {6}).}

{\ displaystyle (x_ {3} \ lor x_ {6}) \ land (x_ {4} \ lor x_ {6}) \ land (x_ {5} \ lor x_ {6}).}

Acest formular se mai numește „2-CNF”, unde „2” indică numărul de litere pentru fiecare clauză.

Problema este de a atribui o valoare booleană (adevărată sau falsă) fiecărui literal din formulă, astfel încât expresia să producă valoarea „adevărat”. În exemplul de mai sus, există 16 combinații de valori booleene care fac formula adevărată (o posibilă atribuire satisfăcătoare este una care atribuie tuturor variabilelor valoarea „adevărat”). În consecință, instanța 2-SAT reprezentată de această expresie este satisfăcătoare.

O altă metodă de reprezentare a problemei este graficul implicațiilor . ^[1]

Algoritm pentru rezolvarea problemei 2-SAT

Având în vedere o formulă în CNF ( conjuncții de disjuncții ale literelor ) creăm un grafic G = <V, E> unde V este setul de noduri ale graficului și E este setul de margini ale graficului. Graficul G este creat astfel:

pentru fiecare literal se creează două noduri, pentru literalul negat și pentru literal negat;
$\exists$ ${\ displaystyle \ există}$ $\ există$ ( $\alpha \lor \beta$ ${\ displaystyle \ alpha \ lor \ beta}$ ${\ displaystyle \ alpha \ lor \ beta}$ ) $\in$ ${\ displaystyle \ in}$ $\în$ Și dacă și numai dacă există o clauză echivalentă cu ( $\urcorner \alpha \lor \beta$ ${\ displaystyle \ urcorner \ alpha \ lor \ beta}$ ${\ displaystyle \ urcorner \ alpha \ lor \ beta}$ ).

Formula este nesatisfăcătoare dacă există o cale de la $\alpha$ ${\ displaystyle \ alpha}$ $\ alfa$ la $\urcorner \alpha$ ${\ displaystyle \ urcorner \ alpha}$ ${\ displaystyle \ urcorner \ alpha}$ (sau vice versa).

Notă

^ Aspvall, Bengt; Plass, Michael F .; Tarjan, Robert E. , Un algoritm în timp liniar pentru testarea adevărului anumitor formule booleene cuantificate , în Information Processing Letters , vol. 8, nr. 3, 1979, pp. 121–123, DOI : 10.1016 / 0020-0190 (79) 90002-4 .

Portalul de matematică : accesați intrările Wikipedia care se ocupă de matematică

[1] Aspvall, Bengt; Plass, Michael F .; Tarjan, Robert E. , Un algoritm în timp liniar pentru testarea adevărului anumitor formule booleene cuantificate , în Information Processing Letters , vol. 8, nr. 3, 1979, pp. 121–123, DOI : 10.1016 / 0020-0190 (79) 90002-4 .

[1]