User:Alamoureux/sandbox

The Tseitin Transformation is used to produce a boolean equation in conjunctive normal form (CNF) from a combinatorial logic circuit so that it may be solved by a SAT solver.

Motivation

The naive approach is to write the circuit as an equation, and use De Morgan's law and distribution. However, this can result in an exponential increase in equation size. The Tseitin Transformation outputs an equation whose size has grown linearly relative to the input circuit's.

Approach

The output equation is the constant 1 set equal to an expression. This expression is a conjunction of sub-expressions, where the satisfaction of each sub-expression enforces the proper operation of a single gate in the input circuit. The satisfaction of the entire output expression thus enforces that the entire input circuit is operating properly.

For each gate, a new variable representing its output is introduced. A small pre-calculated CNF expression that relates the inputs and outputs is appended (via the and operation) the output expression. Note that inputs to these gates can be both the original literals, or the introduced variables representing outputs of sub-gates.

A final clause is appended with a single literal: the final gate's output variable. If this literal is complemented, then the satisfaction of this clause enforces the output expression's to false; otherwise the expression is forced true.

Gate Sub-expressions

Listed is some of the possible sub-expressions that can be created for various logic gates.

Type	Operation	CNF Sub-expression
AND	$C=A\cdot B$	$(A\vee B\vee {\overline {C}})\wedge ({\overline {A}}\vee C)\wedge ({\overline {B}}\vee C)$
OR	$C=A+B$	$({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee {\overline {C}})\wedge (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)$
NOR	$C={\overline {A\oplus B}}$	$(A\vee B\vee C)\wedge ({\overline {A}}\vee {\overline {C}})\wedge ({\overline {B}}\vee {\overline {C}})$
NAND	$C={\overline {A\cdot B}}$	$({\overline {A}}\vee {\overline {B}}\vee C)\wedge (A\vee {\overline {C}})\wedge (B\vee {\overline {C}})$

Simple combinatorial logic

The following circuit returns true when at least some of its inputs are true, but not more than two at a time. It implements the equation $y={\overline {x1}}\cdot x2+x1\cdot {\overline {x2}}+{\overline {x2}}\cdot x3$. A variable is introduced for each gates' output; here each is marked in red:


Notice that the output of the inverter with $x_{2}$ as an input has two variables introduced. While this is redundant, it does not affect the equisatisfiability of the resulting equation. Now substitute each gate with its appropriate CNF sub-expression:

gate	CNF sub-expression
$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 t(gate6\vee {\overline {gate8}}\vee gate7)$

The final output variable is $gate8$ so to enforce that the output of this circuit be true, one final simple clause is appended: $(gate8)$. Combining these equations results in the final instance of 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$

One possible satisfying assignment of these variables is:

variable	value
gate2	0
gate3	1
gate1	1
gate6	1
gate7	0
gate4	0
gate5	1
gate8	1
x2	0
x3	1
x1	0

The values of the introduced values are usually discarded, but they can be used to trace the logic path in the original circuit. Here, $(x1,x2,x3)=(0,0,1)$ indeed meets the criteria for the original circuit to output true. To find a difference answer, the clause $(x1\vee x2\vee {\overline {x3}})$ can be appended and the SAT solver executed again.

Derivation

Presented is one possible derivation of the CNF sub-expression for some chosen gates:

AND Gate

The AND gate is operating properly when the following conditions hold:

1. if the output C is true, then one (or both) of its inputs A, B is true
2. if the output C is false, then both its inputs A, B are false

express these conditions as an expression that must be satisfied:
$(C\rightarrow (A\vee B))\wedge ({\overline {C}}\rightarrow ({\overline {A}}\wedge {\overline {B}}))$
convert the implications to AND's and OR's
$({\overline {C}}\vee (A\vee B))\wedge (C\vee ({\overline {A}}\wedge {\overline {B}}))$
it's nearly CNF already; complement the rightmost clause twice
$({\overline {C}}\vee A\vee B)\wedge {\overline {\overline {(C\vee ({\overline {A}}\wedge {\overline {B}}))}}}$
apply De Morgan's law once
$({\overline {C}}\vee A\vee B)\wedge {\overline {({\overline {C}}\wedge (A\vee B))}}$
distribute
$({\overline {C}}\vee A\vee B)\wedge {\overline {(({\overline {C}}\wedge A)\vee ({\overline {C}}\wedge B)))}}$
apply De Morgan's law
$({\overline {C}}\vee A\vee B)\wedge (C\vee {\overline {A}})\wedge (C\vee {\overline {B}})$

NOT Gate

The NOT gate is operating properly when its input and output oppose each other. That is:

1. if the output C is true, the input A is false
2. if the output C is false, the input A is true

express these conditions as an expression that must be satisfied:
$(C\rightarrow {\overline {A}})\wedge ({\overline {C}}\rightarrow A)$
$({\overline {C}}\vee {\overline {A}})\wedge (C\vee A)$

NOR Gate

The NOR gate is operating properly when the following conditions hold:

1. if the output C is true, then neither A or B are true
2. if the output C is false, then at least one of A and B were true

express these conditions as an expression that must be satisfied:
$(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 (A\vee B)}}\wedge (C\vee A\vee B))$
$({\overline {A}}\vee {\overline {C}})\wedge ({\overline {A}}\wedge {\overline {B}})\wedge (C\vee A\vee B))$

References

• G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115–125. Steklov Mathematical Institute (1968)