On the Complexity of Branching Proofs

TL;DR

This paper investigates the complexity of branching proofs for integer infeasibility, showing bounds on proof size and coefficients, and providing new results on Tseitin formulas and specific polytopes.

Contribution

It proves that branching proofs can be recompiled with polynomially bounded coefficients, shows Tseitin formulas have quasi-polynomial cutting plane refutations, and constructs polytopes requiring exponential branching proofs.

Findings

Coefficients in branching proofs can be bounded by 0^{O(n^2)}.

Tseitin formulas admit quasi-polynomial size cutting plane refutations.

Certain polytopes require exponential length branching proofs.

Abstract

We consider the task of proving integer infeasibility of a bounded convex $K$ in $\mathbb{R}^n$ using a general branching proof system. In a general branching proof, one constructs a branching tree by adding an integer disjunction $\mathbf{a} \mathbf{x} \leq b$ or $\mathbf{a} \mathbf{x} \geq b+1$, $\mathbf{a} \in \mathbb{Z}^n$, $b \in \mathbb{Z}$, 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 \in \mathbb{N}$ such that $K \in R \mathbb{B}_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$.