[Proof Complexity] Seminar Mon May 10 at 14:00 CET with Noah Fleming: On the complexity of branch and cut

[Jakob Nordström]

Dear all,

As a follow-up to the seminar with Daniel Dadush just announced, on Monday May 10 at 14:00 CET we will have the pleasure of listening to a talk on quite a similar topic by Noah Fleming from the University of Toronto titled "On the complexity of branch and cut".

We will meet virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming video seminars can be found at http://www.csc.kth.se/~jakobn/videoseminars/ (an address that should change soonish, but for now it is what it is). If you do not wish to receive these announcements, or receive several copies of them, please send a message to jakob.nordstrom at cs.lth.se.

Best regards,
Jakob Nordström

**********

Monday May 10 at 14:00
On the Complexity of Branch and Cut
(Noah Fleming, University of Toronto)

The Stabbing Planes proof system was introduced to model practical branch-and-cut integer programming solvers. As a proof system, Stabbing Planes can be viewed as a simple generalization of DPLL to reason about linear inequalities. It is powerful enough to simulate Cutting Planes and produce short refutations of the Tseitin formulas — certain unsatisfiable systems of linear equations mod 2 — which are canonical hard examples for many algebraic proof systems. In a surprising recent result, Dadush and Tiwari showed that these short Stabbing Planes refutations of the Tseitin formulas could be translated into Cutting Planes proofs. This raises the question of whether all Stabbing Planes can be efficiently translated into Cutting Planes. In recent work, we give a partial answer to this question.

In this talk I will introduce and motivate the Stabbing Planes proof system. I will then show how Stabbing Planes proofs with quasi-polynomially bounded coefficients can be quasi-polynomially translated into Cutting Planes. As a consequence of this translation, we can show that Cutting Planes has quasi-polynomial size refutations of any unsatisfiable system of linear equations over a finite field. A remarkable property of our translation for systems of linear equations over finite fields, and the translation of Dadush and Tiwari for the Tseitin formulas, is that the resulting proofs are also quasi-polynomially deep. A natural question is thus whether these depth bounds can be improved. In the last part of the talk, I will discuss progress towards answering this question in the form of a new depth lower bound technique for Cutting Planes, which works also for the stronger semantic Cutting Planes system, and which allows us to establish the first linear lower bounds on the depth of semantic Cutting Planes refutations of the Tseitin formulas.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.csc.kth.se/~jakobn/ (webpages still in transit)