[Proof Complexity] Dmitry Itsykson seminar on Monday
thapen
thapen at math.cas.cz
Fri Mar 12 09:45:53 CET 2021
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/.
More information about the Proof-Complexity
mailing list