On the Power and Limitations of Branch and Cut

TL;DR

This paper explores the relationship between Stabbing Planes and Cutting Planes proof systems, showing how bounded coefficient proofs can be simulated, and establishing new lower bounds on proof depth and size for these systems.

Contribution

It demonstrates the translation of bounded coefficient Stabbing Planes proofs into Cutting Planes, and introduces new geometric techniques to establish lower bounds on proof depth.

Findings

Exponential lower bounds on SP* proof size.

Short refutations of linear systems over finite fields by Cutting Planes.

First lower bounds on the depth of Semantic Cutting Planes proofs.

Abstract

The Stabbing Planes proof system was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas -- certain unsatisfiable systems of linear equations mod 2 -- which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients SP* can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.