[Proof Complexity] Dmitry Itsykson seminar on Monday

[thapen]

Dear colleagues,

Dmitry Itsykson will give a proof complexity talk in our online logic 
seminar on Monday, at 15:30 Prague time - see 
https://calendar.math.cas.cz/content/proof-complexity-natural-formulas-communication-arguments

To join go to
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

Best,

Neil

---

Speaker: Dmitry Itsykson, Steklov Institute of Mathematics in 
St.Petersburg

Title: 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/.