# 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:
* se a saída C é verdadeira, então pelo menos uma das entradas A ou B é verdadeiro,
* 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 é:
* se a saída C é verdade, a entrada A é falso
* 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:
* se a saída C é verdadeira, então nem A e nem B forem verdadeiras
* 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))$