On the Proof Complexity of Linear Programming Based Branch-and-Bound

This thesis investigates the proof system associated to the branch-and-bound method for linear integer programming, that is, we treat branch-and-bound trees as proofs of the integer-freeness of certain polyhedra (equivalently, of the infeasibility of integer linear programs). We treat both the proof system resulting from branch-and-bound branching on variable disjunctions as well as the one resulting from branching on general disjunctions. We show that several simple known lower bounds on the size of proofs in these systems can be derived from so-called hiding sets. We also review some different techniques for simple lower bounds. We then show that branch-and-bound with general disjunctions admits a property called quasi-feasible monotone real interpolation. This allows us to derive the first sub-exponential (in fact, the first super-linear) lower bound on the size of a branch-and-bound tree for a particular program (measured against the encoding length of the program) by transferring a lower bound from monotone circuit complexity. As intermediate results, we show that branch-and-bound admits the feasible disjunction property and that monotone real circuits can perform binary search efficiently. We discuss how to derive similar bounds for the natural ILP formulation of the satisfiability problem for random CNFs in a certain parameter regime via the notion of insatisfiability certificates introduced by Hrubeš and Pudlák. Moreover, we show that computing either the size of the smallest branch-and-bound tree for a particular program or the size of the tree produced by various branching rules employed in practice is #P-hard and approximating it within some subexponential factor is not possible in subexponential time unless the exponential time hypothesis fails. We review a construction by Alekhnovich and Razborov for the (treelike) resolution proof system, which also yields the non-automatizability of branch-and-bound using variable disjunctions (unless FPT = W[P]). We note that this extends to the case where the support of every constraint is sparse and give a similar construction for the integer linear program formulation of the matching problem in 3-hypergraphs. On the positive side, we give a fixed-parameter tractable algorithm for finding a branch-and-bound tree using variable disjunctions for the matching polytope, parameterized by the treewidth of the underlying graph, the size of a smallest branch-and-bound tree and the bound on the matching deficiency we want to show. Finally, we discuss various questions surrounding reflection properties for branch-and-bound using general disjunctions. We find that branch-and-bound behaves quite similarly to the resolution proof system in this regard, and hope that this will serve as a first step towards a proof of the non-automatizability of branch-and-bound using general disjunctions similar to the proof for the resolution proof system by Atserias and Müller.