On the Complexity of Branching Proofs
share
We consider the task of proving integer infeasibility of a bounded convex K in ℝ^n 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, 𝐚∈ℤ^n, 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 (n R)^O(n^2), where R ∈ℕ such that K ∈ R 𝔹_1^n, 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.
READ FULL TEXT