Resolution width-size trade-offs for the Pigeon-Hole Principle

We prove the following two results: (1) There is a resolution proof of the Weak Pigeon-Hole Principle, WPHP_n^mof size 2^{O([n log n/log m]+log m)} for any number of pigeons m and any number of holes n. (2) Any resolution proof of WPHP_n ^m of width (1/16 - ε) n² has to be of size 2 ^Ω(n), independently from m.. These results give not only a resolution size-width tradeoff for the Weak Pigeon-Hole Principle, but also almost optimal such trade-off for resolution in general. The upper bound (1) may be of independent interest, as it has been known for the two extreme values of m, m = n + 1 and in = 2^{√(n log n)}, only