Tseytin Transformation

The Tseytin Transformation is an algorithm for converting any propositional logic formula into CNF in linear time by adding extra variables.