[Proof Complexity] MIAO seminar Tue Oct 18 at 14:00 CET with Emre Yolcu: Exponential separations using guarded extension variables

[Jakob Nordström]

Dear all,

Next Tuesday October 18 at 14:00 Emre Yolcu from Carnegie Mellon University will give a seminar on his work exploring the strength of resolution-based proof systems that have been studied (and used) in the context of SAT solving and proof logging, but for which many intriguing questions have remained open. Emre's talk is titled "Exponential separations using guarded extension variables", and you find the abstract at the bottom of this message.

We will run this as a hybrid seminar at the University of Copenhagen. Local participants are welcome to øv-3-0-25, Universitetsparken 1, University of Copenhagen. Other participants are welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

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 at http://www.jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

Tuesday Oct 18 at 14:00 at DIKU øv-3-0-25, Universitetsparken 1, University of Copenhagen and on Zoom
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.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se