Massimo Lauria: Optimality of size-degree tradeoffs for polynomial calculus

Please register for a light lunch at  doodle.com/fbwv7rpieu86ckd4  no later than Sunday 6 pm.

Abstract

Polynomial calculus is a way of refuting unsatisfiable CNF formulas by translating them to polynomials and proving that these polynomials have no common root. To show lower bounds on the size of such proofs, one usually proves strong lower bounds on degree, and then uses a general size-degree trade-off theorem saying that very high degree implies very high size.

There is an annoying gap in this theorem, however, in that fairly high degree, up to sqrt(n), cannot be proven to say anything about size. A natural question is whether this is inherent or whether the theorem could be strengthened so that somewhat strong degree lower bounds would yield somewhat strong size lower bounds.

We rule out this possibility by proving that the size-degree trade-off in its current form is essentially optimal. We do so by studying formulas encoding properties of linear orderings, which are known to have small proofs, and showing that these formulas require sqrt(n) degree.

Joint work with Nicola Galesi.

Format of lunch seminar + reading group

The lunch seminar + reading group meetings are intended to run for a total of 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 not to return after the break. No questions asked.