Transforme un CNF en un 3-CNF equivalente definido en las mismas variables

8

(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: ).(x1x2x3x4)

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.FFFF

¿Cuál es la complejidad de este problema?

Xavier Labouze
fuente
Por equivalente se refiere a equi-satisfactoria, supongo.
Jan Johannsen
1
Más bien, "con el mismo conjunto de modelos".
Xavier Labouze
FYI tseitin transformar es el nombre para la transformación de -SAT a 3-SAT utilizando VARs adicionales. Parece que su pregunta es algo así como preguntar acerca de la existencia de un algoritmo de compresión para SAT. suena como si quisieras las mismas soluciones acortando las cláusulas a 3 o menos variables. de EE, esto se relaciona con enumerar todos los términos mínimos y encontrar coberturas mínimas y preguntar si existe alguno que cumpla con los criterios (en este caso, todas las cláusulas 3 o menos vars). parece tener una complejidad potencialmente alta. n
vzn
Tal vez sea co-NP-complete: elija una fórmula 3CNF , una nueva fórmula con 4 nuevas variables . tiene una fórmula equivalente a 3CNF en las mismas variables si y solo si no es satisfactoria. φ = ( y 1y 2y 3y 4 ) C 1. . . C n y 1 , . . . , y 4 φ φφ=C1...Cnφ=(y1y2y3y4)C1...Cny1,...,y4φφ
Marzio De Biasi
@MarzioDeBiasi. Agradable ! Sin embargo, no estoy seguro de que sea suficiente para demostrar la integridad de la co-NP (de alguna manera, espero una mayor competencia, pero es solo una intuición ...)
Xavier Labouze

Respuestas:

6

(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

φ=(y1y2y3y4)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 1y 2y 3 ) ( y 1y 2y 4 ) C 1. . . C m φ (y1y2y3)(y1y2y4)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φφφxix˙iφXφXyiφX=(y1y2y3y4). 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¬y2y3)φy1=false,y2=true,y3=false,y4=true,x˙1,...,x˙nφ

Marzio De Biasi
fuente
Gracias por la respuesta. No obtengo el : hubiera dicho que si es insatisfecha, también lo es , que es equivalente a la cláusula vacía (tamaño 0). Para ), solo pensar si , entonces es equivalente a ...()φφ(φ=(x¬x)(y1y2y3y4)(x¬x)(y1y2x)(y3y4¬x)
Xavier Labouze el
@XavierLabouze: sí, tu parece mejor. En ( supongo que hay un 3CNF equivalente , y luego deduzco una contradicción al suponer que la original es satisfactoria. ¿Crees que está mal? ())φφ
Marzio De Biasi
Tienes razón: me equivoqué al decir que tiene el mismo conjunto de modelos que . (y1y2y3y4)(x¬x)(y1y2x)(y3y4¬x)
Xavier Labouze
¿ que es igual a ? ¿Puede explicar esto: "Obtenemos que es satisfactoria si y solo si es satisfactoria", entonces está agregando "(ambos contienen solo variables )", ¿cómo puede estar seguro de que lo harán? solo contiene ? Además, no entiendo la conclusión, ¿probaste que agregar la cláusula 4 variables a 3-cnf desde las mismas variables es coNP-Complete? (y1y2y3)(y1y2y4)(y1y2)(y3y4)φXφXyiyi
Ilya Gazman
1
φ1=(y1y2y3)(y1y2y4) y son equisatisfactables pero no son equivalentes (iguales conjunto de modelos): y1 = F, y2 = F, y3 = T, y4 = T es un modelo válido para pero no para . En la pregunta estamos hablando de fórmulas equivalentes. La prueba se basa en el hecho de que no puede tener el mismo conjunto de modelos de ninguna fórmula 3CNF. φ2=(y1y2)(y3y4)φ1φ2(y1y2y3y4)
Marzio De Biasi