P/poly vs NP separation based on circuit trees instead of DAGs

Question

there are various theorems that relate major complexity class separations to circuit family DAGs sizes, in particular for P/poly vs NP. in contrast,

are there theorems/conjectures that relate P/poly vs NP separation to the size of circuit trees (aka formulas)?

note of course that CNF/SAT is a boolean formula. an example in this form would be something like if a CNF circuit family $C_n$ requires size $\Omega(g(n))$ clauses to compute function $f$ (alternately, can compute $f'$ in $O(g'(n))$ clauses) then NP $\not\subset$ P/poly, but the question is not limited to CNF & is asking about formulas in general. ([1] is a somewhat related question)

[1] Complexity of converting a boolean circuit to a boolean formula

Answer 1

As Sasho suggested, I am putting my comment as an answer.

The separations between monotone versions of $\mathsf{NC}^1/\mathsf{poly}$ and $\mathsf{P/poly}$ versions of complexity are long known (Karchmer-Wigderson, Grigni-Sipser, etc), but in the non-monotone world almost nothing was known. Fortunately, Ben Rossman has recently found the first separation of formulas vs. circuits in the bounded depth setting.

Let $\mathrm{Circuit}(S,d)$ (resp., $\mathrm{Formula}(S,d)$) denote the set of all boolean functions computable by unbounded fanin circuits (resp. formulas) of depth $\leq d$ and size $\leq S$. It is clear that $$ \mathrm{Circuit}(S,d) \subseteq \mathrm{Formula}(S^d,d). $$ In particular, $$ \mathrm{Circuit}(n^{O(1)},d) \subseteq \mathrm{Formula}(n^{O(d)},d). $$ What Ben has shown is that, if $d=d(n)\leq \log\log\log n$, then $$ \mathrm{Circuit}(n^{O(1)},d) \not\subseteq \mathrm{Formula}(n^{o(d)},d). $$ Even more important is that he shows this separation on an explicit and basic function $\mathrm{STCONN}(n,k)$: given an $n$-vertex graph, decide whether it has an $s$-$t$ path of length $\leq k$. This function is in $\mathrm{Circuit}(n^{O(1)},\log k)$. His main result is: if $dk^3\leq \log n/\log\log n$ then $$ \mathrm{STCONN}(n,k)\in \mathrm{Formula}(S,d)\ \Longrightarrow\ S\geq n^{\Omega(\log k)}. $$ This implies a tight depth lower bound: if $k\leq \log\log n$ then $$ \mathrm{STCONN}(n,k)\in \mathrm{Circuit}(n^{O(1)},d)\ \Longrightarrow\ d=\Theta(\log k). $$ The existing techniques for small-depth circuit -- namely switching lemmas and approximation by low-degree polynomials-- do not distinguish between formulas and circuits due to their bottom-up nature. Top-down arguments, as Karchmer-Wigderson games, are difficult to realize in the non-monotone case. What Ben uses is a combination of these arguments.

Answer 2

The class of functions computable by formulas of polynomial size is equivalent to the (nonuniform) class $\mathsf{NC}^1$ of functions computable by (bounded fanin/fanout) circuits of logarithmic depth. Proving the two implications is a nice exercise. In one direction, you can recursively "untangle" each level of a circuit by creating copies of gates. This increases the size by a constant factor for each of the $O(\log n)$ levels of the circuit. The other direction is proven by balancing the tree of the formula.

Also, $\mathsf{NC}^1$ is equivalent, by Barrington's theorem, to width 5 polynomial size branching programs.

We know that the uniform version of $\mathsf{NC}^1$ is contained in $\mathsf{L} \subseteq \mathsf{P}$ ($\mathsf{L}$ stands for deterministic logspace). It is not known whether any of these containments is proper AFAIK. Also it is not known whether the non-uniform $\mathsf{NC}^1$ is a proper subset of $\mathsf{P/\text{poly}}$.