Tseytin transformation

The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces an equisatisfiable boolean formula in conjunctive normal form (CNF).

Input vectors that make the circuit output "true" are in 1-to-1 correspondence with assignments that satisfy the formula.

The naive approach is to write the circuit as a Boolean expression, and use De Morgan's law and the distributive property to convert it to CNF.

The Tseytin transformation outputs a formula whose size grows linearly relative to the input circuit's.

Note that inputs to these gates can be either the original literals or the introduced variables representing outputs of sub-gates.

Combining these equations results in the final instance of SAT: One possible satisfying assignment of these variables is: The values of the introduced variables are usually discarded, but they can be used to trace the logic path in the original circuit.

Presented is one possible derivation of the CNF sub-expression for some chosen gates: An OR gate with two inputs A and B and one output C satisfies the following conditions: We can express these two conditions as the conjunction of two implications: Replacing the implications with equivalent expressions involving only conjunctions, disjunctions, and negations yields which is nearly in conjunctive normal form already.

Distributing the rightmost clause twice yields and applying the associativity of conjunction gives the CNF formula The NOT gate is operating properly when its input and output oppose each other.