Speaker: Ralf Rothenberger (University of Potsdam)

Title: Random k-SAT and the Satisfiability Threshold
Abstract: Random k-SAT is a model to generate k-CNFs with a given number of variables n and a given number of clauses m at random. The model was introduced as a means to study the hardness of solving k-SAT on "typical" input formulas, but studying it turned out to be much more fruitful than expected. One interesting property of the model is the emergence of a satisfiability threshold. The satisfiability threshold is the clause-variable-ratio m/n where random formulas transition from being almost surely satisfiable to being almost surely unsatisfiable. However, analyzing the position and behavior of the satisfiability threshold has been and still is a challenging field of study. In fact, studying the satisfiability threshold led to the development of a plethora of new techniques for the analysis of random structures. In this talk I give a short introduction to the satisfiability threshold and noteworthy results related to it. Furthermore, I will introduce a generalization of the random k-SAT model with given expected variable frequencies and show how these expected frequencies influence the behavior of the satisfiability threshold.

Speaker: Noah Fleming (University of Toronto)

Title: The Proof Complexity of Practical Integer Programming
Abstract: The Stabbing Planes proof system was introduced to model practical branch-and-cut integer programming solvers. As a proof system, Stabbing Planes can be viewed as a simple generalization of DPLL to reason about linear inequalities. It is powerful enough to simulate Cutting Planes and produce short refutations of the Tseitin formulas — certain unsatisfiable systems of linear equations mod 2 — which are canonical hard examples for many algebraic proof systems. In a surprising recent result, Dadush and Tiwari showed that these short Stabbing Planes refutations of the Tseitin formulas could be translated into Cutting Planes proofs. This raises the question of whether all Stabbing Planes can be efficiently translated into Cutting Planes. In recent work, we give a partial answer to this question.

In this talk I will introduce and motivate the Stabbing Planes proof system as a simple proof system which is a direct generalization of DPLL. I will then discuss the relationship between Stabbing Planes and Cutting Planes.