Cutting Planes Proofs of Tseitin and Random Formulas

Proof Complexity studies the length of proofs of propositional tautologies in various restricted proof systems. One of the most well-studied is the Cutting Planes proof system, which captures reasoning which can be expressed using linear inequalities. A series of papers proved lower bounds on the length of Cutting Planes using the method of feasible interpolation whereby proving lower bounds on the size of Cutting Planes lower bounds proofs of a certain restricted class of formulas is reduced to monotone circuit lower bounds. However, it was not known how to obtain lower bounds for more natural formulas such as the Tseitin (mod 2) formulas or random formulas. In this talk I will discuss two recent results for Cutting Planes. The first is joint work together with Pankratov, Pitassi, and Robere (and proved independently by Hrubeš and Pudlak) which proves exponential lower bounds on the length of Cutting Planes proofs of random Θ(log n)-CNF formulas. The second is a surprising result of Dadush and Tiwari which gives quasi-polynomial size Cutting Planes proofs of the Tseitin tautologies. My aim is to highlight the main conceptual ideas in the proofs of both of these results.