COMP 596

Propositional Proof Complexity

Name: Robert Robere
Email: robere AT cs DOT mcgill DOT ca
When: Tuesday, Thursday from 10:05am-11:25am
Where: MDHAR G-01


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:

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.