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.

Diese Arbeit untersucht das zu der Branch-and-Bound Methode für ganzzahlige lineare Programme gehörige Beweissystem, d.h., wir betrachten Branch-and-Bound Bäume als Beweise für die Integer-Freiheit bestimmter Polyeder (oder äquivalenterweise auch für die Unzulässigkeit von ganzzahligen linearen Programmen). Wir betrachten dabei sowohl das zu Branch-and-Bound mit Variablen-Disjunktionen gehörige Beweissystem, als auch das Beweissystem, welches zu Branch-and-Bound mit allgemeinen Disjunktionen gehört. Wir zeigen zunächst, dass einige simple untere Schranken für die Größe von Branch-and-Bound Bäumen aus der Literatur auf uniforme Weise mithilfe sogenannter Hiding Sets hergeleitet werden können. Außerdem betrachten wir weitere Methoden, um einfache untere Schranken zu erhalten. Des weiteren zeigen wir, dass Branch-and-Bound mit allgemeinen Disjunktionen die quasi-effiziente reelle Interpolations-Eigenschaft besitzt. Das erlaubt uns die erste sub-exponentielle untere Schranke für die Größe eines Branch-and-Bound Baums für ein bestimmtes ganzzahliges lineares Programm zu zeigen (gemessen gegen dessen Kodierungslänge). Diese Schranke ist gleichzeitig auch die erste superlineare solche Schranke. Die Interpolationseigenschaft erlaubt uns dazu eine untere Schranke für die monoton reelle Schaltkreiskomplexität bestimmter Funktionen auszunutzen. Zu diesem Zweck beweisen wir zunächst, dass Branch-and-Bound außerdem auch die effiziente Disjunktions-Eigenschaft besitzt und dass monotone reelle Schaltkreise effizient binäre Suche durchführen können. Wir erläutern, wie wir mit dieser Methode analoge Resultate für die übliche Formulierung für die Erfüllbarkeit von zufälligen Bool’schen Formeln in konjunktiver Normalform (für eine bestimmte Wahl von Parametern) erhalten können, wobei wir den von Hrubeš and Pudlák eingeführten Begriff der Unzulässigkeitszertifikate benutzen. Wir zeigen, dass es sowohl #P-hart ist, die Größe des kürzesten Branch-and- Bound Baums für ein bestimmtes Problem zu bestimmen, als auch die Größe des Branch-and-Bound Baums, welcher von einigen praktischen Regeln erzeugt wird. Des weiteren ist es nicht möglich diese Größen in sub-exponentieller Zeit bis auf einen gewissen sub-exponentiellen Faktor zu approximieren, falls die Exponentialzeitshypothese wahr ist. Wir betrachten eine Konstruktion von Alekhnovich and Razborov, welche mit der Nicht-Automatisierbarkeit des Resolutionskalküls auch die Nicht-Automatisierbarkeit von Branch-and-Bound mit Variablen-Disjunktionen zeigt, falls nicht FPT = W[P]. Wir bemerken, dass dieses Resultat auch im Fall, dass alle Nebenbedingungen dünn besetzt sind, Bestand hat und geben eine analoge Konstruktion, welche die Nicht-Automatisierbarkeit von Branch-and-Bound mit Variablen-Disjunktionen eingeschränkt auf die natürliche Formulierung des Matching Problems in 3-Hypergraphen zeigt. Als positives Resultat geben wir einen effizienten parametrisierten Algorithmus, welcher einen Branch-and-Bound Baum für das fraktionalen Matching Polytop produziert, wobei der Algorithmus mit der Größe eines kürzesten Baumes, der Baumweite des zugrundeliegenden Graphen und der unteren Schranke an die Matching Defizienz, welche wir beweisen wollen, parametrisiert ist. Schlussendlich untersuchen wir, wie sich Branch-and-Bound mit allgemeinen Disjunktionen in Bezug auf Reflektionseigenschaften verhält. Wir zeigen, dass Branch-and- Bound sich in dieser Hinsicht sehr ähnlich wie das Resolutionskalkül verhält und hoffen, dass unsere Resultate als erster Schritt in Richtung eines Beweises der Nicht-Automatsierbarkeit von Branch-and-Bound mit allgemeinen Disjunktionen im Stil des Beweises des analogen Resultats für das Resolutionskalkül von Atserias and Müller dienen.