Short Proofs Are Narrow (Well, Sort of), But Are They Tight?

by Dr Jakob Nordström (KTH)

Tuesday 27 Nov 2007, 15:00 → 16:00 Europe/Stockholm

Roslagstullsbacken 35

Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The main bottleneck for such algorithms, other than the obvious one of time, is the amount of memory used. In the field of proof complexity, the resources of time and memory correspond to the length and space of resolution proofs. There has been a long line of research trying to understand these proof complexity measures, as well as relating them to the width of proofs, i.e., the size of a largest clause, which has proven to be intimately connected with both length and space. While strong results have been proven for length and width, unfortunately our understanding of space is still quite poor. In this talk, we will try to give an overview of proof complexity and resolution, and present some of the key results relating length, width and space. Time permitting, we will also try to describe a very recent result in this area, which is joint work with Johan Håstad.