“tree-like” vs “DAG-like” resolution

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

• 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 Jan 24 '14 at 20:22

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, proved recently by Komargodski, Raz and Tal, extending an old result of Håstad.

• 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 Jan 24 '14 at 21:16