What is known about the complexity of finding minimal circuits that compute SAT up to length $n$?  More formally: what is the complexity of a function which, given $1^{n}$ as input outputs a minimal circuit $C$ such that for any formula $\varphi$ with $|\varphi| \leq n$, $C(\varphi) = SAT(\varphi)$?(I'm specifically interested in lower bounds.)The naive deterministic algorithm (compute SAT by brute force up to length $n$, then try all circuits in order of size until you find one that correctly computes SAT up to length $n$) takes $\leq 2^{O(n)}$ time to compute SAT, and then an additional $O(2^n 2^M)$ time to find a minimal circuit, where $M$ is the size of the minimal circuit.  Is there a deterministic algorithm that finds minimal circuits for SAT whose running time is $o(2^n 2^M)$, where $M$ is the size of the minimal circuit?  Or does this imply some complexity collapse?Here are two things that, although related to my question, are definitely not what I'm asking about (which is, I think, why I found it a little difficult to search for):The circuit minimization problem: given a circuit $C$ (or a function $f$ given by its truth table, or several other variants) find a minimal circuit $C'$ computing the same function as $C$.  Even if circuit minimization were easy, it would not necessarily imply that the above task is easy, as even computing the function we want to minimize (SAT up to length $n$) is believed to be hard, whereas in the circuit minimization problem the function we want to minimize is free (it's given as the input).$NP$ versus $P/poly$.  My question is not merely about what size the minimal circuit has; it is about the complexity of finding a minimal circuit, regardless of its size.  Obviously if we can compute minimal circuits in polynomial time then $NP \subseteq P/poly$ (and in fact $NP \subseteq P$, since then the circuit family is $P$-uniform), but the converse need not be true.  Indeed, I believe Immerman and Mahaney were the first to construct an oracle where $NP \subseteq P/poly$ but $P \neq NP$ -- that is, $NP$ has polynomial-size circuits but they cannot be found in polynomial time.
What is known about the complexity of finding minimum circuits for SAT?
cc.complexity theory;sat