Schedule

Date	Materials	Topics
September 30	Lecture 1.pdf	What is a proof? (Section 1.1) Proof complexity definition (Section 1.2) Resolution and equivalence of DPLL and Tree Resolution (Section 1.3)
October 5	Lecture 2.pdf	Ordered and Regular Resolution (Section 1.3) Tseitin formulas (Section 1.6) Frege proofs (Section 1.3) Extended Frege and Extended Resolution (Section 1.3) C-Frege proofs for circuit complexity class C (Section 1.3) Hierarchy of logical proof systems Nullstellensatz proofs (Section 1.4)
October 6	exercises1.pdf	- First exercises due Friday October 16 (submit via Canvas)
October 7	Lecture 3.pdf	Nullstellensatz proofs (Section 1.4) Dual variables (Section 1.4) Finding low degree Nullstellensatz proofs (Section 1.4) Polynomial Calculus (PC) proofs (Section 1.4) PCR, PC with dual variables, simulates resolution (Section 1.4) Finding low degree PC and PCR proofs (Section 1.4) Pigeonhole Principle (Section 1.6) Start of exponential lower bound for PHP in resolution (Section 2.1)
October 12	Lecture 4.pdf	Exponential lower bound for PHP in resolution (Section 2.1) Resolution width and conversion of small tree-like proofs to small width proofs (Section 2.2)
October 13	exercises2.pdf	- Exercise due Friday October 23 (submit via Canvas)
October 14	Lecture 5.pdf	Small size resolution proofs imply small width proofs (Section 2.2) Width-based resolution proof search for small size proofs (Section 2.2) Boundary expansion and lower bounds on resolution proof width (Section 2.3)
October 19	Lecture 6.pdf	Large bipartite expansion implies boundary expansion (Section 2.3) Random k-CNF formulas and their unsatisfiability threshold (Section 1.6) Random k-CNF formulas typically have large bipartite expansion (yielding resolution width and proof size lower bounds) (Section 2.4)
October 21	Lecture 7.pdf	More applications of width lower bounds for Resolution (Section 2.5) Alternative characterizations of subclasses of Resolution proofs (Section 2.6)
October 26	Lecture 8.pdf	Algebraic proofs non-clausal translations and low-degree Nullstellensatz proofs (Section 3.1) d-designs and degree lower bounds for Nullstellenstz proofs (Section 3.2) Degree lower bounds for Induction Principle and Pebbling formulas (Section 3.2) Size-degree relationship for PC and PCR proofs (Section 3.3) Gaussian width (Section 3.4)
October 28	Lecture 9.pdf	Gaussian Width (Section 3.4) Polynomial Calculus over the ±1 basis and equivalence of degree with ordinary PC proofs (Section 3.4) Equivalence of zeroes of binomial polynomials over ±1 basis and mod-2 Gaussian equations (Section 3.4) PC refutations of binomials over &\plusmn;1 basis can always be binomial (Section 3.4) PC degree of refutations of binomials is at least 1/2 Gaussian width (Section 3.4) PC degree and PCR size lower bounds for Tseitin formulas (Section 3.4) PC degree and PCR size lower bounds for random k-CNF formulas (Section 3.4)
November 1	exercises3.pdf	- Exercises due Friday November 13 (submit via Canvas)
November 2	Lecture 10.pdf	Semi-Algebraic proof systems (Section 1.5) Cutting Planes (Section 1.5) Cutting Planes efficiently simulates Resolution (Section 1.5) Efficient Cutting Planes proofs of Pigeonhole formulas (Section 1.6)
November 4	Lecture 11.pdf	CDCL solvers (and relationship with resolution) (Section 1.3)
November 9	Lecture 12.pdf	Pseudo-Boolean solvers and Cutting Planes implementation (Section 1.5) Sherali-Adams proofs (Section 1.5)
November 16	Lecture 13.pdf	Sherali-Adams proofs review (Section 1.5) Sherali-Adams simulates resolution (Section 1.5) Sum-of-Squares (SoS) proofs (Section 1.5) SoS proofs of the pigeonhole principle (Section 1.6) Sos simulates polynomial calculus over the reals (Section 1.5)
November 18	Lecture 14.pdf	Sum-of-Squares (SoS) proof search (Section 1.5) Relating Sherali-Adams and SoS to LP and SDP (Section 1.5) Intro to communication complexity (Section 4.1)
November 23	Lecture 15.pdf	Two-party and multiparty communication complexity (Section 4.1) Multiparty communication complexity of polynomial inequalities (Section 4.2) Tree-like proofs and communication complexity of Search_F (Section 4.2) Lower bounds for low degree tree-like proofs for Positivstellensat Calculus (and resolution and cutting planes) (Section 4.2)
November 25	Lecture 16.pdf	Resolution lower bound via feasible interpolation (Section 4.3) Cutting Planes lower bound via feasible interpolation (Section 4.3)
November 30	Lecture 17.pdf	Semantic Cutting Planes proofs and triangle DAGs (not yet in notes) Lifted formulas via Index gadget (not yet in notes) Lower bounds for semantic CP lifted from resolution width (not yet in notes) Pseudo-expectation definitions for Sherali-Adams and SoS (see Fleming, Kothari, Pitassi) Pseudo-expectations imply degree lower bounds for Sherali-Adams and SoS (see Fleming, Kothari, Pitassi)
December 1	exercises4.pdf	- Exercises due Friday December 18 (submit via Canvas)
December 2	Lecture 18.pdf	Pseudo-expectation for Sherali-Adams and LP solutions (see Fleming, Kothari, Pitassi) Pseudo-expectation for SoS and SDP solutions (see Fleming, Kothari, Pitassi) Ellipsoid algorithm for convex programming (see Flemining, Kothari, Pitassi) Degree 2 SoS and MAXCUT (see Fleming, Kothari, Pitassi) Unique Games Conjecture and degree 2 SoS for MAXCSP (see Fleming, Kothari, Pitassi) Pseudo-expectation for SoS over {+1,-1} variables (see Fleming, Kothari, Pitassi)
December 7	Lecture 19.pdf	Pseudo-expectations for linear constraints below Gaussian width (see Flemin, Kothari, Pitassi: Section 5.1) Linear SoS degree and exponential size lower bounds for random k-CNF, random k-XOR, Tseitin on expanders (see Fleming, Kothari, Pitassi: Section 5.2) Pseudo-expectation for Knapsack (see sumofsquares.org notes) Extension complexity for LP, SDP (see Fleming, Kothari, Pitassi) Lower bounds for LP, SDP extensions of MAXCSP in terms of SA and SoS degree (see Fleming, Kotheri, Pitassi)
December 9	Lecture 20.pdf	NP-hardness for finding sub-exponential approximation to optimal proof size for Resolution, Cutting Planes, NS, PC, SA, Regular resolution, Ordered Resolution. DRAT proof system and its use in practice to check complete SAT solvers. AC⁰-Frege proof lower bounds. Open problems.