Reduction of Circuit Satisfiability to CNFSAT CNFSAT is Karp reducible to Circuit-SAT by replacing all the conjunctions with AND gate, disjunctions with OR gate and negations with NOT gate. However, if we apply the same approach to Karp reduce Circuit-SAT to CNFSAT, it may result in an exponential algorithm but the instance map should be done in polynomial time.

How should we approach it then?
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.