Speaker: Jakob Nordstrom
Massachusetts Institute of Technology (MIT)
Title: Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions
Abstract: 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.