期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-31
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：A canonical communication problem Search(ϕ) is defined for every unsatisfiable CNF ϕ: an assignment to the variables of ϕ is distributed 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 [GP14]. All known lower bounds on Search(ϕ) (e.g. [BPS07, GP14, IPU94]) 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 F2 [IS14]. Let a formula PMG encode that a graph G has a perfect matching. If G has an odd number of vertices, then PMG has a tree-like Res(⊕)-refutation of a polynomial-size [IS14]. 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 PMKn 2,n . Then we apply our approach for k-party communication complexity in the NOF model and obtain a Ω 1 k 2 n/2k−3k/2 lower bound on the randomized k-party communication complexity of Search BPHPM 2n w.r.t. to some natural partition of the variables, where BPHPM 2n is the bit pigeonhole principle and M = 2n 2n(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(log1− n) for some > 0. We also show that BPHP2 n 1 2n superpolynomially separates tree-like Th(log1− m) from tree-like Th(log m), where m is the number of variables in the refuted formula.
