MIAO video seminar: Proof complexity lower bounds by composition
Title: Proof complexity lower bounds by composition
Speaker: Robert Robere, McGill University
Host: Jacob Nordström, Department of Computer Science, Lund University Joint with
Where: Online - link by registration
In recent years, there has been an explosion in the development of so-called "lifting theorems" in proof complexity and other closely related areas which have led to the resolution of many long-standing open problems. The basic idea of a lifting theorem is simple: in order to prove a lower bound in a "complicated" system that we do not understand (for example, Cutting Planes refutations), we will "escalate" the hardness from a "simple" system that we do understand (for example, Resolution refutations) by taking a hard formula F for the simple system and composing it with a specially chosen "gadget function" that removes the power of the complicated system. In many cases, it is possible to prove that the "best" possible strategy in the complicated system for refuting the composed formula is to simulate the proof of the uncomposed formula in the simple system (and thus lower bounds for the uncomposed formula are "escalated" or "lifted" to lower bounds for the composed formula). While lifting theorems in circuit complexity can be traced back to the work of Raz and McKenzie [RM99], recent developments have pushed these techniques to many new areas, and have shown how lifting is a flexible tool that allows quite finely tuned tradeoffs between different parameters for a wide variety of proof systems.
In this talk, we give an introduction to and survey of lifting results in proof complexity and related fields, like communication complexity and circuit complexity, and outline some of the ways that lifting can be used to control various "complexity parameters" of unsatisfiable CNF formulas (like proof length, proof space, proof depth, etc.). We will highlight several recent developments in the area and indicate some future directions.
Please register at lth.se/digitalth/events/register in order to get an access link to the zoom platform.
The MIAO video seminars are arranged by the Mathematical Insights into Algorithms for Optimization (MIAO) research group at the University of Copenhagen and Lund University. Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break an optional ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners a self-contained overview of some exciting research results. For listeners who are particularly interested, there is then an opportunity to return for a second part where we get into more technical details.