Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle
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.
Unable to display preview. Download preview PDF.
- 1.P. Beame and T. Pitassi, “Simplified and improved resolution lower bounds”, Proc. FOCS’96, pp. 274–282, 1996.Google Scholar
- 2.M. L. Bonet, J. L. Esteban, N. Galesi and J. Johannsen, “Exponential separations between restricted resolution and cutting planes proof systems”, Proc. FOCS’98, pp. 638–647, 1998.Google Scholar
- 4.S. Buss and T. Pitassi, “Resolution and the weak pigeonhole principle”, Proc. CSL’97, LNCS 1414, pp.149–156, 1997.Google Scholar
- 8.A. A. Razborov, A. Wigderson and A. Yao, “Read-Once Branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus”, Proc. STOC’97, pp. 739–748, 1997.Google Scholar