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

[Jakob Nordström]

Dear all,


This is just to say that unfortunately we have to cancel the seminar tomorrow, but we hope to be able to reschedule to a date in the near future.

Best regards,
Jakob Nordström

________________________________
From: Jakob Nordström
Sent: 31 March 2021 21:47
To: CS - miao-seminar-theory
Cc: Daniel Dadush
Subject: Seminar Fri Apr 16 at 14:00 CET with Daniel Dadush: On the complexity of branching proofs


Dear all,

On Friday April 16 at 14:00 CET we have a seminar with Daniel Dadush from CWI titled "On the complexity of branching proofs". See below for the abstract.

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 is posted (from time to time) at http://www.csc.kth.se/~jakobn/videoseminars/. 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 CET
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)