License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2020.34
URN: urn:nbn:de:0030-drops-125863
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12586/
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átal-Gomory (CG) cuts.
As our second contribution, we show that Tseitin formulas, an important class of infeasible SAT instances, have quasi-polynomial sized cutting plane (CP) refutations. This disproves a conjecture that Tseitin formulas are (exponentially) hard for CP. Our upper bound follows by recompiling the quasi-polynomial 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:1--34:35},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-156-6},
ISSN = {1868-8969},
year = {2020},
volume = {169},
editor = {Shubhangi Saraf},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12586},
URN = {urn:nbn:de:0030-drops-125863},
doi = {10.4230/LIPIcs.CCC.2020.34},
annote = {Keywords: Branching Proofs, Cutting Planes, Diophantine Approximation, Integer Programming, Stabbing Planes, Tseitin Formulas}
}
|
Keywords: |
|
Branching Proofs, Cutting Planes, Diophantine Approximation, Integer Programming, Stabbing Planes, Tseitin Formulas |
|
Collection: |
|
35th Computational Complexity Conference (CCC 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
17.07.2020 |
