Resolution Lower Bounds for Refutation Statements

TL;DR

This paper establishes exponential lower bounds on the size of resolution refutations for unsatisfiable CNF formulas, with applications to natural encodings, reflection principles, and proof system separations.

Contribution

It provides the first exponential lower bounds for the size of resolution refutations of the statement that a formula has a resolution refutation, addressing open questions and improving known results.

Findings

Exponential lower bounds for resolution refutations of certain CNFs.

Resolution size lower bounds for reflection principles.

New examples separating Res(2) from Resolution exponentially.

Abstract

For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in (Atserias, M\"uller 2019) asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in (Atserias, Bonet 2004). (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in (Segerlind, Buss, Impagliazzo 2004)).