Problema de satisfacibilidad de circuitos

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 consistentemente en 1 o 0 de manera que el circuito produzca una salida de 1. Si ese es el caso, el circuito se llama satisfacible . De lo contrario, el circuito se llama 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 booleana (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 entonces CircuitSAT puede reducirse a los otros problemas de satisfacibilidad para demostrar su NP-completitud. ^{[ 1 ] [ 3 ]} La satisfacibilidad de un circuito que contiene${\displaystyle m}$Las compuertas binarias arbitrarias pueden decidirse en el tiempo${\displaystyle O(2^{0,4058m})}$. ^{[ 4 ]}

Dado un circuito y un conjunto de entradas que satisfacen la condición, se puede calcular la salida de cada puerta en tiempo constante. Por lo tanto, la salida del circuito es verificable en tiempo polinomial. Así, Circuit SAT pertenece a la clase de complejidad NP. Para demostrar la NP-dificultad , es posible construir una reducción de 3SAT a Circuit SAT.

Supongamos que la fórmula 3SAT original tiene variables${\displaystyle x_{1},x_{2},\dots ,x_{n}}$y operadores (AND, OR, NOT)${\displaystyle y_{1},y_{2},\dots,y_{k}}$Diseña un circuito de tal manera que tenga una entrada correspondiente a cada variable y una compuerta correspondiente a cada operador. Conecta las compuertas según la fórmula 3SAT. Por ejemplo, si la fórmula 3SAT es${\displaystyle (\lnot x_{1}\land x_{2})\lor x_{3},}$El circuito tendrá 3 entradas, una puerta AND, una puerta OR y una puerta NOT. La entrada correspondiente a${\displaystyle x_{1}}$se invertirá antes de enviarlo a una puerta AND con${\displaystyle x_{2},}$y la salida de la puerta AND se enviará a una puerta OR con${\displaystyle x_{3}.}$

Nótese que la fórmula 3SAT es equivalente al circuito diseñado anteriormente; por lo tanto, su salida es la misma para la misma entrada. En consecuencia, si la fórmula 3SAT tiene una asignación satisfactoria, el circuito correspondiente dará como resultado 1, y viceversa. Por lo tanto, se trata de una reducción válida, y el problema Circuit SAT es NP-difícil.

Esto completa la demostración de que el problema SAT de circuitos es NP-completo.

La reducción de CircuitSAT o sus variantes se puede utilizar para demostrar la NP-dificultad de ciertos problemas y nos proporciona una alternativa a las reducciones de lógica binaria y de doble riel. Los componentes que dicha reducción necesita construir son:

• Un dispositivo de cableado. Este dispositivo simula los cables del circuito.
• Un dispositivo divisor. Este dispositivo garantiza que todos los cables de salida tengan el mismo valor que el cable de entrada.
• Dispositivos que simulan las compuertas del circuito.
• Un auténtico dispositivo terminador. Este dispositivo se utiliza para forzar que la salida de todo el circuito sea verdadera.
• Un dispositivo de giro. Este dispositivo nos permite redirigir los cables en la dirección correcta según sea necesario.
• Un dispositivo de cruce. Este dispositivo nos permite cruzar dos cables sin que interactúen entre sí.

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 a partir de puertas NAND de 2 entradas (un conjunto funcionalmente completo de operadores booleanos): se asigna a cada red en el circuito una variable, luego para cada puerta NAND, se construyen las cláusulas de forma normal conjuntiva ( v ₁ ∨ v ₃ ) ∧ ( v ₂ ∨ v ₃ ) ∧ (¬ v ₁ ∨ ¬ v ₂ ∨ ¬ v ₃ ), donde v ₁ y v ₂ son las entradas a la puerta NAND y v ₃ es la salida. Estas cláusulas describen completamente la relación entre las tres variables. Uniendo las cláusulas de todas las puertas con una cláusula adicional que restringe que la variable de salida del circuito sea verdadera se completa la reducción; Existe una asignación de las variables que satisface 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 recíproco —que SAT es reducible a circuito-SAT— se deduce trivialmente reescribiendo la fórmula booleana como un circuito y resolviéndolo.

• Problema de valor del circuito
• Satisfacibilidad de circuitos estructurados
• Problema de satisfacibilidad