Teorema de Cook-Levin o teorema de Cook

En la teoría de la complejidad computacional, el teorema de Cook-Levin, también conocido como teorema de Cook, establece que el problema de satisfacibilidad booleano es NP-completo. Es decir, está en NP, y cualquier problema en NP puede reducirse en tiempo polinomial mediante una máquina de Turing determinista al problema booleano de satisfacibilidad.

Stephen Arthur Cook y LA Levin en 1973 demostraron de forma independiente que el problema de satisfacibilidad (SAT) es NP-completo. Stephen Cook, en 1971, publicó un importante artículo titulado ‘La complejidad de los procedimientos de prueba de teoremas’, en el que describía la forma de obtener la prueba de un problema NP-completo reduciéndolo a SAT . Demostró que los problemas de Circuit-SAT y 3CNF-SAT son tan difíciles como SAT . De manera similar, Leonid Levin trabajó de forma independiente en este problema en la entonces Unión Soviética. La prueba de que SAT es NP-completo se obtuvo gracias a los esfuerzos de estos dos científicos. Más tarde, Karp redujo 21 problemas de optimización, como el recorrido hamiltoniano, la cobertura de vértices ,y clique, al SAT y demostró que esos problemas son NP-completos.

Por lo tanto, un SAT es un problema significativo y puede enunciarse de la siguiente manera:

Dada una expresión booleana F que tiene n variables x ₁ ,x ₂ ,….,x _n , y operadores booleanos, ¿es posible tener una asignación de variables verdadera o falsa tal que la expresión binaria F sea verdadera?

Este problema también se conoce como la fórmula – SAT . Un SAT (fórmula-SAT o simplemente SAT) toma una expresión booleana F y verifica si la expresión (o fórmula) dada es satisfactoria. Se dice que una expresión booleana es satisfactoria para algunas asignaciones válidas de variables si la evaluación llega a ser verdadera. Antes de discutir los detalles de SAT, analicemos ahora algunas terminologías importantes de una expresión booleana.

• Variable booleana: una variable, digamos x , que solo puede tener dos valores, verdadero o falso, se denomina variable booleana.
• Literal: Un literal puede ser una variable lógica, digamos x , o la negación de la misma, es decir x o x̄ ; x se llama literal positivo, y x̄ se llama literal negativo
• Cláusula: Una secuencia de variables (x ₁ ,x ₂ ,….,x _n ) que se pueden separar mediante unoperador lógico OR se denomina cláusula. Por ejemplo, (x ₁ V x ₂ V x ₃ ) es una cláusula de tres literales.
• Expresiones: se pueden combinar todas las cláusulas anteriores utilizando un operador booleano para formar una expresión.
• Forma CNF: una expresión está en forma CNF (forma normal conjuntiva) si el conjunto de cláusulas está separado por un operador AND (^) , mientras que los literales están conectados por un operador OR (v) . El siguiente es un ejemplo de una expresión en la forma CNF:
  • f = (x ₁ V x̄ ₂ V x ₃₎ ∧ (x ₁ V x̄ ₃ V x ₂ )
• 3 – CNF: Se dice que una expresión está en 3-CNF si está en la forma conjuntiva normal, y cada cláusula tiene tres literales exactos.

Por lo tanto, un SAT es uno de los problemas más difíciles, ya que no existe un algoritmo conocido que no sea el enfoque de fuerza bruta. Un algoritmo de fuerza bruta sería un algoritmo de tiempo exponencial, ya que se deben intentar 2 ^{n asignaciones posibles para verificar si la expresión booleana dada es verdadera o no.} Stephen Cook y Leonid Levin demostraron que el SAT es NP-completo.

Cook demostró la reducción de otros problemas difíciles a los SAT. Karp proporcionó pruebas de 21 problemas importantes, como el recorrido hamiltoniano, la cobertura de vértices y la camarilla, reduciéndolos a SAT mediante la reducción de Karp.

 Presentemos brevemente los tres tipos de SAT. Son los siguientes:

1. Circuito- SAT: Un circuito-SAT se puede establecer de la siguiente manera: dado un circuito booleano, que es una colección de puertas como AND , OR y NOT , y n entradas, ¿existe alguna asignación de entrada de variables booleanas para que la salida del circuito dado es cierto? Nuevamente, la dificultad con estos problemas es que para n entradas al circuito. Se deben comprobar 2 ^{n salidas posibles.} Por lo tanto, este algoritmo de fuerza bruta es un algoritmo exponencial y, por lo tanto, este es un problema difícil.
2. CNF-SAT: Este problema es un problema restringido de SAT , donde la expresión debe estar en forma normal conjuntiva. Se dice que una expresión está en forma de conjunción si todas las cláusulas están conectadas por eloperador booleano AND . Como en el caso de un SAT , se trata de asignar valores de verdad a n variables de modo que la salida de la expresión sea verdadera .
3. 3-CNF-SAT(3-SAT): Este problema es otra variante donde la restricción adicional es que la expresión está en forma conjuntiva normal y que cada cláusula debe contener exactamente tres literales. Este problema también se trata de asignar n asignaciones de valores de verdad a n variables de la expresión booleana de modo que la salida de la expresión sea verdadera. En palabras simples, dada una expresión en 3-CNF, un problema de 3-SAT consiste en verificar si la expresión dada es satisfactoria.

Estos problemas se pueden usar para probar la completitud NP de algunos problemas importantes.