Resolution lower bounds for the weak functional pigeonhole principle. (Q1401365)

The main result of the paper is that every resolution refutation of the functional version of the pigeonhole principle must have the size \(\exp (\Omega(n/(\log m)^2))\), where \(n\) is the number of the pigeons and \(m\) is the number of holes. This fact implies an \(\exp(\Omega(n^{1/3}))\) lower bound when the number of pigeons \(m\) is arbitrary. The paper contains an overview of some open problems.