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 sizeexpΩδ(H)λ(H)r(H)(logn(H))(r(H)+logn(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)(logn(G))2 (implying an exp(Ω(δ(G)1/3)) lower bound that depends on the minimal degree only). As a direct corollary, every resolution proof of the functional onto version of the pigeonhole principle onto−FPHPnm must have size expΩn(logm)2 (which becomes expΩ(n1/3) when the number of pigeons m is unbounded). This in turn immediately implies an exp(Ω(t/n3)) lower bound on the size of resolution proofs of the principle asserting that the circuit size of the Boolean function fn 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 a more general principle M(U|H) asserting that H contains a matching covering all vertices in U⊆V(H).