Dadush, Daniel ;
Tiwari, Samarth
On the Complexity of Branching Proofs
Abstract
We consider the task of proving integer infeasibility of a bounded convex K in ℝⁿ using a general branching proof system. In a general branching proof, one constructs a branching tree by adding an integer disjunction 𝐚𝐱 ≤ b or 𝐚𝐱 ≥ b+1, 𝐚 ∈ ℤⁿ, 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 in the affirmative, by showing that any branching proof can be recompiled so that the normals of the disjunctions have coefficients of size at most (n R)^O(n²), where R ∈ ℕ is the radius of an 𝓁₁ ball containing K, while increasing the number of nodes in the branching tree by at most a factor O(n). Our recompilation techniques works by first replacing each disjunction using an iterated Diophantine approximation, introduced by Frank and Tardos (Combinatorica 1986), and proceeds by "fixing up" the leaves of the tree using judiciously added ChvátalGomory (CG) cuts.
As our second contribution, we show that Tseitin formulas, an important class of infeasible SAT instances, have quasipolynomial sized cutting plane (CP) refutations. This disproves a conjecture that Tseitin formulas are (exponentially) hard for CP. Our upper bound follows by recompiling the quasipolynomial sized SP refutations for Tseitin formulas due to Beame et al, which have a special enumerative form, into a CP proof of the same length using a serialization technique of Cook et al (Discrete Appl. Math. 1987).
As our final contribution, we give a simple family of polytopes in [0,1]ⁿ requiring exponential sized branching proofs.
BibTeX  Entry
@InProceedings{dadush_et_al:LIPIcs:2020:12586,
author = {Daniel Dadush and Samarth Tiwari},
title = {{On the Complexity of Branching Proofs}},
booktitle = {35th Computational Complexity Conference (CCC 2020)},
pages = {34:134:35},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771566},
ISSN = {18688969},
year = {2020},
volume = {169},
editor = {Shubhangi Saraf},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12586},
URN = {urn:nbn:de:0030drops125863},
doi = {10.4230/LIPIcs.CCC.2020.34},
annote = {Keywords: Branching Proofs, Cutting Planes, Diophantine Approximation, Integer Programming, Stabbing Planes, Tseitin Formulas}
}
17.07.2020
Keywords: 

Branching Proofs, Cutting Planes, Diophantine Approximation, Integer Programming, Stabbing Planes, Tseitin Formulas 
Seminar: 

35th Computational Complexity Conference (CCC 2020)

Issue date: 

2020 
Date of publication: 

17.07.2020 