Understanding the Hardness of Proving Formulas in Propositional Logic

by Dr Jakob Nordström (KTH)

Tuesday 21 Feb 2012, 13:30 → 14:30 Europe/Stockholm

122:026

Proving formulas in propositional logic is a fundamental problem in computer science and mathematics. On the one hand, this problem is believed to be theoretically intractable in general, and deciding whether this is the case is one of the famous million dollar Millennium Problems. On the other hand, these days automated theorem provers, or so-called SAT-solvers, are routinely used to solve large-scale real-world applications of this problem with millions of variables. This is in contrast to that there are also known small example formulas with just hundreds of variables that causes even state-of-the-art SAT-solvers to stumble. What lies behind the spectacular success of SAT-solvers? And how can one determine whether a particular formula is hard or tractable? In this talk, we will discuss what the field of proof complexity has to say about these questions. In particular, we propose that the spacecomplexity of a formula could be a good measure of its hardness. We prove that this would have drastic implications for the impossibility of simultaneously optimizing time and memory consumption, the two main resources of SAT-solvers. Somewhat surprisingly, our results are obtained by relatively elementary means from combinatorial pebble games on graphs, studied extensively in the 70s and 80s. No prior knowledge of computational complexity theory or logic is assumed. This talk is partly based on joint work with Eli Ben-Sasson at the Technion in Haifa, Israel.