Reduction of Circuit Satisfiability to CNFSAT
The exponential blowup when converting circuits to conjunctive normal form is avoided by introducing new variables to represent the output of each sub-circuit plus a simple set of rules represent each sub-circuit and force their output into the variables (see Tseitin transformation).  The size of the resulting CNF formula is linear to the size of the circuit, and grows linearly as the circuit size is increased.