Problema de satisfacibilidad booleana

En teoría de la complejidad computacional, el Problema de satisfacibilidad booleana (también llamado SAT) fue el primer problema identificado como perteneciente a la clase de complejidad NP-completo.

Historia

Su NP-completitud fue demostrada por Stephen Cook en 1971 (el Teorema de Cook).[1]​ Hasta entonces el concepto de problema NP-completo no había sido definido. El SAT sigue siendo NP-completo incluso si todas las fórmulas están en forma normal conjuntiva (FNC) con 3 variables por cláusula (3SAT-FNC) creando el problema (3SAT), o aun en el caso de que solo se permita un único valor verdadero en cada cláusula (3SAT en 1) Cláusula de Horn.

En 1960 Martin Davis y Hilary Putnam desarrollaron un algoritmo para comprobar la satisfactibilidad de las fórmulas de la lógica proposicional en FNC; es decir, en un conjunto de cláusulas unidas por conjunciones. El algoritmo usa una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula donde la variable aparezca afirmada con una cláusula en la que la variable esté negada. En 1962 se desarrolló el algoritmo DPLL por Davis-Putnam-Logemann-Lovelandes, un algoritmo completo basado en la vuelta atrás (backtracking) que sirve para decidir la satisfacibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva; es decir, para resolver el problema FNC-SAT, al igual que hacía el algoritmo anterior de Davis y Putnam.

Other Languages