CSAIL Event Calendar: Previous Series

Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions

Speaker: Jakob Nordstrom , MIT
Date: April 20 2010
Time: 4:15PM to 5:15PM
Location: 32-155
Host: Scott Aaronson, CSAIL, MIT

In recent years, deciding if a CNF formula is satisfiable has gone from a theoretical question to a practical approach for solving real-world problems. For current state-of-the-art satisfiability algorithms, typically based on resolution and clause learning, the two main bottlenecks are the amounts of time and memory space used. Understanding time and memory consumption of SAT-solvers, and how these resources are related to one another, is therefore a question of great interest.

Roughly a decade ago, it was asked whether proof complexity had anything intelligent to say about this question, corresponding to the interplay between size and space of proofs. In this talk, I will explain how this question can be answered almost completely by combining two tools, namely good old pebble games on graphs, studied extensively in the 70s and 80s, and a new, somewhat surprising, theorem showing how weak space lower bounds can be amplified to strong bounds simply by making variable substitutions in the corresponding CNF formulas.

Joint work with Eli Ben-Sasson.

See other events that are part of Theory Colloquium 2009/2010

See other events happening in April 2010