Abstract
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 kparty communication complexity of Search(φ) in the numberonforehead (NOF) model imply treesize lower bounds, rank lower bounds, and sizespace tradeoffs for the formula φ in the semantic proof system T^{cc}(k,c) that operates with proof lines that can be computed by kparty randomized communication protocol using at most c bits of communication [Göös and Pitassi, 2014]. All known lower bounds on Search(φ) (e.g. [Beame et al., 2007; Göös and Pitassi, 2014; Russell Impagliazzo et al., 1994]) are realized on adhoc 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 twoparty communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over 𝔽₂ [Dmitry Itsykson and Dmitry Sokolov, 2014]. 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 treelike Res(⊕)refutation of a polynomialsize [Dmitry Itsykson and Dmitry Sokolov, 2014]. 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 treelike Res(⊕)refutations of PM_{K_{n+2,n}}.
Then we apply our approach for kparty communication complexity in the NOF model and obtain a Ω(1/k 2^{n/2k  3k/2}) lower bound on the randomized kparty communication complexity of Search(BPHP^{M}_{2ⁿ}) w.r.t. to some natural partition of the variables, where BPHP^{M}_{2ⁿ} is the bit pigeonhole principle and M = 2ⁿ+2^{n(11/k)}. In particular, our result implies that the bit pigeonhole requires exponential treelike Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k and k = 𝒪(log^{1ε} n) for some ε > 0. We also show that BPHP^{2ⁿ+1}_{2ⁿ} superpolynomially separates treelike Th(log^{1ε} m) from treelike Th(log m), where m is the number of variables in the refuted formula.
BibTeX  Entry
@InProceedings{itsykson_et_al:LIPIcs.CCC.2021.3,
author = {Itsykson, Dmitry and Riazanov, Artur},
title = {{Proof Complexity of Natural Formulas via Communication Arguments}},
booktitle = {36th Computational Complexity Conference (CCC 2021)},
pages = {3:13:34},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771931},
ISSN = {18688969},
year = {2021},
volume = {200},
editor = {Kabanets, Valentine},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14277},
URN = {urn:nbn:de:0030drops142773},
doi = {10.4230/LIPIcs.CCC.2021.3},
annote = {Keywords: bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, treelike proofs}
}
Keywords: 

bit pigeonhole principle, disjointness, multiparty communication complexity, perfect matching, proof complexity, randomized communication complexity, Resolution over linear equations, treelike proofs 
Collection: 

36th Computational Complexity Conference (CCC 2021) 
Issue Date: 

2021 
Date of publication: 

08.07.2021 