Abstract: 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, those systems become equivalent to extended resolution. We are concerned with their versions 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 them 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-, those systems are already 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 prove several new separations between those systems, giving an almost complete picture of their relative strengths.
This talk is based on joint work with Marijn Heule, to appear in ITCS 2023.