Transformación de Tseytin

La transformación de Tseytin , también conocida como transformación de Tseitin , toma como entrada un circuito lógico combinacional arbitrario y produce una fórmula booleana equisatisfacible en forma normal conjuntiva (FNC). La longitud de la fórmula es lineal con respecto al tamaño del circuito. Los vectores de entrada que hacen que la salida del circuito sea "verdadera" están en correspondencia biunívoca con las asignaciones que satisfacen la fórmula. Esto reduce el problema de la satisfacibilidad de circuitos (incluida cualquier fórmula) al problema de la satisfacibilidad de fórmulas en FNC de 3 dimensiones. Fue descubierta por el científico ruso Grigori Tseitin .

El enfoque ingenuo consiste en escribir el circuito como una expresión booleana y utilizar la ley de De Morgan y la propiedad distributiva para convertirlo a la forma normal conjuntiva (FNC). Sin embargo, esto puede resultar en un aumento exponencial del tamaño de la ecuación. La transformación de Tseytin produce una fórmula cuyo tamaño crece linealmente en relación con el del circuito de entrada. La aplicación original consistía en crear "pasajeros estadísticos" para una empresa de transporte nórdica a partir de los billetes de un solo viaje de un día, uniendo efectivamente viajes sin etiquetar que podrían corresponder a una sola persona.

La ecuación de salida es la constante 1 igualada a una expresión. Esta expresión es una conjunción de subexpresiones, donde el cumplimiento de cada una de ellas garantiza el correcto funcionamiento de una compuerta en el circuito de entrada. Por lo tanto, el cumplimiento de la expresión de salida completa garantiza el correcto funcionamiento de todo el circuito de entrada.

Para cada compuerta, se introduce una nueva variable que representa su salida. A la expresión de salida se le añade, mediante la operación lógica "y", una pequeña expresión precalculada en forma normal conjuntiva (FNC) que relaciona las entradas y las salidas. Cabe destacar que las entradas a estas compuertas pueden ser tanto los literales originales como las variables introducidas que representan las salidas de las subcompuertas.

Aunque la expresión de salida contiene más variables que la de entrada, sigue siendo equisatisfacible , lo que significa que es satisfacible si y solo si la ecuación de entrada original es satisfacible. Cuando se encuentra una asignación de variables satisfactoria, dichas asignaciones para las variables introducidas pueden simplemente descartarse.

A la cláusula final se le añade un literal único: la variable de salida de la puerta final. Si este literal se complementa, la satisfacción de esta cláusula hace que la expresión de salida sea falsa; de lo contrario, la expresión se fuerza a ser verdadera.

Considere la siguiente fórmula $${\displaystyle \phi$$ :=((p\lor q)\land r)\to (\neg s).}

Consideremos todas las subfórmulas (excluyendo las variables simples): $${\displaystyle {\begin{aligned}&\neg s,\\&p\lor q,\\&(p\lor q)\land r,\\&((p\lor q)\land r)\to (\neg s).\end{aligned}}}$$

Introduzca una nueva variable para cada subfórmula: $${\displaystyle {\begin{aligned}x_{1}&\leftrightarrow \neg s,\\x_{2}&\leftrightarrow p\lor q,\\x_{3}&\leftrightarrow x_{2}\land r,\\x_{4}&\leftrightarrow x_{3}\to x_{1}.\end{aligned}}}$$

Conjunte todas las sustituciones y la sustitución por${\displaystyle \phi }$: $${\displaystyle T(\phi ):=x_{4}\land (x_{4}\leftrightarrow x_{3}\to x_{1})\land (x_{3}\leftrightarrow x_{2}\land r)\land (x_{2}\leftrightarrow p\lor q)\land (x_{1}\leftrightarrow \neg s).}$$

Todas las sustituciones se pueden transformar en FNC, por ejemplo $${\displaystyle {\begin{aligned}x_{2}\leftrightarrow p\lor q&\equiv (x_{2}\to (p\lor q))\land ((p\lor q)\to x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg (p\lor q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land ((\neg p\land \neg q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg p\lor x_{2})\land (\neg q\lor x_{2}).\end{aligned}}}$$

A continuación se enumeran algunas de las posibles subexpresiones que se pueden crear para diversas compuertas lógicas. En una expresión de operación, C actúa como una 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 cumple el contrato de la operación booleana para todos los posibles valores de entrada.

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 compuerta; aquí cada una está marcada en rojo:

Nótese que la salida del inversor con x ₂ como entrada tiene dos variables introducidas. Si bien esto es redundante, no afecta la equisatisfacibilidad de la ecuación resultante. Ahora sustituya cada puerta con su subexpresión CNF apropiada:

La variable de salida final es gate8, por lo que para garantizar que la salida de este circuito sea verdadera, se agrega una cláusula simple final: (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:

Los valores de las variables introducidas suelen descartarse, pero pueden utilizarse para rastrear la ruta lógica en el circuito original. Aquí,${\displaystyle (x1,x2,x3)=(0,0,1)}$De hecho, cumple con los criterios para que el circuito original dé como resultado verdadero. Para encontrar una respuesta diferente, se puede agregar la cláusula (x1 ∨ x2 ∨ x3 ) y ejecutar nuevamente el solucionador SAT.

Se presenta una posible derivación de la subexpresión CNF para algunas compuertas elegidas:

• GS Tseytin , "Sobre la complejidad de la derivación en el cálculo proposicional" . En: Slisenko, A.  O. (ed.) Estudios en matemáticas constructivas y lógica matemática, Parte II , Seminarios en matemáticas, pp.  115-125 . Instituto Matemático Steklov (1970). Traducido del ruso: Zapiski Nauchnykh Seminarov LOMI 8 (1968), pp.  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.