Lecture Notes

• [Lecture 1] - Introduction
• [Lecture 2] - Propositional Proof Systems, Resolution (Definition, Completeness)
• [Lecture 3/4] - Resolution (Tree-Like, Complexity Measures, PHP Lower Bounds, Width-Size Relation)
• [Lecture 5] - Resolution (Width-Size Relation cont., Tseitin Formulas, Expander Graphs, Random k-CNFs)
• [Lecture 6] - Resolution (Automatizability/Automatability, Prover-Delayer Games)
• [Lecture 7] - Resolution (Prover-Delayer Games, Intro to SAT Algorithms)
• [Lecture 8] - Resolution (SAT Algorithms, PPSZ, CDCL, Relationship to Proofs)
• [Lecture 9] - Cutting Planes (Definitions, Division Rule, Upper Bounds for PHP)
• [Lecture 10] - Cutting Planes (Simulating Resolution, Start of Feasible Interpolation)
• [Lecture 11] - Cutting Planes (Feasible Interpolation for Resolution, The Karchmer-Wigderson Connection)
• [Lecture 12] - Cutting Planes (Feasible Interpolation for Cutting Planes)
• [Lecture 13] - Nullstellensatz (Algebraic Proof Systems, Polynomial Encodings, Nullstellensatz Definitions, Pebbling Formulas and Pebble Games)
• [Lecture 14] - Nullstellensatz (Nullstellensatz Proofs of Tseitin, History of Algebraic Proof Systems, Span Programs)
• [Lecture 15] - Polynomial Calculus, the Ideal Proof System
• [Lecture 16] - Sherali Adams (Introduction, Beginning of LP Connection)
• [Lecture 17] - Sherali Adams (Polyhedral and Probabilistic Interpretation)
• [Lecture 18] - Sherali Adams (Strong Completeness, Pseudo-Distributions)
• [Lecture 19] - Sherali Adams (Proof Systems and Polytopes, Integrality Gaps)
• [Lecture 20] - Sums of Squares (Definition, Comparison to Proof Systems, Short Proof of PHP)
• [Lecture 21] - Sums of Squares (SOS Pseudo-Expectations, Algorithmic Aspects, Analysis of Goemans-Williamson SDP for Max-Cut)

Papers for Project Presentations

Boolean Proof Systems (Resolution, Clause Learning, etc.)

• [Krajícek 97] Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• [Alekhnovich et al 99] Space Complexity in Propositional Calculus (Claimed!)
• [Bonet-Galesi 01] Optimality of size-width tradeoffs for resolution. (Claimed!)
• [Beame-Kautz-Sabharwal 04] Towards Understanding and Harnessing the Potential of Clause Learning
• [Razborov 16] A New Kind of Tradeoffs in Propositional Proof Complexity
• [Atserias-Mueller 19] Automating Resolution is NP-Hard (Partially Claimed, Open to Collaboration)

Algebraic Proof Systems (Nullstellensatz, PC, etc.)

• [Pudlák-Sgall 96] Algebraic models of computation and interpolation for algebraic proof systems
• [Buss et al 01] Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes
• [Alekhnovich-Razborov 03] Lower Bounds for Polynomial Calculus: Non-binomial case
• [Grochow-Pitassi 14] Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System
• [de Rezende et al 19] Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling (Claimed by me --- see talk at MIPT)

Semi-Algebraic Proof Systems (Cutting Planes, Sherali-Adams, SOS, etc.)

• [Pudlák 97] Lower bounds for resolution and cutting plane proofs and monotone computations
• [de la Vega-Mathieu 07] Linear Programming Relaxations of Maxcut (Claimed!)
• [Galesi-Pudlák-Thapen 14] The space complexity of cutting planes refutations (Claimed!)
• [Hopkins-Li 17] Mixture Models, Robustness, and Sum of Squares Proofs
• [Barak-Steurer 17] Sum-of-squares proofs and the quest toward optimal algorithms

Other Topics

• [Razborov-Rudich 97] Natural Proofs
• [Paturi-Pudlák-Zane 99] The Satisfiability Coding Lemma
• [Alekhnovich et al 08] The complexity of properly learning simple concept classes
• [Pudlák 09] Quantum deduction rules (Claimed!)
• [Pudlák-Thapen 19] Random resolution refutations (Claimed!)

Course Description

This course will start with the following basic question:

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

The study of this question belongs to the field of propositional proof complexity. Since proofs appear everywhere in computer science, proof complexity has many deep connections with some of our central open problems:

• In upper bounds, proof complexity forms the basis for the study of many fundamental algorithms used both in theory and in practice, such as: SAT solvers and Model Checking, Gröbner bases, Linear Programming, Cutting Planes and Branch-and-Bound solvers, and Semidefinite Programming/Sums of Squares. All of these algorithms are, fundamentally, proof search algorithms, which search for the shortest proof in some "weak" proof system.
• In lower bounds, proof complexity is profoundly connected to major open problems in complexity theory, such as proving circuit lower bounds, P vs. NP, and the Unique Games Conjecture.

Furthermore, the past decade has seen an immense amount of progress in proof complexity, with many open problems resolved and many more now ripe for attack.

This course is intended to serve as an introduction to modern proof complexity, emphasizing its connections with computational complexity and algorithms in optimization. We will study some of the central proof systems that occur in theory and in practice, showing how proofs in each of the systems are intimately tied with fundamental algorithms in optimization, and with proving lower bounds in certain computational models. Throughout we will also survey many open problems. We will (hopefully!) get to look at (all of) the following topics:

- Introduction to Proof Complexity

Propositional Proof Systems and NP vs. coNP. Proof search (i.e. Automatability), and Feasible Interpolation. Canonical propositional tautologies: the Pigeonhole Principle, Tseitin Formulas, Random k-CNFs, and others.

- Resolution, SAT Solvers, and Boolean Circuits.

Resolution proofs and some restrictions. Decision Trees. Introduction to Conflict-Driven Clause-Learning SAT solvers (CDCL). Lower bounds on Resolution proof length. Feasible interpolation and connections to Boolean circuit lower bounds via "lifting".

- Nullstellensatz and Polynomial Calculus, Gröbner Bases, and Span Programs.

Introduction to algebraic proof systems, Hilbert's Nullstellensatz, and Polynomial Calculus. Gröbner Bases algorithms. Lower bounds, Feasible Interpolation by Span Programs. Connections to Quantum Algorithms.

- Cutting Planes, Branch-and-Bound Solvers, Real Circuits.

Cutting Planes proofs. Branch-and-Bound solvers for Integer Programming and Stabbing Planes proofs. Feasible Interpolation by Monotone Real Circuits, Lower Bounds.

- Sherali-Adams, Linear Programming, and Extended Formulations.

Sherali-Adams proofs and Linear Programming for Optimization. Extended Formulations of Linear Programs. Lower bounds for Sherali-Adams proofs.

- Sums-of-Squares, Semidefinite Programming, and Semidefinite Extended Formulations.

Sums-of-Squares proofs and Hilbert's 17th Problem. Semidefinite programs for optimization and the Laserre Hierarchy. Lower bounds for Sums-of-Squares. Semidefinite Extended Formulations. Connections to machine learning: tensor decomposition, learning mixtures of Gaussians, and more.

Course Prerequisites

Mathematical maturity, particularly in discrete mathematics. An undergraduate course in theoretical computer science will be helpful (such as COMP 330). However, no specific background will be needed and the course will be essentially self-contained.

Marking Scheme

This course will not have exams. The final grade will be based on participation, assignments, and a final project. Given the current COVID-19 situation, I may or may not expect students to scribe lectures as well.

Final Project

As a final project, students will be asked to go "in-depth", read a paper close to the topics studied in class, and then give a presentation on it. The final project can be completed in pairs. If you like, you can find your own paper that you think is relevant and present on it! I will also give out a list of good potential papers closer to the fall.