The Taub Faculty of Computer Science Events and Talks

Proof complexity started its life as an attempt to prove that NP is different from coNP.

The main goal of the area is to show that no proof system can prove that all negative instances of 3SAT are unsatisfiable using polynomial size proofs.

However, this goal has proved too difficult, and nowadays the area concentrates on proving the same for specific proof systems.

The focus of this talk is the proof system *cutting planes*, which is the proof complexity analog of the popular branch-and-bound algorithm for integer programming. A proof in this system consists of a sequence of inequalities over Boolean variables. We will describe a pair of such inequalities (encoding an unsatisfiable subset sum instance) that have no common Boolean solutions, but proving this in cutting planes requires a proof of exponential size.

No familiarity with proof complexity will be assumed.

Joint work with Pavel Hrubes and Massimo Lauria.