Resolution lower bounds for the weak pigeon hole principle
Ran Raz · Journal of the ACM · 2002
(MATH) We prove that any Resolution proof for the weak pigeon hole principle, with n holes and any number of pigeons, is of length ω(2nε), (for some constant ε ρ 0). One corollary is that a certain propositional formulation of the statement NP ot \subset P/poly does not have short Resolution proofs.