En informática teórica , el problema de satisfacibilidad de circuito (también conocido como CIRCUIT-SAT , CircuitSAT , CSAT , etc.) es el problema de decisión de determinar si un circuito booleano determinado tiene una asignación de sus entradas que hace que la salida sea verdadera. [1] En otras palabras, pregunta si las entradas a un circuito booleano determinado se pueden establecer consistentemente en 1 o 0 de manera que el circuito genere 1 . Si ese es el caso, el circuito se llama satisfactible . De lo contrario, el circuito se llama insatisfactorio. En la figura de la derecha, el circuito izquierdo se puede satisfacer configurando ambas entradas en 1 , pero el circuito derecho no es satisfactorio.
CircuitSAT está estrechamente relacionado con el problema de satisfacibilidad booleana (SAT) y, además, se ha demostrado que es NP completo . [2] Es un problema prototípico de NP-completo; El teorema de Cook-Levin a veces se demuestra en CircuitSAT en lugar de en el SAT, y luego CircuitSAT se puede reducir a otros problemas de satisfacibilidad para demostrar su integridad NP. [1] [3] La satisfacibilidad de un circuito que contiene puertas binarias arbitrarias se puede decidir a tiempo . [4]
Dado un circuito y un conjunto satisfactorio de entradas, se puede calcular la salida de cada puerta en tiempo constante. Por tanto, la salida del circuito es verificable en tiempo polinomial. Por tanto, el circuito SAT pertenece a la clase de complejidad NP. Para mostrar la dureza NP , es posible construir una reducción de 3SAT al Circuito SAT.
Supongamos que la fórmula original de 3SAT tiene variables y operadores (Y, O, NO) . Diseñe un circuito tal que tenga una entrada correspondiente a cada variable y una puerta correspondiente a cada operador. Conecte las puertas según la fórmula 3SAT. Por ejemplo, si la fórmula 3SAT es el circuito tendrá 3 entradas, una puerta Y, una O y una NO. La entrada correspondiente a se invertirá antes de enviar a una puerta AND con y la salida de la puerta AND se enviará a una puerta OR con
Tenga en cuenta que la fórmula 3SAT es equivalente al circuito diseñado anteriormente, por lo tanto, su salida es la misma para la misma entrada. Por lo tanto, si la fórmula 3SAT tiene una asignación satisfactoria, entonces el circuito correspondiente generará 1 y viceversa. Entonces, esta es una reducción válida y el Circuit SAT es NP-duro.
Esto completa la prueba de que el Circuito SAT es NP-Completo.
Supongamos que tenemos un circuito booleano plano (es decir, un circuito booleano cuyo gráfico subyacente es plano ) que contiene sólo puertas NAND con exactamente dos entradas. Planar Circuit SAT es el problema de decisión de determinar si este circuito tiene una asignación de sus entradas que hace que la salida sea verdadera. Este problema es NP-completo. Además, si se cambian las restricciones de modo que cualquier puerta del circuito sea una puerta NOR , el problema resultante sigue siendo NP-completo. [5]
El circuito UNSAT es el problema de decisión de determinar si un circuito booleano dado genera resultados falsos para todas las asignaciones posibles de sus entradas. Este es el complemento del problema del Circuito SAT y, por lo tanto, es Co-NP-completo .
La reducción de CircuitSAT o sus variantes se puede utilizar para mostrar la dureza NP de ciertos problemas y nos proporciona una alternativa a las reducciones de lógica binaria y de doble carril. Los elementos que dicho recorte debe construir son:
Este problema pregunta si es posible localizar todas las bombas con un tablero Buscaminas . Se ha demostrado que es CoNP completo mediante una reducción del problema del circuito UNSAT. [6] Los dispositivos construidos para esta reducción son: alambre, división, puertas Y y NO y terminador. [7] Hay tres observaciones cruciales con respecto a estos dispositivos. En primer lugar, el dispositivo dividido también se puede utilizar como dispositivo NO y como dispositivo de giro. En segundo lugar, basta con construir dispositivos Y y NO, porque juntos pueden simular la puerta NAND universal. Finalmente, dado que se pueden componer tres NAND sin intersecciones para implementar un XOR, y dado que XOR es suficiente para construir un cruce, [8] esto nos proporciona el dispositivo de cruce necesario.
La transformación de Tseytin es una reducción sencilla de Circuit-SAT a SAT . La transformación es fácil de describir si el circuito está construido completamente con puertas NAND de 2 entradas (un conjunto funcionalmente completo de operadores booleanos): asigne a cada red del circuito una variable, luego, para cada puerta NAND, construya la forma normal conjuntiva cláusulas ( v 1 ∨ v 3 ) ∧ ( v 2 ∨ v 3 ) ∧ (¬ v 1 ∨ ¬ v 2 ∨ ¬ v 3 ), donde v 1 y v 2 son las entradas a la puerta NAND y v 3 es la salida . Estas cláusulas describen completamente la relación entre las tres variables. Combinar las cláusulas de todas las compuertas con una cláusula adicional que restrinja la variable de salida del circuito para que sea verdadera completa la reducción; existe una asignación de las variables que satisfacen todas las restricciones si y sólo si el circuito original es satisfactorio, y cualquier solución es una solución al problema original de encontrar entradas que hagan que el circuito produzca 1. [1] [9] Lo contrario: que SAT es reducible a Circuit-SAT: sigue trivialmente reescribiendo la fórmula booleana como un circuito y resolviéndola.
