General information

Proof complexity, naturally, studies proofs and its fundamental question, which is related to some of the most important questions in computer science, is the following:

Given a true statement A, how long is the shortest proof that A is true?

Proof complexity also analyzes methods for finding short proofs if they exist. Since, for example, the statement A could be "This code is bug-free" or "No solution to these constraints has value better than K", proof complexity has applications to many areas of computer science, including optimization and formal verification among others.

Proof complexity also gives us tools to analyze the power and limitations of entire classes of algorithms. For example:

• modern SAT solvers that are at the heart of much of the current work in formal methods in PL/SE can be understood in terms of resolution proofs.
• semi-definite programming based on sum-of-squares proofs is the best algorithm we know for solving large classes of optimization problems. In this case, the mere existence of a short proof that there is a solution is already enough to guarantee that there is a good algorithm to find that solution.

As hinted at by these examples, part of proof complexity involves understanding the best methods for expressing and checking proofs which include methods other than logic, such as polynomial equations, or integer inequalities.

The past decade has seen major progress in proof complexity and new applications, with many open problems resolved and many more now ready for attack. This course will give an introduction to modern proof complexity that will cover the classics in the field, as well as many of the most exciting recent developments. Throughout, we will focus on the applications of proof complexity and its many open problems.

Logistics

• Instructor: Paul Beame
• Time and Lectures link: Mondays and Wednesdays, beginning Sept 30, 2020 at 3:00-4:20 pm on Zoom.
• Work: short easy exercises to keep everyone following along, class participation, a final presentation from a selected list of papers/topics.

Resources

There is no single text that covers this material at the right level so we have detailed course notes. These cover somewhat more material than we will be able to go over in class.

• Course Notes

For some of the recent material involving sum-of-squares proofs, and semi-algebraic algebraic proofs more generally, we will use the recent monograph:

• Fleming, Kothari, Pitassi: Semialgebraic Proofs and Efficient Algorithms

Survey talks:

• The Limits of Proof

• A Tutorial Introduction to Proof Complexity

Surveys of Proof Complexity

• 2020 Buss, Nordström: Current draft: Proof Complexity and SAT Solving. In preparation. To appear in the 2nd edition of the Handbook of Satisfiability, edited by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh.

• 2012 Buss: Towards NP-P via Proof Complexity and Search

• 2007 Segerlind: The Complexity of Propositional Proofs

• 1999 Beame, Pitassi: Propositional Proof Complexity: Past, Present, and Future

• 1995 Urquhart: The Complexity of Propositional Proofs