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 .
Considere todos as subformulas (sem variáveis):
Introduza uma nova variável para cada subformula:
Em conjunção com todas as substituições e a substituição para :
Todas as substituições podem ser transformadas em FNC, e.g.
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 symbol AND NAND symbol NAND OR symbol OR NOR symbol NOR NOT symbol NOT XOR symbol XOR
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 . Uma variável é introduzida para cada saída das portas; aqui cada um é marcado em vermelho: Ficheiro:Comb_logic_tseitin.svg
Observe que a saída do inversor com 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: portasub-expressão FNC A saída final da variável é a então, para impor que a saída deste circuito seja verdadeira, uma cláusula final simples é acrescentada: . Combinando estas equações resulta em última instância de SAT:
Uma possível atribuição satisfatória destas variáveis é: variávelvalorgate20gate31 gate11 gate61 gate70 gate40 gate51 gate81 x20 x31 x10 Os valores dos valores introduzidos são normalmente descartados, mas eles podem ser usados para rastrear o caminho lógico do circuito original. Aqui, de fato, satisfaz os critérios para o circuito original para ter como saída verdade. Para encontrar uma resposta diferente, a cláusula 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:
Substituindo as implicações com expressões equivalentes envolvendo apenas conjunções, disjunções, e negações de rendimentos
que é quase forma normal conjuntiva. A distribuição da extrema cláusula à direita duas vezes rendimentos
e aplicando a associatividade ' do conjunto dá a fórmula CNF
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:
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:
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. Categoria:Porta lógica