Jakob Nordström:Understanding the Hardness of Proving Formulas in Propositional Logic

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 problem instances with millions of variables.

The field of proof complexity studies formal systems for reasoning about logic formulas. In this talk, we will survey some recent theoretical results on the resolution proof system, which is the basis for current state of-the-art SAT solvers, and discuss what these results might say about the potential and limitations of such solvers. Time permitting, we will also mention some intriguing open questions concerning related proof systems based on algebraic and geometric reasoning.

No prior knowledge of computational complexity theory is assumed. This talk is based on joint work with Eli Ben-Sasson at the Technion in Haifa, Israel.