Proof Complexity of Natural Formulas via Communication Arguments.

A canonical communication problem Search (ϕ) is defined for every unsatisfiable CNF ϕ: an assignment to the variables of ϕ is partitioned among the communicating parties, they are to find a clause of ϕ falsified by this assignment. Lower bounds on the randomized k -party communication complexity of Search (ϕ) in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula ϕ in the semantic proof system T cc ( k , c ) that operates with proof lines that can be computed by k -party randomized communication protocol using at most c bits of communication [9]. All known lower bounds on Search (ϕ) (e.g. [1, 9, 13]) are realized on ad-hoc formulas ϕ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas. First, we demonstrate our approach for two-party communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over F 2 [14]. Let a formula PM G encode that a graph G has a perfect matching. If G has an odd number of vertices, then PM G has a tree-like Res(⊕)-refutation of a polynomial-size [14]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound 2 Ω( n ) on size of tree-like Res(⊕)-refutations of PM K n +2, n . Then we apply our approach for k -party communication complexity in the NOF model and obtain a [EQUATION] lower bound on the randomized k -party communication complexity of Search (BPHP M 2 n ) w.r.t. to some natural partition of the variables, where BPHP M 2 n is the bit pigeonhole principle and M = 2 n + 2 n (1--1/ k ) . In particular, our result implies that the bit pigeonhole requires exponential tree-like Th( k ) proofs, where Th( k ) is the semantic proof system operating with polynomial inequalities of degree at most k and k = O(log 1--ϵ n ) for some ϵ > 0. We also show that BPHP 2 n +1 2 n superpolynomially separates tree-like Th(log 1--ϵ m ) from tree-like Th(log m ), where m is the number of variables in the refuted formula.