Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions
Speaker: Jakob Nordstrom , MITContact:
Date: April 20 2010
Time: 4:15PM to 5:15PM
Host: Scott Aaronson, CSAIL, MIT
Be Blackburn , 3-6098, firstname.lastname@example.orgRelevant URL:
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