<p>The same distinction exists in circuit complexity: tree-like circuits are known as <em>formulas</em>, and it is easier to prove lower bounds for them. For example, there are no superlinear lower bounds for circuits (for explicit functions), but for formulas there is an $\tilde\Omega(n^3)$ average-case <a href="http://eccc.hpi-web.de/report/2013/058/">lower bound</a>, proved recently by Komargodski, Raz and Tal, extending an <a href="http://www.csc.kth.se/~johanh/shrinkgeneral.pdf">old result</a> of Håstad.</p>

CC BY-SA 3.0
2014-01-24T21:16:28.797Z
yeah of course DAG/trees in circuits, thats why pointed it out as a potential "bridge" between circuits and SAT resolution proof theory. there are exponential lower bounds proven in the latter (eg with pigeonhole problems etc as in the paper) but not (much) in the former.
vzn
CC BY-SA 3.0
2014-01-24T21:13:23.923Z
2014-01-24T21:13:23.923Z
Yuval Filmus
<p>hi all there seems to be a deep/not-much-explored phenomenon in the way that SAT resolution proofs can define a tree and/or a DAG &amp; its relationship to lower bounds/circuit complexity. could there be something very significant here? here is a 1999 paper by Iwama, Miyazaki that describes this phenomenon: <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.9531" rel="nofollow noreferrer">Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle</a>. from abstract:</p>

<blockquote>
  <p>Our main result shows that a shortest proof size of tree-like resolution for the pigeonhole principle is superpolynomially larger than that of DAG-like resolution. In the proof of a lower bound, we exploit a relationship between tree-like resolution and backtracking, which has long been recognized in this field but not been used before to give explicit results.</p>
</blockquote>

<p>this seems very significant in that at heart, circuits are all about DAGs, and have long conjectured there may be a link here such that circuits might be defined by the trees or DAGs that occur in SAT resolution proofs. however, there is only a single binary-like operation in resolution proofs, so that is one challenge,[4] whereas in circuits at the minimum there are usually two, AND/OR with monotone circuits, although the single XOR operation is functionally complete.[1] the dichotomy of trees vs DAGs seems also a big theme arising in complexity theory.[2,3]</p>

<p>anyway, my question:</p>

<blockquote>
  <p>are there new results/directions in this area/line of research? something that builds on it or considers something similar?</p>
</blockquote>

<p>this is more a big-picture question and am not looking for strictly identical methods etc. and not all answers need have refs.</p>

<p>[1] <a href="https://cstheory.stackexchange.com/questions/10396/0-1-vector-xor-problem">(0,1)-vector XOR problem</a> tcs.se<br>
[2]  <a href="https://cstheory.stackexchange.com/questions/19621/p-poly-vs-np-separation-based-on-circuit-trees-instead-of-dags">P/poly vs NP separation based on circuit trees instead of DAGs</a> tcs.se<br>
[3] <a href="https://cs.stackexchange.com/questions/9940/formulas-vs-circuits">formulas vs circuits</a> cs.se<br>
[4] <a href="https://cs.stackexchange.com/questions/9211/building-functionally-complete-boolean-circuits-out-of-trinary-logic">building circuits out of trinary logic</a> cs.se<br>
[5] <a href="https://cstheory.stackexchange.com/questions/16500/in-sat-resolution-proofs-are-all-dags-possible?rq=1">in SAT resolution proofs, are all DAGs possible?</a> tcs.se</p>

CC BY-SA 3.0
2014-01-24T20:22:45.657Z
Even the simple diamond DAG lies outside the space of transformation functions on n elements, which in general are directed trees that feed into cycles if you draw their monogenic inclusion relation.
Chad Brewbaker
<reference-request><graph-theory><circuit-complexity><big-picture><resolution>
"tree-like" vs "DAG-like" resolution
vzn
# "tree-like" vs "DAG-like" resolution

(Asked by: username_0 on 2014-01-24)

hi all there seems to be a deep/not-much-explored phenomenon in the way that SAT resolution proofs can define a tree and/or a DAG & its relationship to lower bounds/circuit complexity. could there be something very significant here? here is a 1999 paper by Iwama, Miyazaki that describes this phenomenon: [Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.9531). from abstract:

> Our main result shows that a shortest proof size of tree-like resolution for the pigeonhole principle is superpolynomially larger than that of DAG-like resolution. In the proof of a lower bound, we exploit a relationship between tree-like resolution and backtracking, which has long been recognized in this field but not been used before to give explicit results.

this seems very significant in that at heart, circuits are all about DAGs, and have long conjectured there may be a link here such that circuits might be defined by the trees or DAGs that occur in SAT resolution proofs. however, there is only a single binary-like operation in resolution proofs, so that is one challenge,[4] whereas in circuits at the minimum there are usually two, AND/OR with monotone circuits, although the single XOR operation is functionally complete.[1] the dichotomy of trees vs DAGs seems also a big theme arising in complexity theory.[2,3]

anyway, my question:

> are there new results/directions in this area/line of research? something that builds on it or considers something similar?

this is more a big-picture question and am not looking for strictly identical methods etc. and not all answers need have refs.

[1] [(0,1)-vector XOR problem](https://cstheory.stackexchange.com/questions/10396/0-1-vector-xor-problem) tcs.se  
[2] [P/poly vs NP separation based on circuit trees instead of DAGs](https://cstheory.stackexchange.com/questions/19621/p-poly-vs-np-separation-based-on-circuit-trees-instead-of-dags) tcs.se  
[3] [formulas vs circuits](https://cs.stackexchange.com/questions/9940/formulas-vs-circuits) cs.se  
[4] [building circuits out of trinary logic](https://cs.stackexchange.com/questions/9211/building-functionally-complete-boolean-circuits-out-of-trinary-logic) cs.se  
[5] [in SAT resolution proofs, are all DAGs possible?](https://cstheory.stackexchange.com/questions/16500/in-sat-resolution-proofs-are-all-dags-possible?rq=1) tcs.se

**Tags:** reference-request, graph-theory, circuit-complexity, big-picture, resolution

> **Comments:**
> **username_1**: Even the simple diamond DAG lies outside the space of transformation functions on n elements, which in general are directed trees that feed into cycles if you draw their monogenic inclusion relation.  

---

## 1 answers

### Answer by username_2 on 2014-01-24. Score: 7

The same distinction exists in circuit complexity: tree-like circuits are known as *formulas*, and it is easier to prove lower bounds for them. For example, there are no superlinear lower bounds for circuits (for explicit functions), but for formulas there is an $\tilde\Omega(n^3)$ average-case [lower bound](http://eccc.hpi-web.de/report/2013/058/), proved recently by Komargodski, Raz and Tal, extending an [old result](http://www.csc.kth.se/~johanh/shrinkgeneral.pdf) of Håstad.

> **Comments:**
> **username_0**: yeah of course DAG/trees in circuits, thats why pointed it out as a potential "bridge" between circuits and SAT resolution proof theory. there are exponential lower bounds proven in the latter (eg with pigeonhole problems etc as in the paper) but not (much) in the former.  

---

