Problema de satisfacibilidad booleana

En teoria de la complexitat computacional, el Problema de satisfacibilidad booleana (també cridat SAT) va ser el primer problema identificat com a pertanyent a la classe de complexitat NP-complet.

Història

La seua NP-completitud va ser demostrada per Stephen Cook en 1971 (el Teorema de Cook). Fins a llavors el concepte de problema NP-complet no havia segut definit. El SAT seguix sent NP-complet inclús si totes les fòrmules estan en forma normal conjuntiva (FNC) en 3 variables per clàusula (3SAT-FNC) creant el problema (3SAT), o encara en el cas de que solament es permeta un únic valor verdader en cada clàusula (3SAT en 1).

En 1960 Martin Davis i Hilary Putnam varen desenrollar un algoritme per a comprovar la satisfacibilidad de les fòrmules de la llògica proposicional en FNC; és dir, en un conjunt de clàusules unides per conjuncions. L'algoritme usa una forma de resolució en la qual les variables són elegides iterativamente i eliminades per mig de la resolució de cada clàusula a on la variable aparega afirmada en una clàusula en la que la variable estiga negada. En 1962 es va desenrollar l'algoritme DPLL per Davis-Putnam-Logemann-Lovelandes, un algoritme complet basat en la regrés arrere (backtracking) que servix per a decidir la satisfacibilidad de les fòrmules de llògica proposicional en una forma normal conjuntiva; és dir, per a resoldre el problema FNC-SAT, de la mateixa manera que feya l'algoritme anterior de Davis i Putnam.

Plantejament

El problema SAT és el problema de saber si, donada una expressió booleana en variables i sense quantificadors, hi ha alguna assignació de valors per a les seues variables que fa que l'expressió siga verdadera. Un eixemple de SAT seria el saber si existixen valors per a $x_1,x_2,x_3,x_4$ tals que l'expressió:

$(x_1\vee \mathrm{\neg }{x}_3)\wedge (\mathrm{\neg }{x}_2\vee x_3\vee \mathrm{\neg }{x}_4)$

siga certa.

Pel contrari, el problema de si l'expressió en qüestió adquirix valor fals per a totes les combinacions de les seues variables, es denomina UNSAT.

Vore també

• Algoritmes SAT