Problemă de satisfacție pentru formulele booleene

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 15 iunie 2021; verificările necesită 3 modificări .

Problema satisfacabilităţii formulelor booleene ( SAT , vyp ) este o problemă algoritmică importantă pentru teoria complexităţii computaţionale .

O instanță de activitate este o formulă booleană constând numai din nume de variabile, paranteze și operații ( ȘI ), ( SAU ) și ( HE ). Problema este: este posibil să se atribuie valori false și adevărate tuturor variabilelor care apar în formulă, astfel încât formula să devină adevărată. $\pană$ $\vee$ $\neg$

Conform teoremei lui Cook , demonstrată de Stephen Cook în 1971, problema SAT pentru formulele booleene scrise în formă normală conjunctivă este NP-complet . Cerința scrierii în formă conjunctivă este esențială, întrucât, de exemplu, problema SAT pentru formulele prezentate în formă normală disjunctivă se rezolvă trivial în timp liniar în funcție de mărimea înregistrării formulei (pentru ca formula să fie satisfăcătoare, doar prezența este necesară cel puţin o conjuncţie care nu conţine simultan şi negaţie pentru o variabilă ). $X$ $\neg x$ $X$

Formulare precisă

Pentru a formula cu precizie problema recunoașterii , se fixează un alfabet finit, cu ajutorul căruia sunt specificate instanțe de limbaj. Hopcroft , Motwani și Ullman în cartea lor Introduction to Automata Theory , Languages, and Computation sugerează utilizarea următorului alfabet : . $\{\wedge,\vee,\neg,(,),x,0,1\)$

Când se utilizează acest alfabet, parantezele și operatorii sunt scrise în mod natural, iar variabilele primesc următoarele nume: , în funcție de numerele lor în notație binară . $x1,x10,x11,x100,\dots$

Să fie o formulă booleană , scrisă în notația matematică obișnuită, să aibă lungimea caracterelor. În ea, fiecare apariție a fiecărei variabile a fost descrisă de cel puțin un simbol, prin urmare, nu există mai mult decât variabile în această formulă. Aceasta înseamnă că în notația propusă mai sus, fiecare variabilă va fi scrisă folosind simboluri. În acest caz, întreaga formulă din noua notație va avea lungimea caracterelor, adică lungimea șirului va crește de un număr polinom de ori. $N$ $N$ $O\stânga(\log{N}\dreapta)$ $O\stânga(N\log{N}\dreapta)$

De exemplu, formula va lua forma . $a\wedge\neg(b\vee c)$ $x1\wedge\neg(x10\vee x11)$

Complexitate computațională

Într-o lucrare din 1970 a lui Stephen Cook , termenul „ problema NP-completă ” a fost introdus pentru prima dată , iar problema SAT a fost prima problemă pentru care această proprietate a fost dovedită.

În demonstrarea teoremei lui Cook, fiecare problemă din clasa NP este redusă explicit la SAT. După apariția rezultatelor lui Cook, NP-completitudinea a fost dovedită pentru multe alte probleme. În acest caz, de cele mai multe ori, pentru a demonstra NP-completitudinea unei anumite probleme, se dă reducerea polinomială a problemei SAT la problema dată, eventual în mai multe etape, adică folosind mai multe probleme intermediare.

Cazuri speciale ale problemei SAT

Cazuri speciale importante și interesante ale problemei SAT sunt:

problema satisfacabilității formulelor booleene în formă normală conjunctivă (SATCNF sau VKNF) este o problemă similară, cu o condiție impusă formulei: trebuie scrisă în formă normală conjunctivă ; de asemenea NP-complet ;
problema de satisfacție pentru formule booleene în formă normală k-conjunctivă (k-SAT sau k-SAT) - problemă de satisfacție, cu condiția ca formula să fie scrisă în formă normală k-conjunctivă ; această problemă este NP-completă pentru . Pentru a rezolva problema, puteți utiliza algoritmul probabilistic Schoening ; $k\geq 3$
problema de satisfacție pentru formulele booleene în formă normală 2-conjunctivă are o soluție polinomială, adică aparține clasei P .

Rezolvatori CDCL

Una dintre cele mai eficiente metode de paralelizare a sarcinilor SAT este solutoarele CDCL (CDCL, English conflict-driven clause learning ), bazate pe variante non-cronologice ale algoritmului DPLL [1] [2] .

Vezi și

Note

↑ Marques-Silva JP GRASP: A search algorithm for propositional satisfaciability / JP Marques-Silva, KA Sakallah // IEEE Transactions on Computers. - 1999. - Vol. 48, nr 5. - P. 506-521.
↑ Semenov A. A., Zaikin O. S. Algoritmi pentru construirea mulțimilor de descompunere pentru paralelizarea în blocuri mari a problemelor SAT. Seria „Matematică” 2012. V. 5, Nr. 4. S. 79-94

Link -uri

Pagina web a Competițiilor SAT internaționale
Sat Live este un site general despre SAT.

Probleme NP-complete
Problema de maximizare a stivuirii (ambalării)	Ambalare in containere ambalare bidimensională ambalare liniară ambalare după greutate ambalare după valoare Problema rucsacului
teoria grafurilor teoria multimelor	Problemă de acoperire a vârfurilor Faceți clic pe problemă Problema unei multimi (multimi) independente Setați problema acoperirii Problema lui Steiner Problema vânzătorului ambulant Problemă generalizată a vânzătorului ambulant
Probleme algoritmice	Problemă de satisfacție pentru formulele booleene (în formă normală conjunctivă)
Jocuri de logică și puzzle-uri	Etichete generalizate (joc în N 2 -1) cea mai scurta solutie problema Probleme ale căror soluții sunt aplicate în Tetris Problemă generalizată de Sudoku Problemă de umplere a pătratului latin Sarcina lui Kakuro
Clasele de dificultate Cercetare operațională Optimizare Optimizare combinatorie Matematică aplicată Teoria algoritmilor Programare dinamică 21 Problemă Karp NP-completă