1 de cada 3 SAT

En complejidad computacional , el problema 3-SAT de uno en tres (también conocido como SAT de uno en tres y SAT exactamente uno ) es una variante NP-completa del problema de satisfacibilidad booleana .

Dada una forma normal conjuntiva con tres literales por cláusula, el problema consiste en determinar si existe una asignación de verdad a las variables tal que cada cláusula tenga exactamente un literal VERDADERO (y, por lo tanto, exactamente dos literales FALSO). En contraste, el 3-SAT ordinario requiere que cada cláusula tenga al menos un literal VERDADERO. Formalmente, un problema 3-SAT de uno en tres se da como una forma normal conjuntiva generalizada con todas las cláusulas generalizadas que utilizan un operador ternario R que es VERDADERO si y solo si exactamente uno de sus argumentos lo es. Cuando todas las variables de una fórmula 3-SAT de uno en tres tienen el mismo literal, el problema de satisfacibilidad se llama 3-SAT monótono de uno en tres .

El problema 3-SAT de uno en tres, junto con su caso monótono, figura como problema NP-completo "LO4" en la obra de referencia estándar Computers and Intractability: A Guide to the Theory of NP-Completeness de Michael R. Garey y David S. Johnson . Thomas Jerome Schaefer demostró que el problema 3-SAT de uno en tres es NP-completo como un caso especial del teorema de dicotomía de Schaefer , que afirma que cualquier problema que generalice la satisfacibilidad booleana de cierta manera pertenece a la clase P o es NP-completo. ^{[ 1 ]}

Aquí hay una instancia SAT 1 de 3 que se puede satisfacer, con 3 variables y 1 cláusula:

R(¬ a , b , c )  

Esta instancia admite 3 soluciones:

• a=falso, b=falso, c=falso
• a=verdadero, b=verdadero, c=falso
• a=verdadero, b=falso, c=verdadero

Aquí tenemos una instancia única de SAT 1 en 3, es decir, una instancia de SAT 1 en 3 que admite exactamente una solución:

R( a , b , c ) ∧ R( g , h , i ) ∧ R( a , d , h ) ∧ R( b , d , g ) ∧ R( b , e , h ) ∧ R( c , f , i )                      

La solución única es a=verdadero, b=falso, c=falso, d=falso, e=verdadero, f=verdadero, g=verdadero, h=falso, i=falso

Y aquí tenemos un ejemplo insatisfacible de 1 de cada 3 casos de SAT:

R(x ₁ , x ₂ , x ₃ )  ∧  R(x ₅ , x ₆ , x ₇ )  ∧  R(x ₁ , x ₄ , x ₇ )  ∧  R(x ₂ , x ₄ , x ₆ )  ∧  R(x ₃ , x ₄ , x ₅ )

Schaefer proporciona una construcción que permite una fácil reducción en tiempo polinomial de 3-SAT a 3-SAT uno en tres. Sea "( x o y o z )" una cláusula en una fórmula 3CNF. Añada seis nuevas variables booleanas a , b , c , d , e , y f , que se utilizarán para simular esta cláusula y ninguna otra. Entonces, la fórmula R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e ) ∧ R ( c , d , f ) ∧ R ( z , c ,FALSE) es satisfacible por alguna configuración de las nuevas variables si y solo si al menos una de x , y , o z es VERDADERA, véase la tabla (abajo). Por lo tanto, cualquier instancia 3-SAT con m cláusulas y n variables puede convertirse en una instancia 3-SAT equisatisfacible de uno en tres con 5 m cláusulas y n + 6 m variables. ^{[ 2 ]}

El resultado de R es VERDADERO (1) si exactamente uno de sus argumentos es VERDADERO, y FALSO (0) en caso contrario. Se examinan las 8 combinaciones de valores para x , y , z , una por línea. Las nuevas variables a , ..., f se pueden elegir para satisfacer todas las cláusulas (exactamente un argumento verde para cada R ) en todas las líneas excepto la primera, donde x ∨ y ∨ z es FALSO.

Otra reducción implica solo cuatro variables nuevas y tres cláusulas: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R( c , d ,¬ z ), ver tabla (abajo). Esta no es una reducción parsimoniosa . Cuando x=1 , y=0 y z=1 , se puede tener a=1 , b=0 , c=1 y d=0 , pero también se puede tener a=0 , b=1 , c=0 y d=1 .

La fórmula 3-SAT positiva de uno en tres es un caso específico donde todos los literales de la fórmula son positivos. La fórmula 1-en-3-SAT positiva es NP-completa. Una fórmula 1-en-3-SAT se puede reducir en tiempo polinomial a una fórmula 1-en-3-SAT positiva introduciendo variables ocultas que son el negativo de las variables que aparecen con un literal negativo. Luego, se deben agregar algunas cláusulas para forzar que esas nuevas variables sean negativas:

R(a  ∨  b  ∨  ¬c) => R(a  ∨  b  ∨  c')  ∧  R(c  ∨  c'  ∨  alwaysZero)  ∧  R(c  ∨  c'  ∨  alwaysZeroToo)  ∧  R(alwaysZero  ∨  alwaysZeroToo  ∨  alwaysOne)

c' es una nueva variable que siempre es el negativo de c , y las nuevas variables alwaysZero , alwaysZeroToo y alwaysOne son constantes y pueden reutilizarse para las reducciones de las demás cláusulas. Para una fórmula de n variables y m cláusulas, la fórmula reducida tiene como máximo 2n + 3 variables y 7m + 1 cláusulas, pero puede ser menor si permitimos constantes o la misma variable dos veces en una cláusula.

Algunas reglas permiten reducir el tamaño de una instancia en tiempo polinomial. ^{[ a ]} ​​Al igual que otros problemas NP-completos, si un grupo de variables no comparte ninguna cláusula con el grupo restante de variables, entonces los dos grupos representan dos instancias SAT 1 en 3 distintas que pueden calcularse independientemente. Las soluciones de la instancia original son el producto cartesiano de las soluciones de las dos instancias y la instancia original es irresoluble si al menos una subinstancia es irresoluble.

El análisis local puede simplificar una instancia:

• Una cláusula que incluya la constante 1 se puede eliminar de forma segura y los literales restantes de la cláusula se establecen en 0 .
• Una cláusula que incluya dos veces la constante 0 se puede eliminar de forma segura y el literal restante de la cláusula se establece en 1 .
• Una cláusula que incluya una constante 0 puede eliminarse sin problemas y un literal de la cláusula puede reemplazarse por el opuesto del tercer literal de la cláusula.
• Una cláusula que incluya dos veces el mismo literal se puede eliminar sin problemas, el literal se establece en 0 y el tercer literal en 1 .
• Una cláusula que incluye un literal y su opuesto se puede eliminar de forma segura y el tercer literal se establece en 0 .

Algunas reglas implican dos cláusulas:

• Cuando dos cláusulas comparten dos variables iguales con los mismos literales, solo se conserva una cláusula y los terceros literales en ambas cláusulas son iguales, por lo que una se reemplaza por la otra en toda la instancia.
• Cuando dos cláusulas comparten dos variables iguales con literales opuestos, podemos eliminar de forma segura ambas cláusulas, reemplazar una variable por la opuesta de la otra y establecer el tercer literal en ambas cláusulas a 0 .
• Cuando dos cláusulas comparten dos variables iguales con un literal opuesto y otro igual, podemos eliminar sin problema ambas cláusulas, establecer la variable con el mismo literal en 0 y el tercer literal puede ser reemplazado por el opuesto de la variable con el literal opuesto.

La siguiente regla es un patrón que implica cuatro cláusulas:

R( x ₁  ∨ y ₁ ∨ z ₁ ) ∧    

R( x ₁  ∨ y ₂ ∨ z ₂ ) ∧    

R( x ₂  ∨ y ₁ ∨ z ₃ ) ∧    

R( x ₂  ∨ y ₂ ∨ z ₁ )   

En la primera posición (en el mundo real, puede ser en cualquier posición), dos literales aparecen dos veces; en la segunda posición, dos literales aparecen dos veces; y en la tercera posición, un literal aparece dos veces, pero ninguna cláusula comparte dos literales idénticos. Se puede simplificar de esta manera:

R( x ₁  ∨ y ₁ ∨ z ₁ )   

x ₁  =  x ₂

y ₁  =  y ₂

z ₁  =  z ₂ =  z ₃

La siguiente regla es un patrón que implica un número dinámico de cláusulas:

R( x ₁  ∨ y ₁ ∨ z ₁ ) ∧    

R( x ₂  ∨ y ₁ ∨ z ₂ ) ∧    

R( x ₂  ∨ y ₂ ∨ z ₁ ) ∧    

R( x ₃  ∨ y ₃ ∨ z ₂ ) ∧    

R( x ₃  ∨ y ₂ ∨ z ₃ ) ∧    

...

R( x _n-1  ∨ y _n-1 ∨ z _n-2 ) ∧    

R( x _n-1  ∨ y _n-2 ∨ z _n-1 ) ∧    

R( x _n  ∨ y _n-1 ∨ z _n-1 )   

Podemos reemplazar x _n por x ₁ .

Prueba

• Si x ₁ =0, entonces y ₁ =1 o z ₁ =1 entonces x ₂ =0 entonces y ₂ =1 o z ₂ =1 entonces x ₃ =0 entonces y ₃ =1 o z ₃ =1 ... entonces x _n−1 =0 entonces y _n−1 =1 o z _n−1 =1 entonces x _n =0
• Si x ₁ =1, entonces y ₁ =z ₁ =0 entonces y ₂ =z ₂ entonces y ₃ =z ₃ ... entonces y _n−1 =z _n−1 entonces y _n−1 =z _n−1 =0 y x _n =1

• Problema de satisfacibilidad booleana