Logic seminar

Proof complexity of natural formulas via communication arguments

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-party communication complexity of Search(BPHP) w.r.t. to some natural partition of the variables, where BPHP is the bit pigeonhole principle. In particular, this lower bound 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.

 

The talk is based on the joint work with Artur Riazanov that is available as ECCC report https://eccc.weizmann.ac.il/report/2020/184/.