 Tseitin transformation

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.