PIMS- SFU Theory Seminar: Noah Flemming

In this talk I will introduce a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. Stabbing Planes proofs extend the DPLL branching from single variables to branching on arbitrary linear inequalities and their "integer negations". This directly generalizes the reasoning underlying standard SAT solvers, which we hope will facilitate the extension of current heuristics to Stabbing Planes-based solvers. Somewhat surprisingly, we are able to show that Stabbing Planes can efficiently simulate Cutting Planes, and is strictly stronger under a reasonable conjecture. In fact, it is possible to characterize the exact restriction of Stabbing Planes proofs that corresponds to Cutting Planes. I will discuss these results and more, as well as several interesting open problems which I believe are in reach.