La transformación de Tseytin , alternativamente escrita transformación de Tseitin , toma como entrada un circuito lógico combinatorio arbitrario y produce una fórmula booleana en forma normal conjuntiva (CNF) , que puede resolverse mediante un solucionador CNF-SAT . La longitud de la fórmula es lineal en el tamaño del circuito. Los vectores de entrada que hacen que la salida del circuito sea "verdadera" están en correspondencia 1 a 1 con las asignaciones que satisfacen la fórmula. Esto reduce el problema de satisfacibilidad del circuito en cualquier circuito (incluida cualquier fórmula) al problema de satisfacibilidad en fórmulas 3-CNF.
Motivación
El enfoque ingenuo es escribir el circuito como una expresión booleana y usar la ley de De Morgan y la propiedad distributiva para convertirlo en CNF. Sin embargo, esto puede resultar en un aumento exponencial en el tamaño de la ecuación. La transformación de Tseytin genera una fórmula cuyo tamaño crece linealmente en relación con el circuito de entrada.
Acercarse
La ecuación de salida es el conjunto constante 1 igual a una expresión. Esta expresión es una conjunción de subexpresiones, donde la satisfacción de cada subexpresión impone el funcionamiento adecuado de una sola puerta en el circuito de entrada. La satisfacción de toda la expresión de salida obliga a que todo el circuito de entrada funcione correctamente.
Para cada puerta, se introduce una nueva variable que representa su salida. Una pequeña expresión CNF precalculada que relaciona las entradas y salidas se agrega (a través de la operación "y") a la expresión de salida. Tenga en cuenta que las entradas a estas puertas pueden ser los literales originales o las variables introducidas que representan las salidas de las sub-puertas.
Aunque la expresión de salida contiene más variables que la entrada, permanece igual de satisfactoria , lo que significa que es satisfactoria si, y solo si, la ecuación de entrada original es satisfactoria. Cuando se encuentra una asignación satisfactoria de variables, esas asignaciones para las variables introducidas pueden simplemente descartarse.
Se agrega una cláusula final con un solo literal: la variable de salida de la puerta final. Si este literal se complementa, entonces la satisfacción de esta cláusula obliga a que la expresión de salida sea falsa; de lo contrario, la expresión se fuerza a verdadera.
Ejemplos de
Considere la siguiente fórmula .
Considere todas las subfórmulas (excluidas las variables simples):
Introduzca una nueva variable para cada subfórmula:
Conjunta todas las sustituciones y la sustitución de :
Todas las sustituciones se pueden transformar en CNF, p. Ej.
Sub-expresiones de puerta
Se enumeran algunas de las posibles subexpresiones que se pueden crear para varias puertas lógicas. En una expresión de operación, C actúa como salida; en una subexpresión CNF, C actúa como una nueva variable booleana. Para cada operación, la subexpresión CNF es verdadera si y solo si C se adhiere al contrato de la operación booleana para todos los valores de entrada posibles.
Tipo | Operación | CNF Sub-expresión |
---|---|---|
Y | ||
NAND | ||
O | ||
NI | ||
NO | ||
XOR | ||
XNOR |
Lógica combinatoria simple
El siguiente circuito devuelve verdadero cuando al menos algunas de sus entradas son verdaderas, pero no más de dos a la vez. Implementa la ecuación y = x1 · x2 + x1 · x2 + x2 · x3 . Se introduce una variable para la salida de cada puerta; aquí cada uno está marcado en rojo:
Observe que la salida del inversor con x 2 como entrada tiene dos variables introducidas. Si bien esto es redundante, no afecta la equisatisfacción de la ecuación resultante. Ahora sustituya cada puerta con su subexpresión CNF apropiada :
portón | CNF sub-expresión |
---|---|
puerta1 | (puerta1 ∨ x1) ∧ ( puerta1 ∨ x1 ) |
puerta2 | ( puerta2 ∨ puerta1) ∧ ( puerta2 ∨ x2) ∧ ( x2 ∨ puerta2 ∨ puerta1 ) |
puerta3 | (puerta3 ∨ x2) ∧ ( puerta3 ∨ x2 ) |
gate4 | ( puerta4 ∨ x1) ∧ ( puerta4 ∨ puerta3) ∧ ( puerta3 ∨ puerta4 ∨ x1 ) |
puerta5 | (puerta5 ∨ x2) ∧ ( puerta5 ∨ x2 ) |
puerta6 | ( puerta6 ∨ puerta5) ∧ ( puerta6 ∨ x3) ∧ ( x3 ∨ puerta6 ∨ puerta5 ) |
puerta7 | (puerta7 ∨ puerta2 ) ∧ (puerta7 ∨ puerta4 ) ∧ (puerta2 ∨ puerta7 ∨ puerta4) |
puerta8 | (puerta8 ∨ puerta6 ) ∧ (puerta8 ∨ puerta7 ) ∧ (puerta6 ∨ puerta8 ∨ puerta7) |
La variable de salida final es gate8, por lo que para hacer cumplir la salida de este circuito, se agrega una cláusula final simple: (gate8). La combinación de estas ecuaciones da como resultado la instancia final de SAT:
- (puerta1 ∨ x1) ∧ ( puerta1 ∨ x1 ) ∧ ( puerta2 ∨ puerta1) ∧ ( puerta2 ∨ x2) ∧
- ( x2 ∨ puerta2 ∨ puerta1 ) ∧ (puerta3 ∨ x2) ∧ ( puerta3 ∨ x2 ) ∧ ( puerta4 ∨ x1) ∧
- ( puerta4 ∨ puerta3) ∧ ( puerta3 ∨ puerta4 ∨ x1 ) ∧ (puerta5 ∨ x2) ∧
- ( puerta5 ∨ x2 ) ∧ ( puerta6 ∨ puerta5) ∧ ( puerta6 ∨ x3) ∧
- ( x3 ∨ puerta6 ∨ puerta5 ) ∧ (puerta7 ∨ puerta2 ) ∧ (puerta7 ∨ puerta4 ) ∧
- (puerta2 ∨ puerta7 ∨ puerta4) ∧ (puerta8 ∨ puerta6 ) ∧ (puerta8 ∨ puerta7 ) ∧
- (puerta6 ∨ puerta8 ∨ puerta7) ∧ (puerta8) = 1
Una posible asignación satisfactoria de estas variables es:
variable | valor |
---|---|
puerta2 | 0 |
puerta3 | 1 |
puerta1 | 1 |
puerta6 | 1 |
puerta7 | 0 |
gate4 | 0 |
puerta5 | 1 |
puerta8 | 1 |
x2 | 0 |
x3 | 1 |
x1 | 0 |
Los valores de las variables introducidas generalmente se descartan, pero se pueden usar para rastrear la ruta lógica en el circuito original. Aquí, (x1, x2, x3) = (0,0,1) de hecho cumple con los criterios para que el circuito original salga verdadero. Para encontrar una respuesta diferente, se puede agregar la cláusula (x1 ∨ x2 ∨ x3 ) y ejecutar nuevamente el solucionador SAT.
Derivación
Se presenta una posible derivación de la subexpresión CNF para algunas puertas elegidas:
Puerta OR
Una puerta OR con dos entradas A y B y una salida C satisface las siguientes condiciones:
- si la salida C es verdadera, entonces al menos una de sus entradas A o B es verdadera,
- si la salida C es falsa, entonces sus entradas A y B son falsas.
Podemos expresar estas dos condiciones como la conjunción de dos implicaciones:
Reemplazar las implicaciones con expresiones equivalentes que involucran solo conjunciones, disyunciones y negaciones produce
que ya está casi en forma conjuntiva normal . Distribuir la cláusula más a la derecha dos veces produce
y aplicando la asociatividad de la conjunción se obtiene la fórmula CNF
NO puerta
La puerta NOT funciona correctamente cuando su entrada y salida se oponen entre sí. Es decir:
- si la salida C es verdadera, la entrada A es falsa
- si la salida C es falsa, la entrada A es verdadera
expresar estas condiciones como expresión que debe cumplirse:
- ,
Puerta NOR
La puerta NOR está funcionando correctamente cuando se cumplen las siguientes condiciones:
- si la salida C es verdadera, entonces ni A ni B son verdaderas
- si la salida C es falsa, entonces al menos uno de A y B eran verdaderos
expresar estas condiciones como expresión que debe cumplirse:
- , , , ,
Referencias
- GS Tseytin: Sobre la complejidad de la derivación en el cálculo proposicional. En: Slisenko, AO (ed.) Estudios en Matemáticas Constructivas y Lógica Matemática, Parte II, Seminarios en Matemáticas, págs. 115-125. Instituto de Matemáticas Steklov (1970). Traducido del ruso: Zapiski Nauchnykh Seminarov LOMI 8 (1968), págs. 234-259.
- GS Tseytin: Sobre la complejidad de la derivación en el cálculo proposicional. Presentado en el Seminario de Lógica Matemática de Leningrado celebrado en septiembre de 1966.