Resolution lower bounds for the weak pigeonhole principle

Research output: Contribution to journalArticlepeer-review

38 Scopus citations


We prove that any Resolution proof for the weak pigeonhole principle, with n holes and any number of pigeons, is of length Ω2(2), (for some global constant ε > 0). One corollary is that a certain prepositional formulation of the statement NP ⊄ P/ poly does not have short Resolution proofs.

Original languageEnglish (US)
Pages (from-to)115-138
Number of pages24
JournalJournal of the ACM
Issue number2
StatePublished - Mar 2004
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence


  • Computational complexity
  • Lower bounds
  • P different than NP
  • Prepositional logic
  • Proof complexity

Cite this