¿Por qué los algoritmos para resolver 2-SAT en tiempo polinómico no pueden hacer lo mismo con 3-SAT?

El algoritmo de Krom (uno de los estándares) se basa en el hecho de que dos cláusulas [math] (x \ lor y) [/ math] y [math] (\ neg x \ lor z) [/ math] se pueden combinar para dar [ math] (y \ lor z) [/ math], que en sí es una disyunción de 2 literales. Paso a paso podemos eliminar variables hasta que tengamos un problema trivial (donde todas las variables aparecen como literales positivos o solo como literales negativos) o como una contradicción.

Si intentamos este mismo truco cuando tenemos 3 literales en cada parte, el resultado tendría 4 literales, no 3. Esto significa que el resultado tendría que transformarse en la forma adecuada para 3 sat, lo que dará como resultado varios cláusulas y / o nuevas variables que se introducen. En lugar de simplificar el resultado, es probable que sea al menos tan complejo o incluso más que el original.

Actualmente se desconoce si puede existir un algoritmo de tiempo polinómico para 3-SAT (este es el problema P vs NP).