Mladen Miksa: From degree to space and back: A journey through algebraic proofs

Lunch is served at 12:00 noon (register at doodle.com/4ehdxtpdcdys2heh by Sunday Dec 8). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

Abstract

Have you ever run a SAT solver on your favourite problem just to realize too late that going cheap on RAM was a bad idea and that the solver won't be able to find a solution? Attending this talk might help you understand better your SAT solver's needs.

In order to theoretically study a SAT solver, we model the reasoning that goes on inside the solver by a corresponding proof system and map different resources of the SAT solver to corresponding complexity measures of the proof system. Thus, we map the running time of a SAT solver to the size of the proof in the proof system, while the memory consumption is mapped to space. In the talk, we focus on the space measure in the algebraic proof system polynomial calculus, which is still poorly understood compared to resolution (the basis of most state-of-the-art SAT solvers).

One of the most important results for our understanding of space in resolution was given by Atserias and Dalmau in 2003, in which they showed a relation between space and resolution width, another very useful complexity measure. As we can generalize resolution width to polynomial calculus degree, a natural question that arises is whether a similar relation to the one given by Atserias and Dalmau holds for polynomial calculus space and degree? In this talk we discuss some partial results towards answering that question.

This talk is based on the paper "Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds", which is a joint work with Yuval Filmus, Massimo Lauria, Jakob Nordström, and Marc Vinyals, and which was presented at ICALP 2013.