Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Theory Seminar: An Instance of Subset Sum Hard for Cutting Planes (An Invitation to Proof Complexity)
event speaker icon
Yuval Filmus (CS, Technion)
event date icon
Wednesday, 02.12.2015, 12:30
event location icon
Taub 201
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.