Resolution lower bounds for perfect matching principles

For an arbitrary hypergraph H let PM(H) be the propositional formula asserting that H contains a perfect matching. We show that every resolution refutation of PM(H) must have size exp((Ω(δ(H)/λ(H)r(H)(log n(H))(r(H)+log n(H)))), where n(H) is the number of vertices, δ(H) is the minimal degree of a vertex, r(H) is the maximal size of an edge, and λ(H) is the maximal number of edges incident to two different vertices. For ordinary graphs G our general bound considerably simplifies to exp (Ω(δ(G)/(log n(G))²))). As a direct corollary, every resolution proof of the functional onto a version of the pigeonhole principle onto - FPHP_n^m must have size exp (Ω(n/(log m)²)) (which becomes exp (Ω(n^1/3)) when the number of pigeons m is unbounded). This in turn immediately implies an exp(Ω(t/n³)) lower bound on the size of resolution proofs of the principle circuit_t (f_n) asserting that the circuit size of the Boolean function f_n in n variables is greater than t. In particular resolution does not possess efficient proofs of NP ≡ P/poly. These results relativize, in a natural way, to more general principle M(U|H) asserting that H contains a matching covering all vertices in U ⊆ V(H)