<p>As Sasho suggested, I am putting my comment as an answer.</p>

<p>The separations between <em>monotone</em> 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 <em>non-monotone</em> world almost nothing was known. Fortunately, Ben Rossman <a href="http://theory.cs.uchicago.edu/abstract.php?id=rossman">has recently found</a> the first separation of formulas vs. circuits in the <em>bounded depth</em> setting.</p>

<p>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 <b>explicit</b> 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
<em>bottom-up</em> nature. <em>Top-down</em> arguments, as Karchmer-Wigderson games, are difficult to realize in the
non-monotone case. What Ben uses is a combination of these arguments. </p>

CC BY-SA 3.0
2013-11-03T16:31:53.650Z
thx! reviewing your notes, [monotone circuits](http://www.thi.informatik.uni-frankfurt.de/Seminare/SS12/monotone-circuits.pdf); do you think thm9.17, 9.18, or 9.25 (which are close to an answer to the question) could be strong enough for any P/poly$\stackrel{?}{=}$NP result, or not?
vzn
CC BY-SA 3.0
2013-11-03T19:49:34.073Z
@vzn: The answer is "most probably - NO, unless we extend the arguments to work under the presence of "auxiliary variables". The thms you mentioned are just Razborov's approximation argument "in disguise" (a "symmetric version"). And he has **proved** [here](http://people.cs.uchicago.edu/~razborov/files/approx.pdf) what we need to get it work in non-monotone case. People trying to extend his argument to non-monotone circuits should carefully read this paper to avoid disappointments.
Stasys
CC BY-SA 3.0
2013-11-04T01:47:33.537Z
was thinking along those lines & thought you might say that! yes, have heard of that paper yet strangely, there is almost/nearly no reaction to it or further analysis/commentary on it by anyone [incl your own highly/deeply comprehensive book!], eg in stark contrast to Natural Proofs [which _also_ does not mention it]. so if it really is a significant "barrier" its an extremely _low-profile_ one... & yet it has been proven that superpoly monotone lower bounds on slice functions are sufficient to separate P/poly from NP (and razborov has apparently never written _anything_ on slice fns...?)
vzn
CC BY-SA 3.0
2013-12-02T19:27:55.043Z
thx for ref, Rossman has now archived his paper at ECCC. [Formulas vs. Circuits for Small Distance Connectivity](http://eccc.hpi-web.de/report/2013/169/)
vzn
CC BY-SA 3.0
2013-11-02T15:00:50.733Z
2013-11-02T15:00:50.733Z
Stasys
<p>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.</p>

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

<p>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}}$.</p>

CC BY-SA 3.0
2013-11-01T23:29:33.047Z
+1 thx/helpful but am looking for a P/poly vs NP thm related to trees/formulas (ie higher/above P complexity)
vzn
CC BY-SA 3.0
2013-11-01T23:34:51.340Z
what I am saying is that problems decidable by polysize formulas might be (and I think are believed to be) a proper subset of P/poly. so a separation between polysize formulas and NP is not known to imply anything about P/poly vs. NP.
Sasho Nikolov
CC BY-SA 3.0
2013-11-02T01:42:15.310Z
interested in any ref related to polysize formulas $\subsetneq$ P/poly. also, edited question somewhat.
vzn
CC BY-SA 3.0
2013-11-02T03:29:16.803Z
@vzn: Evidence that L is a strict subset of P can also be taken as evidence that NC^1 (=poly formula size) is a strict subset of P/poly. See this related question: http://cstheory.stackexchange.com/questions/19315/what-are-the-compelling-reasons-for-believing-l-neq-p
Joshua Grochow
CC BY-SA 3.0
2013-11-02T13:24:18.823Z
The separations between *monotone* versions of $\mathsf{NC}^1/\mathsf{poly}$ and $\mathsf{P/poly}$ are long known (Karchmer-Wigderson, Grigni-Sipser, etc), but in the *non-monotone* world almost nothing was known. Fortunately, Ben Rossman [has recently found](http://theory.cs.uchicago.edu/abstract.php?id=rossman) the first separation of formulas vs. circuits in the *bounded depth* setting.
Stasys
CC BY-SA 3.0
2013-11-02T13:43:13.980Z
@Stasys your comment looks like it could be an answer?
Sasho Nikolov
CC BY-SA 3.0
2013-11-01T23:24:44.173Z
2013-11-01T23:29:57.093Z
2013-11-01T23:29:57.093Z
Sasho Nikolov
<p>there are various theorems that relate major complexity class separations to circuit family DAGs sizes, in particular for P/poly vs NP. in contrast,</p>

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

<p>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 &amp; is asking about formulas in general. ([1] is a somewhat related question) </p>

<p>[1] <a href="https://cstheory.stackexchange.com/questions/4867/complexity-of-converting-a-boolean-circuit-to-a-boolean-formula">Complexity of converting a boolean circuit to a boolean formula</a></p>

CC BY-SA 3.0
2013-11-01T23:39:52.270Z
your example is a bit odd: you are saying that the existence of a small-size formula for some problem would imply a class separation.  but usually such a thing implies a collapse. do you have something in mind?
Sasho Nikolov
CC BY-SA 3.0
2013-11-02T00:35:26.833Z
oops messed up the order of NP $\not\subset$ P/poly, edited that. as to your question that is reminiscent of this other question [proving lower bounds by proving upper bounds](http://cstheory.stackexchange.com/questions/3229/proving-lower-bounds-by-proving-upper-bounds)
vzn
CC BY-SA 3.0
2013-11-09T19:12:20.967Z
found this question by gowers somewhat similar [are there super poly formula bounds & is formula size similar to circuit size](http://gowers.tiddlyspace.com/#%5B%5BCan%20we%20prove%20a%20superpolynomial%20lower%20bound%20for%20formula%20complexity%3F%5D%5D%20%5B%5BIs%20formula%20complexity%20comparable%20to%20circuit%20complexity%3F%5D%5D%20%5B%5BIs%20there%20a%20useful%20formal%20complexity%20measure%3F%5D%5D%20GettingStarted%20%5B%5BIs%20there%20an%20efficient%20Ramsey%20lift%20for%20the%20parity%20function%3F%5D%5D)
vzn
<cc.complexity-theory><graph-theory><lower-bounds><p-vs-np><circuits>
P/poly vs NP separation based on circuit trees instead of DAGs
vzn
# P/poly vs NP separation based on circuit trees instead of DAGs

(Asked by: username_0 on 2013-11-01)

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](https://cstheory.stackexchange.com/questions/4867/complexity-of-converting-a-boolean-circuit-to-a-boolean-formula)

**Tags:** cc.complexity-theory, graph-theory, lower-bounds, p-vs-np, circuits

> **Comments:**
> **username_1**: your example is a bit odd: you are saying that the existence of a small-size formula for some problem would imply a class separation.  but usually such a thing implies a collapse. do you have something in mind?  
> **username_0**: oops messed up the order of NP $\not\subset$ P/poly, edited that. as to your question that is reminiscent of this other question [proving lower bounds by proving upper bounds](http://cstheory.stackexchange.com/questions/3229/proving-lower-bounds-by-proving-upper-bounds)  
> **username_0**: found this question by gowers somewhat similar [are there super poly formula bounds & is formula size similar to circuit size](http://gowers.tiddlyspace.com/#%5B%5BCan%20we%20prove%20a%20superpolynomial%20lower%20bound%20for%20formula%20complexity%3F%5D%5D%20%5B%5BIs%20formula%20complexity%20comparable%20to%20circuit%20complexity%3F%5D%5D%20%5B%5BIs%20there%20a%20useful%20formal%20complexity%20measure%3F%5D%5D%20GettingStarted%20%5B%5BIs%20there%20an%20efficient%20Ramsey%20lift%20for%20the%20parity%20function%3F%5D%5D)  

---

## 2 answers

### Answer by username_2 on 2013-11-02. Score: 7 | Accepted answer

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](http://theory.cs.uchicago.edu/abstract.php?id=rossman) 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.

> **Comments:**
> **username_0**: thx! reviewing your notes, [monotone circuits](http://www.thi.informatik.uni-frankfurt.de/Seminare/SS12/monotone-circuits.pdf); do you think thm9.17, 9.18, or 9.25 (which are close to an answer to the question) could be strong enough for any P/poly$\stackrel{?}{=}$NP result, or not?  
> **username_2**: @username_0: The answer is "most probably - NO, unless we extend the arguments to work under the presence of "auxiliary variables". The thms you mentioned are just Razborov's approximation argument "in disguise" (a "symmetric version"). And he has **proved** [here](http://people.cs.uchicago.edu/~razborov/files/approx.pdf) what we need to get it work in non-monotone case. People trying to extend his argument to non-monotone circuits should carefully read this paper to avoid disappointments.  
> **username_0**: was thinking along those lines & thought you might say that! yes, have heard of that paper yet strangely, there is almost/nearly no reaction to it or further analysis/commentary on it by anyone [incl your own highly/deeply comprehensive book!], eg in stark contrast to Natural Proofs [which _also_ does not mention it]. so if it really is a significant "barrier" its an extremely _low-profile_ one... & yet it has been proven that superpoly monotone lower bounds on slice functions are sufficient to separate P/poly from NP (and razborov has apparently never written _anything_ on slice fns...?)  
> **username_0**: thx for ref, Rossman has now archived his paper at ECCC. [Formulas vs. Circuits for Small Distance Connectivity](http://eccc.hpi-web.de/report/2013/169/)  

---

### Answer by username_1 on 2013-11-01. Score: 8

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}}$.

> **Comments:**
> **username_0**: +1 thx/helpful but am looking for a P/poly vs NP thm related to trees/formulas (ie higher/above P complexity)  
> **username_1**: what I am saying is that problems decidable by polysize formulas might be (and I think are believed to be) a proper subset of P/poly. so a separation between polysize formulas and NP is not known to imply anything about P/poly vs. NP.  
> **username_0**: interested in any ref related to polysize formulas $\subsetneq$ P/poly. also, edited question somewhat.  
> **username_3**: @username_0: Evidence that L is a strict subset of P can also be taken as evidence that NC^1 (=poly formula size) is a strict subset of P/poly. See this related question: http://cstheory.stackexchange.com/questions/19315/what-are-the-compelling-reasons-for-believing-l-neq-p  
> **username_2**: The separations between *monotone* versions of $\mathsf{NC}^1/\mathsf{poly}$ and $\mathsf{P/poly}$ are long known (Karchmer-Wigderson, Grigni-Sipser, etc), but in the *non-monotone* world almost nothing was known. Fortunately, Ben Rossman [has recently found](http://theory.cs.uchicago.edu/abstract.php?id=rossman) the first separation of formulas vs. circuits in the *bounded depth* setting.  
> **username_1**: @username_2 your comment looks like it could be an answer?  

---

