Abstract

Recently several works have observed an exceptionally strong type of tradeoff — known as a supercritical tradeoff — in which one parameter is pushed beyond worst-case when another is restricted. In this talk, I will describe how to obtain a supercritical tradeoff between two natural parameters of proofs in (DNF) Resolution and Cutting Planes: *size* and *depth*. These proof systems capture the behaviour of popular SAT and integer programming algorithms respectively; the size of proofs corresponds to the runtime of the algorithms and depth corresponds to parallelizability. Thus, this result can be understood as giving a family of formulas for which any short computation must be highly sequential. In describing the proof, I will sketch a simplified proof of a supercritical depth/width tradeoff due to Razborov, which is at the heart of our result. (This is joint work with Robert Robere and Toniann Pitassi.)

Attachment