Is there CIRCUIT-SAT algorithms that slightly depends on gates count?

Question

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?

Answer 1

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.