What is known about the complexity of finding minimum circuits for SAT?

Question

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.

Answer 1

Let's assume that one cannot solve SAT much faster non-uniformly than uniformly. That is, there is a TM M solving SAT in time T(n), and the smallest circuit for SAT has size T'(n) that's not much smaller than T(n) (say, $T(n) = poly(T'(n))$ - in particular this holds if the smallest circuit for solving SAT has size $2^{\Omega(n)}$ which may very well be true).

So, you could get an "almost" minimal circuit by just running some canonical simulation of M by a circuit, in time that's basically optimal (as much time as it takes you to write the output). Just for this reason, am guessing there will be no lower bound for this question based on any "nice" assumption. However, I don't know how to go from an "almost minimal" to actually minimal. One way to do so will be to use the fact that finding the circuit up to size $S$ is a question in the polynomial hierarchy, and so you should be able to solve it in roughly $T(T(n))$ time which will be $2^{o(M)}$ if $T(n)=2^{n^{o(1)}}$.