Marc Vinyals: Marc VinyalsSpace in proof complexity
Time: Mon 2016-11-28 12.00
Location: Room 4523, Lindstedtsvägen 5, KTH CSC
Participating: Marc Vinyals, Theory Group, KTH
PRACTICALITIES
Lunch is served at 12:00 noon (register at this doodle at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for 1½-2 hours of more technical discussions.
ABSTRACT
Space in proof complexity measures the amount of memory that a verifier needs to check a proof, which imposes a lower bound on the memory a SAT solver needs to generate a proof. Space is very well understood for the most common proof system, resolution, but less so in other proof systems. In this talk we will survey some recent results about space in other settings: stronger proof systems such as polynomial calculus and cutting planes on the one hand, and a weaker "CDCL" proof system that is closer to the actual capabilities of SAT-solving algorithms on the other hand. We will even explore alternative definitions of space. The proof techniques will lead us to discussing adjacent areas of computational complexity such as pebble games and communication complexity.
The first part of this seminar (during the lunch hour) will also double as Marc's 80% seminar, where he outlines his PhD thesis to be defended in mid-2017.