Transformação de Tseytin

A transformação de Tseytin, alternativamente escrita  como transformação de Tseitin tem como entrada um circuito lógico combinatório arbitrário e produz uma fórmula booleana na forma normal conjuntiva (FNC), o que pode ser resolvido através de um solucionador FNC-SAT. O comprimento da fórmula é linear no tamanho do circuito. Vetores de entrada que fazem a saída do circuito ser "verdadeira" estão na correspondência 1-para-1 com as atribuições que satisfazem a fórmula. Isto reduz o problema da satisfatibilidade do circuito em qualquer circuito (incluindo qualquer fórmula) para o problema da satisfatibilidade nas fórmulas 3-FNC.

Motivação

A alternativa é escrever o circuito como uma expressão Booleana, e usar a lei de De Morgan e a propriedade distributiva para convertê-lo para FNC. No entanto, isso pode resultar em um aumento exponencial no tamanho da equação. A transformação de Tseytin dá como saída uma fórmula, cujo tamanho cresce linearmente em relação à entrada do circuito.

Abordagem

A equação de saída é a constante 1 igual a uma expressão. Esta expressão é um conjunto de sub-expressões, onde a satisfação de cada sub-expressão impõe o bom funcionamento de uma única porta na entrada do circuito. A satisfação de toda a saída da expressão, portanto, impõe que toda a entrada do circuito está funcionando corretamente.

Para cada porta, uma nova variável que representa a sua saída é introduzida. Uma pequena expressão FNC pré-calculada que relaciona as entradas e saídas é acrescentada (através de uma operação "e") para a expressão de saída. Observe que as entradas para estas portas, podem ser para literais originais ou para introdução de variáveis que representam saídas de sub-portas.

Embora a expressão de saída contém mais variáveis do que a de entrada, ele permanece equisatisfatível, o que significa que ele é satisfatível se, e somente se,a entrada original da equação é satisfatível. Quando uma atribuição satisfatória de variáveis é encontrada, essas atribuições para as variáveis introduzidas pode ser simplesmente descartada.

A cláusula final, é acrescentada com um único literal: a última saída da porta da variável. Se este literal é complementado, então, a satisfação desta cláusula aplica a expressão de saída para falso; caso contrário, a expressão é forçado para verdadeiro.

Exemplos

Considere a seguinte fórmula $\phi$ .

$\phi :=((p\lor q)\land r)\to (\neg s)$

Considere todos as subformulas (sem variáveis):

${\begin{aligned}&\neg s\\&p\lor q\\&(p\lor q)\land r\\&((p\lor q)\land r)\to (\neg s)\end{aligned}}$

Introduza uma nova variável para cada subformula:

${\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}}$

Em conjunção com todas as substituições e a substituição para $\phi$:

$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 as substituições podem ser transformadas em FNC, e.g.

${\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}}$

Sub-expressões de porta

Algumas sub-expressões possíveis estão listadas que podem ser criadas para diferentes portas lógicas. Em uma operação de expressão, C age como uma saída; uma sub-expressão FNC, C age como uma nova variável Booleana. Para cada operação, a sub-expressão FNC é verdadeira se, e somente se, C adere ao contrato de operação Booleana para todos os possíveis valores de entrada.

Type	Operation	CNF Sub-expression
AND	$C=A\cdot B$	$({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee {\overline {C}})\wedge (B\vee {\overline {C}})$
NAND	$C={\overline {A\cdot B}}$	$({\overline {A}}\vee {\overline {B}}\vee {\overline {C}})\wedge (A\vee C)\wedge (B\vee C)$
OR	$C=A+B$	$(A\vee B\vee {\overline {C}})\wedge ({\overline {A}}\vee C)\wedge ({\overline {B}}\vee C)$
NOR	$C={\overline {A+B}}$	$(A\vee B\vee C)\wedge ({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})$
NOT	$C={\overline {A}}$	$({\overline {A}}\vee {\overline {C}})\wedge (A\vee C)$
XOR	$C=A\oplus B$	$({\overline {A}}\vee {\overline {B}}\vee {\overline {C}})\wedge (A\vee B\vee {\overline {C}})\wedge (A\vee {\overline {B}}\vee C)\wedge ({\overline {A}}\vee B\vee C)$

Lógica combinatória simples 

O circuito a seguir retorna verdade quando pelo menos algumas de suas entradas são verdadeiras, mas não mais do que duas vezes. Ele implementa a equação $y={\overline {x1}}\cdot x2+x1\cdot {\overline {x2}}+{\overline {x2}}\cdot x3$. Uma variável é introduzida para cada saída das portas; aqui cada um é marcado em vermelho:

Observe que a saída do inversor com $x_{2}$ como uma entrada tem duas variáveis introduzidas. Enquanto isso é redundante, não afeta a equisatisfatibilidade da equação resultante. Agora substitua cada porta com a sub-expressão apropriada FNC:

porta	sub-expressão FNC
$gate1$	$(gate1\vee x1)\wedge ({\overline {gate1}}\vee {\overline {x1}})$
$gate2$	$({\overline {gate2}}\vee gate1)\wedge ({\overline {gate2}}\vee x2)\wedge ({\overline {x2}}\vee gate2\vee {\overline {gate1}})$
$gate3$	$(gate3\vee x2)\wedge ({\overline {gate3}}\vee {\overline {x2}})$
$gate4$	$({\overline {gate4}}\vee x1)\wedge ({\overline {gate4}}\vee gate3)\wedge ({\overline {gate3}}\vee gate4\vee {\overline {x1}})$
$gate5$	$(gate5\vee x2)\wedge ({\overline {gate5}}\vee {\overline {x2}})$
$gate6$	$({\overline {gate6}}\vee gate5)\wedge ({\overline {gate6}}\vee x3)\wedge ({\overline {x3}}\vee gate6\vee {\overline {gate5}})$
$gate7$	$(gate7\vee {\overline {gate2}})\wedge (gate7\vee {\overline {gate4}})\wedge (gate2\vee {\overline {gate7}}\vee gate4)$
$gate8$	$(gate8\vee {\overline {gate6}})\wedge (gate8\vee {\overline {gate7}})\wedge (gate6\vee {\overline {gate8}}\vee gate7)$

A saída final da variável é a $gate8$ então, para impor que a saída deste circuito seja verdadeira, uma  cláusula final simples é acrescentada: $(gate8)$. Combinando estas equações resulta em última instância de SAT:

$(gate1\vee x1)\wedge ({\overline {gate1}}\vee {\overline {x1}})\wedge ({\overline {gate2}}\vee gate1)\wedge ({\overline {gate2}}\vee x2)\wedge$ $({\overline {x2}}\vee gate2\vee {\overline {gate1}})\wedge (gate3\vee x2)\wedge ({\overline {gate3}}\vee {\overline {x2}})\wedge ({\overline {gate4}}\vee x1)\wedge$ $({\overline {gate4}}\vee gate3)\wedge ({\overline {gate3}}\vee gate4\vee {\overline {x1}})\wedge (gate5\vee x2)\wedge$ $({\overline {gate5}}\vee {\overline {x2}})\wedge ({\overline {gate6}}\vee gate5)\wedge ({\overline {gate6}}\vee x3)\wedge$ $({\overline {x3}}\vee gate6\vee {\overline {gate5}})\wedge (gate7\vee {\overline {gate2}})\wedge (gate7\vee {\overline {gate4}})\wedge$ $(gate2\vee {\overline {gate7}}\vee gate4)\wedge (gate8\vee {\overline {gate6}})\wedge (gate8\vee {\overline {gate7}})\wedge$ $(gate6\vee {\overline {gate8}}\vee gate7)\wedge (gate8)=1$

Uma possível atribuição satisfatória destas variáveis é:

variável	valor
gate2	0
gate3	1
gate1	1
gate6	1
gate7	0
gate4	0
gate5	1
gate8	1
x2	0
x3	1
x1	0

Os valores dos valores introduzidos são normalmente descartados, mas eles podem ser usados para rastrear o caminho lógico do circuito original. Aqui, $(x1,x2,x3)=(0,0,1)$ de fato, satisfaz os critérios para o circuito original para  ter como saída verdade. Para encontrar uma resposta diferente, a cláusula $(x1\vee x2\vee {\overline {x3}})$ pode ser acrescentada e o solucionador SAT executado novamente.

Derivação

Apresentada é a de uma possível derivação da sub-expressão FNC  para algumas portas escolhidas:

Porta OR 

Uma porta OR com duas entradas A e B e uma saída C  satisfaz as seguintes condições:

1. se a saída C é verdadeira, então pelo menos uma das entradas A ou B é verdadeiro,
2. se a saída C é falsa, tanto em suas entradas A e B são falsas.

Podemos expressar estas duas condições como a conjunção de duas implicações:

$(C\rightarrow (A\vee B))\wedge ({\overline {C}}\rightarrow ({\overline {A}}\wedge {\overline {B}}))$

Substituindo as implicações com expressões equivalentes envolvendo apenas conjunções, disjunções, e negações de rendimentos

$({\overline {C}}\vee (A\vee B))\wedge (C\vee ({\overline {A}}\wedge {\overline {B}})),$

que é quase  forma normal conjuntiva. A distribuição da extrema cláusula à direita duas vezes rendimentos

$({\overline {C}}\vee A\vee B)\wedge ((C\vee {\overline {A}})\wedge (C\vee {\overline {B}})),$

e aplicando a associatividade ' do conjunto dá a fórmula CNF

$({\overline {C}}\vee A\vee B)\wedge (C\vee {\overline {A}})\wedge (C\vee {\overline {B}})$

Porta NOT

A porta NOT está operando adequadamente quando sua entrada e saída se opõem. O que é:

1. se a saída C é verdade, a entrada A é falso
2. se a saída C é falsa, a entrada de Um é verdadeiro

expressar essas condições, como uma expressão que deve ser satisfeita: $(C\rightarrow {\overline {A}})\wedge ({\overline {C}}\rightarrow A)$ $({\overline {C}}\vee {\overline {A}})\wedge (C\vee A)$

Porta NOR

A porta NOR está operando adequadamente quando mantém as seguintes condições:

1. se a saída C é verdadeira, então nem A e nem B forem verdadeiras
2. se a saída C é falsa, pelo menos um de A e B eram verdadeiras

expressar essas condições, como uma expressão que deve ser satisfeita:

$(C\rightarrow {\overline {(A\vee B)}})\wedge ({\overline {C}}\rightarrow (A\vee B))$

${\overline {\overline {({\overline {C}}\vee ({\overline {A}}\wedge {\overline {B}}))}}}\wedge (C\vee A\vee B))$

${\overline {(C\wedge (A\vee B))}}\wedge (C\vee A\vee B))$

${\overline {(A\wedge C)\vee (B\wedge C)}}\wedge (C\vee A\vee B))$

$({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})\wedge (C\vee A\vee B))$

Referências

• G. S. Tseytin: a complexidade de derivação no cálculo proposicional. Em: Slisenko, A. O. (ed.) Estudos Construtivas Matemática e Lógica Matemática, Parte II, dos Seminários de Matemática, pp. 115–125. Matemática Steklov Institute (1970). Traduzido de russo: Zapiski Nauchnykh Seminarov LOMI 8 (1968), pp. 234-259.