[Proof Complexity] Seminar Fri Apr 23 at 14:00 CET with Daniel Dadush: On the complexity of branching proofs

Jakob Nordström jakob.nordstrom at cs.lth.se
Sat Apr 17 18:09:51 CEST 2021

Dear all,

The previously announced seminar with Daniel Dadush has now been rescheduled to Friday April 23 at 14:00 CET. The title is still "On the complexity of branching proofs" and the abstract can still be found below.

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


Friday Apr 16 at 14:00
On the complexity of branching proofs
(Daniel Dadush, CWI)

We consider the task of proving integer infeasibility of a bounded convex K in R^n using a general branching proof system. In a general branching proof, one constructs a branching tree by adding an integer disjunction ax <= b or ax >= b+1, for an integer vector a and an integer b, at each node, such that the leaves of the tree correspond to empty sets (i.e., K together with the inequalities picked up from the root to leaf is empty). Recently, Beame et al (ITCS 2018), asked whether the bit size of the coefficients in a branching proof, which they named stabbing planes (SP) refutations, for the case of polytopes derived from SAT formulas, can be assumed to be polynomial in n. We resolve this question by showing that any branching proof can be recompiled so that the integer disjunctions have coefficients of size at most (nR)^{O(n2)}, where R is the radius of an l_1 ball containing K, while increasing the number of nodes in the branching tree by at most a factor O(n). As our second contribution, we show that Tseitin formulas, an important class of infeasible SAT instances, have quasi-polynomial sized cutting plane (CP) refutations, disproving the conjecture that Tseitin formulas are (exponentially) hard for CP. As our final contribution, we give a simple family of polytopes in [0,1]^n requiring branching proofs of length 2^n/n.

Joint work with Samarth Tiwari.

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)

More information about the Proof-Complexity mailing list