En ciencias de la computación , el Problema de Satisfacción de Sharp (a veces llamado Sharp-SAT o #SAT ) es el problema de contar el número de interpretaciones que satisfacen una fórmula booleana dada , introducida por Valiant en 1979. [1] En otras palabras, pregunta en de cuántas formas las variables de una fórmula booleana dada pueden ser reemplazadas consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula se evalúe como VERDADERA . Por ejemplo, la fórmula es satisfactorio mediante tres asignaciones de valor booleano distintas de las variables, es decir, para cualquiera de las asignaciones ( = VERDADERO, = FALSO), ( = FALSO, = FALSO),
( = VERDADERO, = VERDADERO), tenemos = VERDADERO.
#SAT es diferente del problema de satisfacibilidad booleano (SAT), que pregunta si existe una solución de fórmula booleana. En cambio, #SAT solicita enumerar todas las soluciones a una fórmula booleana. #SAT es más difícil que SAT en el sentido de que, una vez que se conoce el número total de soluciones de una fórmula booleana, SAT puede decidirse en tiempo constante. Sin embargo, lo contrario no es cierto, porque saber que una fórmula booleana tiene una solución no nos ayuda a contar todas las soluciones , ya que hay un número exponencial de posibilidades.
#SAT es un ejemplo bien conocido de la clase de problemas de conteo , conocido como # P-completo (leído como P sostenido completo). En otras palabras, cada instancia de un problema en la clase de complejidad #P puede reducirse a una instancia del problema #SAT. Este es un resultado importante porque surgen muchos problemas de conteo difíciles en Combinatoria Enumerativa , Física estadística , Confiabilidad de red e Inteligencia artificial sin ninguna fórmula conocida. Si se demuestra que un problema es difícil, entonces proporciona una explicación teórica de la complejidad de la falta de fórmulas atractivas. [2]
# P-Completitud
#SAT es # P-completo . Para probar esto, primero tenga en cuenta que #SAT está obviamente en #P.
A continuación, probamos que #SAT es # P-hard. Tome cualquier problema #A en #P. Sabemos que A se puede resolver usando una máquina de Turing no determinista M. Por otro lado, a partir de la demostración del teorema de Cook-Levin , sabemos que podemos reducir M a una fórmula booleana F. Ahora, cada asignación válida de F corresponde a una ruta única aceptable en M, y viceversa. Sin embargo, cada camino aceptable tomado por M representa una solución a A. En otras palabras, hay una biyección entre las asignaciones válidas de F y las soluciones a A. Entonces, la reducción usada en la demostración del Teorema de Cook-Levin es parsimoniosa. Esto implica que #SAT es # P-hard.
Casos especiales intratables
El conteo de soluciones es intratable (# P-completo) en muchos casos especiales para los que la satisfacibilidad es manejable (en P), así como cuando la satisfacibilidad es intratable (NP-completo). Esto incluye lo siguiente.
# 3SAT
Esta es la versión de conteo de 3SAT . Se puede demostrar que cualquier fórmula en SAT se puede reescribir como una fórmula en forma 3- CNF preservando el número de asignaciones satisfactorias. Por lo tanto, #SAT y # 3SAT cuentan como equivalentes y # 3SAT también es # P-complete.
# 2SAT
Aunque 2SAT (decidir si una fórmula 2CNF tiene una solución) es polinomio, contar el número de soluciones es # P-completo.
# Cuerno-SAT
De manera similar, aunque la satisfacibilidad de Horn es polinomial, contar el número de soluciones es # P-completo. Este resultado se deriva de una dicotomía general que caracteriza qué problemas similares al SAT son # P-completo. [3]
Planar # 3SAT
Esta es la versión de conteo de Planar 3SAT . La reducción de dureza de 3SAT a Planar 3SAT dada por Lichtenstein [4] es parsimoniosa. Esto implica que Planar # 3SAT es # P-completo.
Planar Monótono Rectilíneo # 3SAT
Esta es la versión de conteo de Planar Monotone Rectilinear 3SAT. [5] La reducción de la dureza NP dada por de Berg & Khosravi [5] es parsimoniosa. Por lo tanto, este problema también es # P-complete.
Estuches especiales tratables
Modelo de conteo es tratable (resolubles en tiempo polinómico) para (ordenadas) BDDs y para D-DNNFs.
Software
sharpSAT es un software para resolver casos prácticos del problema #SAT. "sharpSAT - Marc Thurley" . sites.google.com . Consultado el 30 de abril de 2019 .
Referencias
- ^ Valiente, LG (1979). "La complejidad de cálculo de la permanente". Informática Teórica . 8 (2): 189-201. doi : 10.1016 / 0304-3975 (79) 90044-6 .
- ^ Vadhan, Salil Vadhan (20 de noviembre de 2018). "Lección 24: Problemas de conteo" (PDF) .
- ^ Creignou, Nadia; Hermann, Miki (1996). "Complejidad de problemas de conteo de satisfacción generalizada". Información y Computación . 125 : 1-12. doi : 10.1006 / inco.1996.0016 . hdl : 10068/41883 .
- ^ Lichtenstein, David (1982). "Fórmulas planas y sus usos". Revista SIAM de Computación . 11: 2 : 329–343.
- ^ a b Khosravi, Amirali; Berg, Mark de (2010). "Particiones óptimas del espacio binario en el plano" . indefinido . Consultado el 1 de mayo de 2019 .