Yes, such an algorithm exists, but it is the same algorithm used for SAT solving in general.

While the Tseytin extension variables associated with gates do appear in the CNF transformation of the original circuit, a minimally competent SAT solver will rarely branch on them. This is because one of the earliest heuristics discovered for speeding up searches was choosing decision variables based on how often they appear in clauses. The one-per-subformula Tseytin extension variables appear in only a few clauses, while the original input variables will be involved in many clauses as the leaves of the tree of Tseytin extensions. So the Tseytin variables will all have low scores and won’t be used often as decision variables. The solver will therefore iterate through assignments of the input variables much like a brute-force search would, except that it will also take advantage of unit propagation, clause learning and all the other features of a modern SAT solver to get through the search space faster.

I say “minimally competent SAT solver” above because a really competent solver would take advantage of well-known CNF preprocessing techniques that can remove most of these gate variables before the actual solver search even starts. So CIRCUIT-SAT solvers are generally just SAT solvers. You *can* gain speed in some circumstances by having access to the original circuit in addition to the CNF result, but the gate variables don’t much factor into that.