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.
[1] (0,1)-vector XOR problem tcs.se
[2] P/poly vs NP separation based on circuit trees instead of DAGs tcs.se
[3] formulas vs circuits cs.se
[4] building circuits out of trinary logic cs.se
[5] in SAT resolution proofs, are all DAGs possible? tcs.se
