Resolution lower bounds for the weak functional pigeonhole principle

摘要

We show that every resolution proof of the functional version FPHPnm of the pigeonhole principle (in which one pigeon may not split between several holes) must have size exp(Omega(n/(log m)(2))). This implies an exp(Omega(n(1/3))) bound when the number of pigeons m is arbitrary. (C) 2002 Elsevier Science B.V. All rights reserved. [References: 21]