On the Virtue of Succinct Proofs: Amplifying Communication Complexity Hardness to Time-Space Trade-offs in Proof Complexity

Theory Reading group

Please register for a light lunch at
doodle.com/kuwgqtbn4imagqnb?lt=4  no later than Sunday evening at 6
pm.

Abstract

Motivated by the satisfiability problem and SAT solving, the last decade
has seen active research into time-space trade-offs in proof systems for
propositional logic. So far most of the research has focused on the
resolution proof system operating with CNF formulas, whereas stronger
systems using algebraic and geometric methods of reasoning have remained
beyond reach.

In this work, we report the first trade-off results for algebraic and
geometric proof systems. Our results are obtained by combining
combinatorial pebble games, extensively studied in the 1970s and 1980s,
with recently developed tools in communication complexity based on
information theory.

No prior knowledge of proof complexity or communication complexity will be
assumed.

This talk presents joint work with Trinh Huynh published in STOC '12.

Format of the reading group

The reading group meetings are intended to run for 3 hours plus minus,
during which time we will have the possibility to first get an overview of
some interesting research results and then study them in some depth.

We start at noon with a light lunch, and as soon as people are seated
there is a presentation for 45-60 minutes. This should be an accessible
talk, not requiring any particular prerequisites. Then there is a short
break. Up to this point the whole exercise should be pretty much
indistinguishable from a regular (lunch) seminar.

After the break, we return for ca two hours of more technical discussions.
Now we open up the hood, look at the formal definitions, and prove at
least some of the key ingredients in the results including all the gory
technical details glossed over in a polished seminar presentation. This
part will typically be on the board, and should hopefully be very
interactive.

However, for those who feel that the first one-hour regular seminar was
enough for today, it is perfectly fine to just discretely drop out during
the break. No questions asked.