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.