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 $ϕ$ .

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

Considere todos as subformulas (sem variáveis):

\begin{matrix} \neg s \\ p \lor q \\ (p \lor q) \land r \\ ((p \lor q) \land r) \to (\neg s) \end{matrix}

Introduza uma nova variável para cada subformula:

\begin{matrix} 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{matrix}

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

T (ϕ) : = 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{matrix} 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{matrix}

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} \lor \overline{B} \lor C) \land (A \lor \overline{C}) \land (B \lor \overline{C})$
NAND	$C = \overline{A \cdot B}$	$(\overline{A} \lor \overline{B} \lor \overline{C}) \land (A \lor C) \land (B \lor C)$
OR	$C = A + B$	$(A \lor B \lor \overline{C}) \land (\overline{A} \lor C) \land (\overline{B} \lor C)$
NOR	$C = \overline{A + B}$	$(A \lor B \lor C) \land (\overline{A} \lor \overline{C}) \land (\overline{B} \lor \overline{C})$
NOT	$C = \overline{A}$	$(\overline{A} \lor \overline{C}) \land (A \lor C)$
XOR	$C = A \oplus B$	$(\overline{A} \lor \overline{B} \lor \overline{C}) \land (A \lor B \lor \overline{C}) \land (A \lor \overline{B} \lor C) \land (\overline{A} \lor B \lor 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{x 1} \cdot x 2 + x 1 \cdot \overline{x 2} + \overline{x 2} \cdot x 3$ . 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
$g a t e 1$	$(g a t e 1 \lor x 1) \land (\overline{g a t e 1} \lor \overline{x 1})$
$g a t e 2$	$(\overline{g a t e 2} \lor g a t e 1) \land (\overline{g a t e 2} \lor x 2) \land (\overline{x 2} \lor g a t e 2 \lor \overline{g a t e 1})$
$g a t e 3$	$(g a t e 3 \lor x 2) \land (\overline{g a t e 3} \lor \overline{x 2})$
$g a t e 4$	$(\overline{g a t e 4} \lor x 1) \land (\overline{g a t e 4} \lor g a t e 3) \land (\overline{g a t e 3} \lor g a t e 4 \lor \overline{x 1})$
$g a t e 5$	$(g a t e 5 \lor x 2) \land (\overline{g a t e 5} \lor \overline{x 2})$
$g a t e 6$	$(\overline{g a t e 6} \lor g a t e 5) \land (\overline{g a t e 6} \lor x 3) \land (\overline{x 3} \lor g a t e 6 \lor \overline{g a t e 5})$
$g a t e 7$	$(g a t e 7 \lor \overline{g a t e 2}) \land (g a t e 7 \lor \overline{g a t e 4}) \land (g a t e 2 \lor \overline{g a t e 7} \lor g a t e 4)$
$g a t e 8$	$(g a t e 8 \lor \overline{g a t e 6}) \land (g a t e 8 \lor \overline{g a t e 7}) \land (g a t e 6 \lor \overline{g a t e 8} \lor g a t e 7)$

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

$(g a t e 1 \lor x 1) \land (\overline{g a t e 1} \lor \overline{x 1}) \land (\overline{g a t e 2} \lor g a t e 1) \land (\overline{g a t e 2} \lor x 2) \land$ $(\overline{x 2} \lor g a t e 2 \lor \overline{g a t e 1}) \land (g a t e 3 \lor x 2) \land (\overline{g a t e 3} \lor \overline{x 2}) \land (\overline{g a t e 4} \lor x 1) \land$ $(\overline{g a t e 4} \lor g a t e 3) \land (\overline{g a t e 3} \lor g a t e 4 \lor \overline{x 1}) \land (g a t e 5 \lor x 2) \land$ $(\overline{g a t e 5} \lor \overline{x 2}) \land (\overline{g a t e 6} \lor g a t e 5) \land (\overline{g a t e 6} \lor x 3) \land$ $(\overline{x 3} \lor g a t e 6 \lor \overline{g a t e 5}) \land (g a t e 7 \lor \overline{g a t e 2}) \land (g a t e 7 \lor \overline{g a t e 4}) \land$ $(g a t e 2 \lor \overline{g a t e 7} \lor g a t e 4) \land (g a t e 8 \lor \overline{g a t e 6}) \land (g a t e 8 \lor \overline{g a t e 7}) \land$ $(g a t e 6 \lor \overline{g a t e 8} \lor g a t e 7) \land (g a t e 8) = 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, $(x 1, x 2, x 3) = (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 $(x 1 \lor x 2 \lor \overline{x 3})$ 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 \to (A \lor B)) \land (\overline{C} \to (\overline{A} \land \overline{B}))

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

(\overline{C} \lor (A \lor B)) \land (C \lor (\overline{A} \land \overline{B})),

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

(\overline{C} \lor A \lor B) \land ((C \lor \overline{A}) \land (C \lor \overline{B})),

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

(\overline{C} \lor A \lor B) \land (C \lor \overline{A}) \land (C \lor \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 \to \overline{A}) \land (\overline{C} \to A)$ $(\overline{C} \lor \overline{A}) \land (C \lor 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 \to \overline{(A \lor B)}) \land (\overline{C} \to (A \lor B))$

$\overline{\overline{(\overline{C} \lor (\overline{A} \land \overline{B}))}} \land (C \lor A \lor B))$

$\overline{(C \land (A \lor B))} \land (C \lor A \lor B))$

$\overline{(A \land C) \lor (B \land C)} \land (C \lor A \lor B))$

$(\overline{A} \lor \overline{C}) \land (\overline{B} \lor \overline{C}) \land (C \lor A \lor 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.

Transformação de Tseytin

Índice

Motivação

Abordagem

Exemplos

Sub-expressões de porta

Lógica combinatória simples

Derivação

Porta OR

Porta NOT

Porta NOR

Referências

Menu de navegação

Transformação de Tseytin

Motivação

Abordagem

Exemplos

Sub-expressões de porta

Lógica combinatória simples

Derivação

Porta OR

Porta NOT

Porta NOR

Referências

Menu de navegação

Pesquisa