În logică și informatică, problema satisfiabilității booleene (numită uneori și problema satisfiabilității propoziționale și abreviată SATISFIABILITY, SAT sau B-SAT) pune întrebarea dacă există o care o formulă booleană dată. Cu alte cuvinte, se verifică dacă variabilele formulei pot fi înlocuite în mod coerent cu valorile TRUE sau FALSE astfel încât formula să se evalueze la TRUE. Dacă acest lucru este posibil, formula este numită satisfiabilă, iar în caz contrar nesatisfiabilă.
De exemplu, formula „a AND NOT b” este satisfiabilă deoarece se pot alege valorile a = TRUE și b = FALSE, ceea ce face ca (a AND NOT b) = TRUE. În schimb, formula „a AND NOT a” este nesatisfiabilă.
SAT este prima problemă despre care s-a demonstrat că este NP-completă — rezultat cunoscut sub numele de . Aceasta înseamnă că toate problemele din clasa de complexitate NP, care include o gamă largă de probleme naturale de decizie și optimizare, sunt cel mult la fel de dificile ca SAT. Nu se cunoaște niciun algoritm care să rezolve eficient fiecare instanță SAT (unde „eficient” înseamnă „determinist în timp polinomial”). Deși se crede în general că un astfel de algoritm nu există, această ipoteză nu a fost demonstrată sau infirmată matematic. Rezolvarea întrebării dacă SAT admite un algoritm în timp polinomial ar rezolva problema P versus NP — una dintre cele mai importante probleme deschise din teoria calculului.
Totuși, începând cu 2007, algoritmii euristici pentru SAT pot rezolva instanțe care implică zeci de mii de variabile și formule alcătuite din milioane de simboluri, ceea ce este suficient pentru numeroase aplicații practice ale SAT în inteligență artificială, și .
Definiții
O , numită și expresie booleană, este construită din variabile, operatorii AND (, notată ∧), OR (disjuncție, ∨), NOT (, ¬) și paranteze. O formulă este satisfiabilă dacă poate deveni TRUE prin atribuirea unor (TRUE sau FALSE) variabilelor sale.
Problema satisfiabilității booleene (SAT) constă în a determina, pentru o formulă dată, dacă aceasta este satisfiabilă. Această problemă de decizie are o importanță centrală în numeroase domenii ale informaticii, inclusiv , teoria complexității, , criptografie și inteligență artificială.
Forma normală conjunctivă
Un literal este fie o variabilă (caz în care se numește literal pozitiv), fie negația unei variabile (literal negativ). O clauză este o disjuncție de literali (sau un singur literal). O clauză se numește dacă conține cel mult un literal pozitiv. O formulă este în (CNF) dacă este o conjuncție de clauze.
De exemplu, este un literal pozitiv, este un literal negativ, iar este o clauză. Formula
este în formă normală conjunctivă. Aceasta este satisfiabilă dacă se aleg valorile x1 = FALSE, x2 = FALSE, iar x3 arbitrar.
În schimb, formula CNF a ∧ ¬a este nesatisfiabilă.
Prin legile , orice formulă de logică propozițională poate fi transformată într-o formulă echivalentă în formă normală conjunctivă, deși aceasta poate deveni exponențial mai lungă. De exemplu, transformarea formulei
în CNF produce o formulă cu clauze.
Totuși, utilizând , se poate construi o formulă CNF echisatisfiabilă a cărei lungime este liniară în raport cu dimensiunea formulei inițiale.
Complexitate
SAT a fost prima problemă despre care s-a demonstrat că este NP-completă, rezultat obținut de Stephen Cook la University of Toronto în 1971 și independent de în 1973.
Până la acel moment, conceptul de problemă NP-completă nici măcar nu fusese definit. Demonstrația arată că orice problemă de decizie din clasa NP poate fi redusă în timp polinomial la problema SAT pentru formule în (CNF), uneori numită CNFSAT.
O proprietate utilă a reducerii lui Cook este că aceasta păstrează numărul soluțiilor acceptate. De exemplu, problema determinării dacă un graf admite o colorare cu 3 culori aparține clasei NP; dacă un graf are 17 colorări valide cu trei culori, formula SAT obținută prin reducerea Cook–Levin va avea exact 17 atribuiri satisfăcătoare.
Rezultatul NP-completitudinii se referă doar la complexitatea în cel mai defavorabil caz. În practică, multe instanțe întâlnite în aplicații pot fi rezolvate mult mai rapid decât ar sugera analiza teoretică.
3-satisfiabilitate
Problema 3-SAT este varianta SAT în care fiecare clauză din CNF conține cel mult trei literali. Această problemă este de asemenea NP-completă și reprezintă una dintre cele .
Pentru a reduce problema SAT generală la 3-SAT, fiecare clauză de forma
poate fi transformată într-o conjuncție de clauze noi, introducând variabile auxiliare. Deși formulele rezultate nu sunt logic echivalente, ele sunt . Lungimea formulei rezultate crește doar polinomial.
3-SAT este frecvent utilizată ca punct de plecare pentru demonstrarea faptului că alte probleme sunt NP-hard. Acest lucru se realizează printr-o de la 3-SAT la problema respectivă.
De exemplu, pentru o formulă CNF cu c clauze se poate construi un graf cu un vârf pentru fiecare literal și cu muchii între literalii compatibili din clauze diferite. Graful are o clice de dimensiune c dacă și numai dacă formula este satisfiabilă.
Există și algoritmi randomizați pentru 3-SAT. Un exemplu este algoritmul lui Schöning (1999), care rulează în timp , unde n este numărul variabilelor, și decide corect problema cu probabilitate mare.
(exponential time hypothesis, ETH) afirmă că nu există niciun algoritm care să rezolve 3-SAT în timp subexponențial în raport cu numărul variabilelor.
Generalizarea problemei 3-SAT conduce la k-SAT, în care fiecare clauză conține cel mult k literali. Pentru orice k ≥ 3, problema rămâne NP-completă.
Studiile statistice ale instanțelor aleatoare de k-SAT au arătat existența unor transformări de fază în funcție de raportul dintre numărul de clauze și numărul de variabile. Pentru un anumit prag critic, formulele sunt satisfiabile cu probabilitate mare, iar peste acest prag devin nesatisfiabile cu probabilitate mare.
Pentru formulele aleatoare de tip 3-SAT, această transformare apare aproximativ la raportul clauze/variabile ≈ 4,26.
Instanțe speciale ale problemei 3SAT
Forma normală conjunctivă (în special cu 3 literali pe clauză) este adesea considerată reprezentarea canonică pentru formulele SAT. După cum s-a arătat mai sus, problema SAT generală poate fi redusă la 3-SAT, adică problema determinării satisfiabilității formulelor aflate în această formă.
SAT liniar O formulă 3-SAT este numită SAT liniar (LSAT) dacă fiecare clauză (privită ca mulțime de literali) intersectează cel mult o altă clauză și, în plus, dacă două clauze se intersectează, atunci ele au exact un literal în comun. O formulă LSAT poate fi reprezentată ca un set de intervale semiînchise disjuncte pe o linie. Problema determinării satisfiabilității unei formule LSAT este NP-completă.
2-satisfiabilitate
Problema SAT devine mai ușoară dacă numărul de literali din fiecare clauză este limitat la cel mult 2; în acest caz problema este numită . Această problemă poate fi rezolvată în timp polinomial și este, de fapt, completă pentru clasa de complexitate . Dacă în plus toate operațiile OR dintre literali sunt înlocuite cu operații XOR, rezultă problema numită exclusive-or 2-satisfiability, care este completă pentru clasa de complexitate = L.
Horn-satisfiabilitate
Problema determinării satisfiabilității unei conjuncții de se numește Horn-satisfiabilitate sau HORN-SAT. Aceasta poate fi rezolvată în timp polinomial printr-un pas al algoritmului de , care produce modelul minim al mulțimii de clauze Horn (în raport cu mulțimea literalilor evaluați ca TRUE). Problema Horn-SAT este . Ea poate fi considerată versiunea clasei P a problemei satisfiabilității booleene. De asemenea, determinarea valorii de adevăr a formulelor Horn cuantificate poate fi realizată în timp polinomial.
Clauzele Horn sunt de interes deoarece pot exprima implicația unei variabile dintr-un set de alte variabile. De exemplu, o clauză de forma
poate fi rescrisă ca
,
adică dacă sunt toate TRUE, atunci și trebuie să fie TRUE.
O generalizare a clasei formulelor Horn este clasa formulelor renameable-Horn, adică mulțimea formulelor care pot fi transformate într-o formulă Horn prin înlocuirea unor variabile cu negațiile lor. De exemplu,
nu este o formulă Horn, dar poate fi transformată într-o formulă Horn prin înlocuirea variabilei x3 cu negația sa. Verificarea existenței unei astfel de transformări se poate face în timp liniar; prin urmare satisfiabilitatea acestor formule aparține clasei P.
Probleme care nu sunt 3SAT
Forma normală disjunctivă SAT devine trivial dacă formulele sunt restrânse la cele aflate în , adică disjuncții de conjuncții de literali. O astfel de formulă este satisfiabilă dacă și numai dacă cel puțin una dintre conjuncțiile sale este satisfiabilă, iar o conjuncție este satisfiabilă dacă nu conține simultan x și ¬x pentru aceeași variabilă x. Această verificare poate fi realizată în timp liniar.
Dacă formulele sunt în forma normală disjunctivă completă, în care fiecare variabilă apare exact o dată în fiecare conjuncție, verificarea se poate face în timp constant (fiecare conjuncție reprezintă o atribuire satisfăcătoare). Totuși, transformarea unei formule SAT generale în formă normală disjunctivă poate necesita timp și spațiu exponențiale.
Exactly-1 3-satisfiability
O altă variantă NP-completă a problemei de 3-satisfiabilitate este one-in-three 3-SAT (numită și 1-in-3-SAT sau exactly-1 3-SAT). Dată fiind o formulă în formă normală conjunctivă cu trei literali pe clauză, problema constă în a determina dacă există o atribuire de valori de adevăr variabilelor astfel încât fiecare clauză să conțină exact un literal TRUE (și doi literali FALSE).
Not-all-equal 3-satisfiability
O altă variantă este problema not-all-equal 3-satisfiability (NAE3SAT). Dată fiind o formulă CNF cu trei literali pe clauză, se cere să se determine dacă există o atribuire a variabilelor astfel încât, în fiecare clauză, cei trei literali să nu aibă aceeași valoare de adevăr. Această problemă este de asemenea NP-completă.
XOR-satisfiability
Un alt caz particular este clasa de probleme în care fiecare clauză conține operatorul XOR în locul operatorului OR. Această problemă aparține clasei P, deoarece o formulă XOR-SAT poate fi interpretată ca un sistem de ecuații liniare modulo 2 și poate fi rezolvată în timp cubic prin eliminare gaussiană.
Teorema dicotomiei a lui Schaefer
Restricțiile de mai sus (CNF, 2CNF, 3CNF, Horn, XOR-SAT) impun ca formulele considerate să fie conjuncții de subformule; fiecare restricție specifică o anumită formă pentru toate subformulele. De exemplu, în 2CNF subformulele pot fi doar clauze binare.
Teorema dicotomiei a lui Schaefer afirmă că, pentru orice restricție asupra funcțiilor booleene care pot fi utilizate pentru a forma aceste subformule, problema corespunzătoare de satisfiabilitate este fie în clasa P, fie NP-completă. Faptul că satisfiabilitatea formulelor 2CNF, Horn și XOR-SAT aparține clasei P reprezintă cazuri particulare ale acestei teoreme.
Următorul tabel rezumă câteva variante comune ale problemei SAT.