אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

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 Tcc(k,c) that operates with proof lines that can be computed by k-party randomized communication protocol using at most c bits of communication [Göös, Pitassi, 2014]. All known lower bounds on Search(ϕ) (e.g. [Impagliazzo, Pitassi, Urquhart, 1994]; [Beame, Pitassi, Segerlind, 2007]; [Göös, Pitassi, 2014], ) 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 [Itsykson, Sokolov, 2014]. 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 [Itsykson, 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 the 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 2n/2k – 3k/2) lower bound on the randomized k-party communication complexity of Search BPHPM2n w.r.t. to some natural partition of the variables, where BPHPM2n 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 BPHP2n+12n superpolynomially separates tree-like Th(log1-ε m) from tree-like Th(log m), where m is the number of variables in the refuted formula. The talk is based on joint work with Dmitry Itsykson.