Noah Fleming
University of Toronto

Random CNF formulas are hard to refute in Cutting Planes

Department of Computer Science
Friday, August 3, 2018, 12:00 pm, Room EN 2022

---

Abstract

Random SAT formulas form one of the most important testbeds of hard examples for AI and SAT algorithms. The conjectured hardness of certifying the unsatisfiability of random SAT formulas has been connected to many areas in theoretical computer science. In 1988, Chvátal and Szeméredi proved that for k>=3, with high probability, a randomly chosen k-CNF formula requires an
exponential number of lines to refute in Resolution. Since then, it has been an open problem to show the conjectured hardness of refuting a random formula.

This work makes progress towards resolving the question of refuting random k-CNF formulas for the Cutting Planes proof system. We prove that random O(log(n))-CNF formulas require an exponential number of lines to refute in Cutting Planes. This result was proved independently as well by Pudlak and Hrubeš.

I aim to make this talk self contained, although an understanding of NP-completeness will be useful. The first half of the talk will be an introduction to proof complexity, the study of short certificates of unsatisfiability, with a focus on the Cutting Planes proof system. In the second half, I will sketch how to obtain the lower bound on the length of Cutting Planes refutations of random
formulas, by proving an equivalence between strengthening of Cutting Planes proofs and monotone circuits.

The work presented here follows the paper Random Θ(log n)-CNFs are hard for Cutting Planes, and is joint work with Denis Pankratov, Toniann Pitassi, and Robert Robere.