= Tseitin transformation
{c}
{wiki=Tseytin_transformation}
= Tseytin transformation
{c}
{synonym}
Introduce a <Boolean variable> for each gate output and impose its equivalence to the gate's input function with a constant number of <clauses>. A final unit <clause> forces acceptance. For a bounded-fan-in <Boolean circuit>, the formula size is linear in the gate count and it is satisfiable exactly when some input makes the <Boolean circuit> output one. Auxiliary variables extend the satisfying assignments; this is equisatisfiability, not equality as functions of the enlarged variable set.
Back to article page
