The Complexity of Some Geometric Proof Systems

Abstract

In this Thesis we investigate proof systems based on Integer Linear Programming. These methods inspect the solution space of an unsatisfiable propositional formula and prove that this space contains no integral points.

We begin by proving some size and depth lower bounds for a recent proof system, Stabbing Planes, and along the way introduce some novel methods for doing so.

We then turn to the complexity of propositional contradictions generated uniformly from first order sentences, in Stabbing Planes and Sum-Of-Squares.

We finish by investigating the complexity-theoretic impact of the choice of method of generating these propositional contradictions in Sherali-Adams.