En informática teórica , el problema de satisfacibilidad de circuitos (también conocido como CIRCUIT-SAT , CircuitSAT , CSAT , etc.) es el problema de decisión de determinar si un circuito booleano dado tiene una asignación de sus entradas que hace que la salida sea verdadera. [1] En otras palabras, pregunta si las entradas de un circuito booleano dado se pueden establecer de manera consistente en 1 o 0 de modo que el circuito genere 1 como salida . Si ese es el caso, el circuito se denomina satisfacible . De lo contrario, el circuito se denomina insatisfacible. En la figura de la derecha, el circuito de la izquierda se puede satisfacer estableciendo ambas entradas en 1 , pero el circuito de la derecha es insatisfacible.
CircuitSAT está estrechamente relacionado con el problema de satisfacibilidad booleano (SAT) y, asimismo, se ha demostrado que es NP-completo . [2] Es un problema NP-completo prototípico; el teorema de Cook-Levin a veces se demuestra en CircuitSAT en lugar de en el SAT, y luego CircuitSAT se puede reducir a los otros problemas de satisfacibilidad para demostrar su NP-completitud. [1] [3] La satisfacibilidad de un circuito que contiene puertas binarias arbitrarias se puede decidir en el tiempo . [4]
Dado un circuito y un conjunto satisfactorio de entradas, se puede calcular la salida de cada compuerta en tiempo constante. Por lo tanto, la salida del circuito es verificable en tiempo polinomial. Por lo tanto, el circuito SAT pertenece a la clase de complejidad NP. Para demostrar la dureza NP , es posible construir una reducción de 3SAT a Circuit SAT.
Supongamos que la fórmula 3SAT original tiene variables y operadores (AND, OR, NOT) . Diseñe un circuito que tenga una entrada correspondiente a cada variable y una compuerta correspondiente a cada operador. Conecte las compuertas de acuerdo con la fórmula 3SAT. Por ejemplo, si la fórmula 3SAT es , el circuito tendrá 3 entradas, una compuerta AND, una OR y una NOT. La entrada correspondiente a se invertirá antes de enviarse a una compuerta AND con y la salida de la compuerta AND se enviará a una compuerta 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. Por lo tanto, esta es una reducción válida y el circuito SAT es NP-hard.
Esto completa la prueba de que el circuito SAT es NP-completo.
Supongamos que se nos da un circuito booleano planar (es decir, un circuito booleano cuyo gráfico subyacente es planar ) que contiene solo puertas NAND con exactamente dos entradas. El circuito planar 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 en el circuito sea una puerta NOR , el problema resultante sigue siendo NP-completo. [5]
El circuito UNSAT es el problema de decisión que consiste en determinar si un circuito booleano dado genera un resultado falso 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 demostrar la dureza NP de ciertos problemas y nos proporciona una alternativa a las reducciones de lógica binaria y de doble carril. Los dispositivos que se deben construir con dicha reducción son:
Este problema plantea la pregunta de si es posible localizar todas las bombas dada una placa de Buscaminas . Se ha demostrado que es CoNP-Completo mediante una reducción del problema Circuit UNSAT. [6] Los dispositivos construidos para esta reducción son: cable, división, puertas AND y NOT y terminador. [7] Hay tres observaciones cruciales con respecto a estos dispositivos. Primero, el dispositivo dividido también se puede utilizar como dispositivo NOT y dispositivo de giro. Segundo, construir dispositivos AND y NOT es suficiente, porque juntos pueden simular la puerta NAND universal. Finalmente, dado que se pueden componer tres NAND sin intersección para implementar un XOR, y dado que XOR es suficiente para construir un crossover, [8] esto nos da el dispositivo de crossover necesario.
La transformación de Tseytin es una reducción directa de Circuit-SAT a SAT . La transformación es fácil de describir si el circuito está completamente construido con puertas NAND de 2 entradas (un conjunto funcionalmente completo de operadores booleanos): asigne a cada red en el circuito una variable, luego para cada puerta NAND, construya las cláusulas de forma normal conjuntiva ( 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. Unir las cláusulas de todas las puertas con una cláusula adicional que restringe la variable de salida del circuito a ser verdadera completa la reducción; existe una asignación de las variables que satisfacen todas las restricciones si y solo si el circuito original es satisfacible, y cualquier solución es una solución al problema original de encontrar entradas que hagan que la salida del circuito sea 1. [1] [9] Lo inverso (que SAT es reducible a Circuito-SAT) se sigue de manera trivial al reescribir la fórmula booleana como un circuito y resolverlo.
