For 3CNF-SAT problems exists a lot of algorithms that still have exponential complexity, but work faster than brute force. The complexity of this algorithm based on a number of variables or the number of clauses (they can't differ a lot because polynomially bounded to each other in 3CNF).
But for CIRCUIT-SAT size of the problem (number of inputs + number of gates) may differ much more - a number of gates may be exponentially larger than the number of inputs. So, after the conversation to 3-CNF (Tseytin transformation which creates new clauses and new variable for each gate), SAT-solvers will be overperformed by naive brute force algorithm, because its complexity only linear depends on gates count (to check SAT need to iterate over all input combinations which count exponentially depends on inputs count and compute outputs for each gate which is constant time operation for each gate).
So, the question is - is there exist CIRCUIT-SAT algorithms that slightly (polynomially or better) depend on gates count and can overperform brute force on cases where gates count much larger than inputs?