Satélite Sharp

En informática , el problema de satisfacibilidad de Sharp (a veces llamado Sharp-SAT , #SAT o conteo de modelos ) es el problema de contar el número de interpretaciones que satisfacen una fórmula booleana dada , introducido por Valiant en 1979. ^[1] En otras palabras, pregunta de cuántas maneras las variables de una fórmula booleana dada pueden reemplazarse consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula evalúe VERDADERO . Por ejemplo, la fórmula es satisfacible por tres asignaciones de valores booleanos distintas de las variables, a saber, para cualquiera de las asignaciones ( = VERDADERO, = FALSO), ( = FALSO, = FALSO) y ( = VERDADERO, = VERDADERO), tenemos${\displaystyle a\lor \neg b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a\lor \neg b={\textsf {TRUE}}.}$

#SAT es diferente del problema de satisfacibilidad booleana (SAT), que pregunta si existe una solución de la fórmula booleana. En cambio, #SAT pide enumerar todas las soluciones de 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 se puede decidir en tiempo constante. Sin embargo, lo inverso 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 , conocidos como #P-completos (léase como P completo agudo). En otras palabras, cada instancia de un problema en la clase de complejidad #P se puede reducir a una instancia del problema #SAT. Este es un resultado importante porque muchos problemas de conteo difíciles surgen en Combinatoria Enumerativa , Física Estadística , Confiabilidad de Redes 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 para la falta de fórmulas atractivas. ^[2]

#SAT es #P-completo . Para demostrarlo, primero observe que #SAT obviamente está en #P.

A continuación, demostramos que #SAT es #P-hard. Tomemos cualquier problema #A en #P. Sabemos que A se puede resolver utilizando una máquina de Turing no determinista M. Por otro lado, a partir de la prueba 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 un camino aceptable único en M, y viceversa. Sin embargo, cada camino aceptable tomado por M representa una solución para A. En otras palabras, hay una biyección entre las asignaciones válidas de F y las soluciones para A. Por lo tanto, la reducción utilizada en la prueba del teorema de Cook-Levin es parsimoniosa. Esto implica que #SAT es #P-hard.

El conteo de soluciones es intratable (#P-completo) en muchos casos especiales para los cuales la satisfacibilidad es intratable (en P), así como cuando la satisfacibilidad es intratable (NP-completo). Esto incluye lo siguiente.

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 de 3- CNF conservando la cantidad de asignaciones satisfactorias. Por lo tanto, #SAT y #3SAT son equivalentes en cuanto al conteo y #3SAT también es #P-completo.

Aunque 2SAT (decidir si una fórmula 2CNF tiene una solución) es polinomial, contar el número de soluciones es #P -completo. ^[3] La #P-completitud ya está en el caso monótono, es decir, cuando no hay negaciones (#MONOTONE-2-CNF).

Se sabe que, asumiendo que NP es diferente de RP , #MONOTONE-2-CNF tampoco puede aproximarse mediante un esquema de aproximación de tiempo completamente polinomial (FPRAS), incluso asumiendo que cada variable ocurre en como máximo 6 cláusulas, pero que existe un esquema de aproximación de tiempo completamente polinomial (FPTAS) cuando cada variable ocurre en como máximo 5 cláusulas: ^[4] esto se desprende de resultados análogos en el problema ♯IS de contar el número de conjuntos independientes en gráficos .

De manera similar, aunque la satisfacibilidad de Horn es polinómica, contar el número de soluciones es #P-completo. Este resultado se desprende de una dicotomía general que caracteriza qué problemas similares a SAT son #P-completos. ^[5]

Esta es la versión de conteo de Planar 3SAT. La reducción de dureza de 3SAT a Planar 3SAT dada por Lichtenstein ^[6] es parsimoniosa. Esto implica que Planar #3SAT es #P-completo.

Esta es la versión de conteo de Planar Monotone Rectilinear 3SAT. ^[7] La ​​reducción de dureza NP dada por de Berg y Khosravi ^[7] es parsimoniosa. Por lo tanto, este problema también es #P-completo.

En el caso de las fórmulas en forma normal disyuntiva (DNF), contar las soluciones también es #P-completo, incluso cuando todas las cláusulas tienen un tamaño de 2 y no hay negaciones : esto se debe a que, según las leyes de De Morgan , contar el número de soluciones de una DNF equivale a contar el número de soluciones de la negación de una fórmula en forma normal conjuntiva (CNF). La intratabilidad se mantiene incluso en el caso conocido como #PP2DNF, donde las variables se dividen en dos conjuntos, y cada cláusula contiene una variable de cada conjunto. ^[8]

Por el contrario, es posible aproximar de manera manejable el número de soluciones de una fórmula de forma normal disyuntiva utilizando el algoritmo Karp-Luby, que es un FPRAS para este problema. ^[9]

La variante de SAT correspondiente a relaciones afines en el sentido del teorema de dicotomía de Schaefer , es decir, donde las cláusulas equivalen a ecuaciones módulo 2 con el operador XOR , es la única variante de SAT para la cual el problema #SAT se puede resolver en tiempo polinomial. ^[10]

Si las instancias de SAT se restringen mediante parámetros de gráfico , el problema #SAT puede volverse manejable. Por ejemplo, #SAT en instancias SAT cuyo ancho de árbol está limitado por una constante se puede realizar en tiempo polinomial . ^[11] Aquí, el ancho de árbol puede ser el ancho de árbol primario, el ancho de árbol dual o el ancho de árbol de incidencia del hipergrafo asociado a la fórmula SAT, cuyos vértices son las variables y donde cada cláusula se representa como una hiperarista.

El conteo de modelos es manejable (resoluble en tiempo polinomial) para BDD (ordenados) y para algunos formalismos de circuitos estudiados en la compilación de conocimiento , como d-DNNF.

El conteo de modelos ponderados (WMC) generaliza #SAT al calcular una combinación lineal de los modelos en lugar de simplemente contar los modelos. En la variante ponderada de WMC, a cada literal se le asigna un peso, de modo que . ${\displaystyle {\text{WMC}}(\phi ;w)=\sum _{M\models \phi }\prod _{l\in M}w(l)}$

WMC se utiliza para inferencia probabilística, ya que las consultas probabilísticas sobre variables aleatorias discretas, como en redes bayesianas, se pueden reducir a WMC. ^[12]

El conteo de modelos algebraicos generaliza aún más #SAT y WMC sobre semianillos conmutativos arbitrarios . ^[13]