(Publiqué esta pregunta en CS hace diez días, sin respuesta desde entonces, así que la publico aquí).
Cualquier fórmula CNF se puede transformar en tiempo polinómico en una fórmula 3-CNF mediante el uso de nuevas variables. No siempre es posible si no se permiten nuevas variables (tome por ejemplo la fórmula de la cláusula única: ).
Definamos el problema (SAT a 3-SAT): dada , una fórmula CNF. ¿Es posible transformar en un 3-CNF equivalente definido en las mismas variables que ? - donde "equivalente" significa con el mismo conjunto de modelos.F
¿Cuál es la complejidad de este problema?
cc.complexity-theory
complexity-classes
sat
Xavier Labouze
fuente
fuente
Respuestas:
(Del comentario anterior) El problema parece difícil de resolver; la reducción simple es de 3CNF-UNSAT (que es coNP-complete): dada una fórmula 3CNF , agregando una nueva cláusula con 4 nuevas variables:φ=C1∧...∧Cm
φφ′ tiene una fórmula 3CNF equivalente definida en las mismas variables si y solo si la fórmula original no es satisfactoria.φ
( ) la fórmula 3CNF es equivalente a( y 1 ∨ y 2 ∨ y 3 ) ∧ ( y 1 ∨ y 2 ∨ y 4 ) ∧ C 1 ∧ . . . ∧ C m φ ′⇐ (y1∨y2∨y3)∧(y1∨y2∨y4)∧C1∧...∧Cm φ′
( ) suponga que tiene una fórmula 3CNF equivalente y que es satisfactoria. Elija una tarea satisfactoria of , y simplifique tanto como reemplazando las variables con la verdad correspondiente valores . Obtenemos que es satisfactoria si y solo si es satisfactoria (ambos contienen solo variables ). Claramente⇒ φ′ φ′′ φ X=⟨x˙1,...,x˙n⟩ φ φ′ φ′′ xi x˙i φ′X φ′′X yi φ′X=(y1∨y2∨y3∨y4) . Cada cláusula de contiene como máximo tres variables, por lo que podemos elegir una de ellas, por ejemplo , y usarla para crear una asignación satisfactoria para :
que no es una asignación satisfactoria para , lo que lleva a contradicción.φ′′X (y1∨¬y2∨y3) φ′ ⟨y1=false,y2=true,y3=false,y4=true,x˙1,...,x˙n⟩ φ′′
fuente