A canonical communication problem Search(F) is defined for every unsatisfiable CNF F: an assignment to the variables of F is distributed among the communicating parties, they are to find a clause of F falsified by this assignment. Lower bounds on the communication complexity of Search(F) imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula F in a large class of proof systems. All known lower bounds on Search(F) are realized on ad-hoc formulas F (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 prove an exponential lower bound on the size of tree-like Res(+) refutations of the Perfect matching principle. Then we apply our approach to k-party communication complexity in the NOF model and obtain a lower bound on the randomized k-... more