MIAO/BARC talk by Emre Yolcu

Exponential separations using guarded extension variables
Emre Yolcu, Carnegie Mellon University

I will talk about the complexity of proof systems augmenting resolution with inference rules that allow, given a formula F in conjunctive normal form, deriving clauses that are not necessarily logically implied by F but whose addition to F preserves satisfiability. When the derived clauses are allowed to introduce variables not occurring in F, the systems we will consider become equivalent to extended resolution. We are concerned with the versions of these systems "without new variables." They are called BC-, RAT-, SBC-, and GER-, denoting respectively blocked clauses, resolution asymmetric tautologies, set-blocked clauses, and generalized extended resolution. Each of these systems formalizes some restricted version of the ability to make assumptions that hold "without loss of generality," which is commonly used informally to simplify or shorten proofs. Except for SBC-, these systems are known to be exponentially weaker than extended resolution. They are, however, all equivalent to it under a relaxed notion of simulation that allows the translation of the formula along with the proof when moving between proof systems. I will show how to take advantage of this fact to construct formulas that separate RAT- from GER- and vice versa. With a similar strategy, we can also separate SBC- from RAT-. Additionally, I will briefly describe polynomial-size SBC- proofs of the pigeonhole principle, which separates SBC- from GER- by a previously known lower bound. These results also separate the three systems from BC- since they all simulate it. We thus obtain an almost complete picture of their relative strengths.

MIAO seminars
Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a 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 an overview of some exciting research results, and after the break people who have the time and interest will get an opportunity to really get into the technical details. (However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.)

More information about upcoming MIAO seminars can be found here 

We are hoping to record the seminar and post on the MIAO Research YouTube channel for people who would like to hear the talk but cannot attend.