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 un problema NP-completo, no estaba 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 aún inclusive, en el caso en que solo se permita un solo valor verdadero en cada cláusula (3SAT en 1) Cláusula de Horn.

En 1960 Martin Davis y Hilary Putnam desarrollan un algoritmo para comprobar la satisfacibilidad de las fórmulas de la lógica proposicional en FNC, es decir en un conjunto de cláusulas unidas por conjunciones. Esto es una forma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que la variable aparece afirmada con una cláusula en la que la variable es negada, en 1962 se desarrolla el algoritmo DPLL por Davis-Putnam-Logemann-Lovelandes, un algoritmo completo basado en la vuelta atrás 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 el algoritmo anterior.

Other Languages