Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle

  • Kazuo Iwama
  • Shuichi Miyazaki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1741)


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.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Beame and T. Pitassi, “Simplified and improved resolution lower bounds”, Proc. FOCS’96, pp. 274–282, 1996.Google Scholar
  2. 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
  3. 3.
    S. Buss, “Polynomial size proofs of the propositional pigeonhole principle”, Journal of Symbolic Logic, 52, pp. 916–927, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    S. Buss and T. Pitassi, “Resolution and the weak pigeonhole principle”, Proc. CSL’97, LNCS 1414, pp.149–156, 1997.Google Scholar
  5. 5.
    S. A. Cook and R. A. Reckhow, “The relative efficiency of propositional proof systems”, J. Symbolic Logic, 44(1), pp. 36–50, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    A. Haken, “The intractability of resolution”, Theoretical Computer Science, 39, pp. 297–308, 1985.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    P. Purdom, “A survey of average time analysis of satisfiability algorithms”, Journal of Information Processing, 13(4), pp.449–455, 1990.zbMATHGoogle Scholar
  8. 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
  9. 9.
    A. Urquhart, “The complexity of propositional proofs”, The Bulletin of Symbolic Logic, Vol. 1, No. 4, pp. 425–467, 1995.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Kazuo Iwama
    • 1
  • Shuichi Miyazaki
    • 1
  1. 1.School of InformaticsKyoto UniversityKyotoJapan

Personalised recommendations