¿Por qué Hornsat, 3sat y 2sat no son equivalentes?

Question

He estado leyendo un poco sobre la teoría de la complejidad recientemente, y me he encontrado con un pequeño obstáculo. El problema de satisfactibilidad de Horn es resoluble en tiempo lineal, pero el problema de satisfactibilidad booleana en general es NP-Difícil. Hasta aquí todo bien, entiendo eso.

Al parecer, la satisfactibilidad booleana es reducible a la satisfactibilidad de una expresión booleana en forma normal conjuntiva con 3 variables por cláusula. Sin embargo, este problema también es NP-Difícil. Eso también está bien para mí, ya que fue demostrado por alguien probablemente mucho más inteligente que yo.

Sin embargo, tengo problemas debido a la siguiente tautología:

$$(a \vee b \vee c) \iff ((\neg a \wedge \neg b)\implies c)$$

No es exactamente una cláusula de Horn, pero aún no he terminado.

Entonces, dado un problema 3SAT, aplicamos la tautología anterior.

Luego reemplazamos cada booleano negado $\neg x$ con una nueva variable $x_n$

Esta es una instancia de HORNSAT, pero desafortunadamente no es equivalente al problema original. Sin embargo, este nuevo problema es polinomialmente equivalente a una cierta instancia de 2SAT (satisfactible si el HORNSAT lo es). Ahora, si por cada variable introducida $x_n$, agregamos lo siguiente a nuestro problema 2SAT: $$ (x \vee x_n)\wedge (\neg x \vee \neg x_n) $$

Entonces, ¿no debería esta instancia 2SAT ser equivalente al problema original de 3SAT? El número de variables se duplicó y tiene un factor lineal más de cláusulas.

Debo estar pasando por alto algo, ¿verdad? No logro ver el error por más que lo intento. ¿Alguien puede explicármelo?

EDIT: y un contraejemplo sería apreciado.

Answer 1

Lo que necesitarías es una traducción entre HORNSAT y 2SAT que te permita traducir un testigo para la satisfacibilidad de la fórmula Horn en un testigo para el 2SAT (¿o viceversa? Pero esto realmente no importa). En cualquier caso, una forma barata de reducir HORNSAT a 2SAT es resolver tu instancia de HORNSAT en tiempo polinómico, es decir, verificar la satisfacibilidad, y luego devolver una instancia trivialmente satisfacible de 2SAT o una instancia trivialmente no satisfactible de 2SAT. En otras palabras, desechas toda la información sobre la fórmula Horn, excepto si es satisfacible o no. En particular, los términos que describen el papel de las nuevas variables que agregas no tienen significado en relación con la instancia de 2SAT que obtienes a partir de la fórmula Horn.