El problema estándar 1-en-3 SAT (o XSAT o X3SAT) es:
Instancia : una fórmula CNF con cada cláusula que contiene exactamente 3 literales
Pregunta : ¿existe una asignación satisfactoria que establezca exactamente 1 literal por cláusula verdadera?
El problema es NP-completo y sigue siendo difícil incluso si no se produce una variable negada. Me pregunto si este problema se vuelve fácil o difícil si se requiere que cada variable ocurra al menos una vez de manera positiva y al menos una vez de manera negativa .
La reducción habitual de 3SAT que muestra que 1-en-3 SAT es difícil reemplaza una cláusula por cláusulas , , donde son frescas para cada cláusula. Por lo tanto, esta reducción no ayuda a responder mi pregunta. He tenido problemas para encontrar un dispositivo que muestre la dureza de esta variante, ya que si exactamente 1 literal en una cláusula es verdadero, entonces los 2 literales no simétricos son falsos. Si resulta fácil, pensar en términos de particiones del conjunto de cláusulas podría hacerlo, pero no puedo ver cómo.( ¬ x ∨ a ∨ b ) ( y ∨ b ∨ c ) ( ¬ z ∨ c ∨ d ) a , b , c , d
fuente
Respuestas:
En un comentario, OP expresó interés en una reducción que generó instancias con 3 variables distintas por cláusula. Aquí hay un enfoque simple:
La reducción es de 1 en 3 SAT con 3 variables distintas por cláusula:
Verifiquemos que esta reducción haga lo que queremos. Las siguientes propiedades son lo que queremos:
La propiedad 1 es trivial para verificar. La propiedad 2 también es fácil de verificar: las variables , y presentan de manera positiva y negativa en las cláusulas agregadas en el segundo punto, mientras que todas las demás variables en la fórmula se presentan de manera positiva y negativa en las cláusulas agregadas en Tercera viñeta.F1 F2 F3
En cuanto a la propiedad 3, esto es menos trivial pero aún así fácil. Puede argumentar fácilmente que la única asignación para las variables , y que satisface cada cláusula desde el segundo punto es hacer que las tres falsas. Pero luego, suponiendo un valor de falso para , las cláusulas y agregadas en el tercer punto se satisfacen si y solo si . Como no hay otras restricciones en , esto significa que siempre es posible extender una asignación satisfactoria para la fórmula de entrada en una asignación satisfactoria para la fórmula de salida: simplemente configure cadaF1 F2 F3 Fi F1 (x,x′,F1) (¬x,¬x′,F1) x′=¬x x′ x′ será la negación de la correspondiente y establecerá cada en falso.x Fi
fuente