Exponential separations using guarded extension variables

Emre Yolcu, Marijn J. H. Heule

We study the complexity of proof systems augmenting resolution with inference rules that allow, given a formula $\Gamma$ in conjunctive normal form, deriving clauses that are not necess…