# Exponential separations using guarded extension variables

Emre Yolcu<EMAIL_ADDRESS>Computer Science Department, Carnegie
Mellon University.  Marijn J. H. Heule11footnotemark: 1

###### Abstract

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 necessarily logically implied by $\Gamma$ but
whose addition to $\Gamma$ preserves satisfiability. When the derived clauses
are allowed to introduce variables not occurring in $\Gamma$, the systems we
consider become equivalent to extended resolution. We are concerned with the
versions of these systems without new variables. They are called
$\mathsf{BC}^{-}$, $\mathsf{RAT}^{-}$, $\mathsf{SBC}^{-}$, and
$\mathsf{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 $\mathsf{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. By taking advantage of
this fact, we construct formulas that separate $\mathsf{RAT}^{-}$ from
$\mathsf{GER}^{-}$ and vice versa. With the same strategy, we also separate
$\mathsf{SBC}^{-}$ from $\mathsf{RAT}^{-}$. Additionally, we give polynomial-
size $\mathsf{SBC}^{-}$ proofs of the pigeonhole principle, which separates
$\mathsf{SBC}^{-}$ from $\mathsf{GER}^{-}$ by a previously known lower bound.
These results also separate the three systems from $\mathsf{BC}^{-}$ since
they all simulate it. We thus give an almost complete picture of their
relative strengths.

##  1 Introduction

###  1.1 Properties of commonly studied proof systems

Most of the commonly studied rule-based propositional proof
systems,111Throughout this paper, by “proof” we mean a refutation of
satisfiability (i.e., a derivation of $\bot$ from a set $\Gamma$ of formulas,
where $\bot$ denotes a contradiction such as the empty clause). such as
resolution [4, 29], Frege [11], cutting planes [7], polynomial calculus [8],
Lovász–Schrijver [25], are in several senses well behaved. For instance, they
are monotonic, strongly sound, and strongly closed under restrictions.

  * •

A proof system $P$ is _monotonic_ if for all sets $\Gamma$ and
$\Gamma^{\prime}$ of formulas such that $\Gamma\subseteq\Gamma^{\prime}$ and
for every formula $\varphi$ we have

$\Gamma\vdash_{P}\varphi\implies\Gamma^{\prime}\vdash_{P}\varphi,$

where $\vdash_{P}$ is the derivability relation for $P$. Since we often
express a proof as a tree, monotonicity naturally holds for most proof
systems. It has the consequence that the validity of an inference in the proof
relies only on some subset of the previously derived formulas as opposed to
the entire set.

  * •

_Strong soundness_ is the property of a proof system $P$ that a formula
$\varphi$ can be derived in $P$ from a set $\Gamma$ of formulas only if
$\varphi$ is logically implied by $\Gamma$ (i.e., every total assignment
satisfying all formulas in $\Gamma$ also satisfies $\varphi$), written as

$\Gamma\vdash_{P}\varphi\implies\Gamma\models\varphi.$ (1)

Soundness is less strict than strong soundness in that it only requires 1 to
hold for $\varphi=\bot$.

  * •

For a formula $\varphi$ and a partial assignment $\alpha$, let
$\varphi|_{\alpha}$ denote the formula obtained by first replacing every
assigned variable $x$ occurring in $\varphi$ by $\alpha(x)$ and then
recursively simplifying all of the subformulas. For a set $\Gamma$ of
formulas, let
$\Gamma|_{\alpha}\coloneqq\\{\psi|_{\alpha}\mid\psi\in\Gamma\\}$. We call
$\varphi|_{\alpha}$ the restriction of $\varphi$ under $\alpha$, and similarly
for $\Gamma$. We say a proof system $P$ is _strongly closed under
restrictions_ if for every set $\Gamma$ of formulas, for every formula
$\varphi$, and for every partial assignment $\alpha$ that does not satisfy
$\varphi$, we have

$\Gamma\vdash_{P}\varphi\implies\Gamma|_{\alpha}\vdash_{P}\varphi|_{\alpha}.$
(2)

As in the case of soundness, (weak) closure under restrictions only requires 2
to hold for $\varphi=\bot$. Closure under restrictions is often also defined
by the more quantitative condition that for every $P$-proof $\Pi$ of $\Gamma$
and every partial assignment $\alpha$ there exist a $P$-proof $\Pi^{\prime}$
of $\Gamma|_{\alpha}$ of size polynomial in the size of $\Pi$.

None of the above properties are necessary for soundness, and proof systems
that do not have them can be stronger since such systems are more permissive
in terms of the kinds of reasoning they allow. Possibly the most prominent
example of such a system in proof complexity is extended Frege [11]. When
refuting a set $\Gamma$ of formulas, extended Frege allows (in addition to the
axioms and the rules of the underlying Frege system) proof steps of the form

$x\leftrightarrow\varphi,$ (3)

where $x$ is a variable and $\varphi$ is an arbitrary formula, with the
condition that $x$ not occur in $\Gamma$, any of the preceding steps, or
$\varphi$. Another example is extended resolution [31], which similarly uses 3
although in a more restricted form since resolution works only with clauses.
With $x$ a “new” variable as before and $p$, $q$ literals, extended resolution
allows introducing $x\leftrightarrow p\land q$ via the following clauses,
where the overline denotes negation:

$\overline{x}\lor p\qquad\overline{x}\lor q\qquad
x\lor\overline{p}\lor\overline{q}$ (4)

Extended Frege (and similarly extended resolution) has none of the above
properties, although the reasons are not particularly interesting:

  * •

Monotonicity fails to hold since we cannot necessarily derive
$x\leftrightarrow\varphi$ from $\Gamma^{\prime}\supseteq\Gamma$ if $x$ already
occurs in $\Gamma^{\prime}$.

  * •

Strong soundness fails to hold since $\Gamma$ may not imply
$x\leftrightarrow\varphi$ under assignments $\alpha$ such that
$\alpha(x)\neq\alpha(\varphi)$. Nevertheless, extended Frege is sound because
$\Gamma$ and $\Gamma\cup\\{x\leftrightarrow\varphi\\}$ are equisatisfiable
(i.e., $\Gamma$ is satisfiable if and only if
$\Gamma\cup\\{x\leftrightarrow\varphi\\}$ is satisfiable), seen as follows: if
an assignment $\alpha$ satisfies $\Gamma$ but falsifies
$x\leftrightarrow\varphi$, flipping $\alpha(x)$ gives a different assignment
$\alpha^{\prime}$ satisfying both $\Gamma$ and $x\leftrightarrow\varphi$.

  * •

Strong closure under restrictions fails to hold since otherwise we could
choose a partial assignment that only assigns $x$ to $\mathit{True}$ and
conclude that every formula $\varphi$ can be derived from $\Gamma$, which
contradicts the soundness of extended Frege.

In all of the above cases, the counterexamples rely crucially on the fact that
$x$ is a new variable. This ability to abbreviate complex formulas by
variables significantly increases the difficulty of proving lower bounds for
extended Frege and makes it one of the strongest propositional proof systems.
(Extended resolution is equivalent to it over refutations of sets of clauses.)
From this point on, we use “formula” and “set of clauses” interchangeably.

Proof systems that violate the above properties for more sophisticated reasons
(i.e., not simply due to the introduction of new variables) also exist. In
this paper we compare the proof complexity of four such systems that augment
resolution with inference rules of varying expressiveness. Given a set
$\Gamma$ of clauses, these rules allow deriving clauses that are not
necessarily logically implied by $\Gamma$ but whose addition to $\Gamma$
preserves satisfiability. We call such clauses redundant. Deciding the
redundancy of a clause with respect to a set of clauses is
$\mathsf{coDP}$-complete222The class $\mathsf{DP}=\\{L_{1}\cap L_{2}\mid
L_{1}\in\mathsf{NP},L_{2}\in\mathsf{coNP}\\}$, which is a superset of both
$\mathsf{NP}$ and $\mathsf{coNP}$, was defined by Papadimitriou and Yannakakis
[28]. [2], so we consider only the inference rules that rely on polynomial-
time verifiable syntactic conditions corresponding to restricted versions of
redundancy. These rules may be viewed as capturing the commonly used technique
of making assumptions that hold “without loss of generality” when writing
informal mathematical proofs. Such assumptions are not logically implied by
the hypotheses at hand, but their use is justified by the fact that they can
be eliminated at the possible cost of an increase in the size of the proof.
The formal rules we study rely on syntactic criteria to justify such
assumptions, with weaker criteria allowing the introduction of stronger
assumptions. In this way, these rules allow us to directly express various
kinds of informal reasoning that are otherwise difficult to formalize.

From the perspective of the broader study of proof complexity, these systems
are somewhat unique in that Frege does not simulate even the weakest variant
unless Frege and extended Frege are equivalent [6, Corollary 2.5]. It would be
interesting to determine whether some variant of these systems, despite having
the same limited syntax as resolution and no new variables, simulates a
subsystem of Frege stronger than resolution.

###  1.2 Related work

####  1.2.1 Proof complexity

The inference rules we study originate from the notion of blocked clauses,
developed initially by Kullmann [22, 23] to give improved deterministic
algorithms for 3-SAT. We call a clause $C$ blocked with respect to a set
$\Gamma$ of clauses if there exists a literal $p\in C$ such that all possible
resolvents of $C$ on $p$ against clauses from $\Gamma$ are tautological (i.e.,
contain a literal and its negation). Kullmann [24] showed that blocked clauses
are redundant and thus considered an inference rule that, given a set $\Gamma$
of clauses, allows us to extend $\Gamma$ with a clause that is blocked with
respect to $\Gamma$. This rule, along with resolution, gives the proof system
called _blocked clauses_ $(\mathsf{BC})$. As illustrated below, $\mathsf{BC}$
is not monotonic, not strongly sound, and not strongly closed under
restrictions.

######  Example 1.1.

The clause $C=\overline{x}\lor\overline{y}$ is blocked with respect to the set
$\Gamma=\\{x\lor y,\ x\lor\overline{y}\\}$.

  * •

Monotonicity fails to hold since we cannot derive $C$ from
$\Gamma^{\prime}=\Gamma\cup\\{y\\}$ in $\mathsf{BC}$: the set
$\Gamma^{\prime}$ is satisfiable but $\Gamma^{\prime}\cup\\{C\\}$ is
unsatisfiable.

  * •

Strong soundness fails to hold since $\Gamma$ does not imply $C$ under
assignments that set both $x$ and $y$ to $\mathit{True}$.

  * •

Strong closure under restrictions fails to hold since for an assignment
$\alpha$ that sets $y$ to $\mathit{True}$ we cannot derive
$C|_{\alpha}=\overline{x}$ from $\Gamma|_{\alpha}=\\{x\\}$ in $\mathsf{BC}$:
the set $\Gamma|_{\alpha}$ is satisfiable but
$\Gamma|_{\alpha}\cup\left\\{C|_{\alpha}\right\\}$ is unsatisfiable.

It is apparent from the definition of a blocked clause that deleting clauses
from $\Gamma$ enlarges the set of clauses that are blocked with respect to
$\Gamma$. With this observation at hand, Kullmann defined a strengthening of
$\mathsf{BC}$ called _generalized extended resolution_ ($\mathsf{GER}$) that
allows the temporary deletion of clauses from $\Gamma$. Arbitrary deletion of
clauses does not necessarily preserve satisfiability; however, since no subset
of a satisfiable $\Gamma$ is unsatisfiable, it is also possible to further
strengthen $\mathsf{GER}$ by allowing the arbitrary deletion of a clause as a
proof step. The resulting system is called _deletion blocked clauses_
($\mathsf{DBC}$).

Conversely to the above point, the failure of monotonicity becomes
particularly important when deletion is not allowed since it implies that the
validity of blocked clause additions performed in sequence are order
dependent. In particular, not every set of clauses that are all blocked with
respect to $\Gamma$ can be derived from $\Gamma$ by a sequence of blocked
clause additions. For this reason, proving upper bounds for generalizations of
$\mathsf{BC}$ involves carefully ensuring the validity of sequences of
inferences.

Without any additional restrictions, the above systems all simulate extended
resolution since the clauses in 4 can be added in sequence as blocked clauses
if we are allowed to introduce new variables: starting with a set $\Gamma$ of
clauses not containing the variable $x$, we can derive

  * •

$\overline{x}\lor p$ followed by $\overline{x}\lor q$ since no occurrence of
the literal $x$ precedes either step (so both clauses are vacuously blocked),
and then

  * •

$x\lor\overline{p}\lor\overline{q}$ since its resolvents on $x$ against
$\overline{x}\lor p$ and $\overline{x}\lor q$ (i.e., the only preceding
occurrences of $\overline{x}$) are tautological.

The study of these systems becomes interesting when we disallow new variables.
A proof of $\Gamma$ is _without new variables_ if it contains only the
variables that already occur in $\Gamma$. Throughout this paper, we denote a
proof system variant that disallows new variables with the superscript “$-$”
(e.g., $\mathsf{BC}^{-}$ is $\mathsf{BC}$ without new variables). We denote a
variant that allows arbitrary deletion with the prefix $\mathsf{D}$. All of
those variants constitute examples of proof systems that share the
peculiarities of extended resolution from Section 1.1 without being allowed
new variables.

Kullmann [24] proved that extended resolution simulates $\mathsf{GER}$. He
also proved that $\mathsf{GER}^{-}$ is exponentially stronger than resolution
and exponentially weaker than extended resolution. In later work, Järvisalo,
Heule, and Biere [17] defined a different generalization of $\mathsf{BC}$ by
essentially replacing “tautological” in the definition of a blocked clause
with “implied by $\Gamma$ through unit propagation.” (Unit propagation is an
automatizable but incomplete variant of resolution.) The result is still a
polynomial-time verifiable redundancy criterion since the only important
property of tautologies in the argument for the redundancy of a blocked clause
$C$ with respect to $\Gamma$ is that tautologies are implied by $\Gamma$. This
generalization is called _resolution asymmetric tautologies_ ($\mathsf{RAT}$).
Yet another generalization of $\mathsf{BC}$ along a different axis is called
_set-blocked clauses_ ($\mathsf{SBC}$), defined by Kiesl, Seidl, Tompits, and
Biere [21]. We call a clause $C$ set-blocked with respect to a set $\Gamma$ of
clauses if there exists some nonempty $L\subseteq C$ such that for all
$D\in\Gamma$ with $D\cap\overline{L}\neq\varnothing$ and $D\cap L=\varnothing$
the set $\bigl{(}C\setminus
L\bigr{)}\cup\bigl{(}D\setminus\overline{L}\bigr{)}$ is tautological. A
blocked clause is the special case where $L$ is a singleton, so set-
blockedness expands the scope of the literals in $C$ that we consider.
Deciding the set-blockedness of a clause with respect to a set of clauses is
$\mathsf{NP}$-complete [21]. To ensure that an $\mathsf{SBC}$ proof is
polynomial-time verifiable, every step in the proof that adds a clause $C$ as
set-blocked is expected to indicate the subset $L\subseteq C$ for which $C$ is
set-blocked. With that said, to reduce clutter, we leave this requirement out
of our definitions and indicate those subsets only informally throughout this
paper.

Subsequent works [15, 19] defined further generalizations, showed simulations
between some variants, and gave polynomial-size proofs (without new variables)
of the pigeonhole principle in a variant called _set-propagation redundancy_
($\mathsf{SPR}^{-}$) that combines $\mathsf{SBC}^{-}$ and $\mathsf{RAT}^{-}$.
Recently, Buss and Thapen [6] initiated a systematic study of the proof
complexity of the many generalizations of $\mathsf{BC}^{-}$. Among other
results, they showed that the bit pigeonhole principle, parity principle,
clique-coloring principle, and Tseitin tautologies have polynomial-size
$\mathsf{SPR}^{-}$ proofs. They also showed that $\mathsf{SPR}^{-}$ can undo
(with polynomial-size derivations) the effects of or-ification, xor-ification,
and lifting with index gadgets. In view of these results, $\mathsf{SPR}^{-}$
appears to be surprisingly strong.333As remarked by Buss and Thapen [6,
Section 4], the apparent strength of $\mathsf{SPR}^{-}$ stems from the ability
to exploit symmetries, which are abundant in the combinatorial principles used
for proving lower bounds against the commonly studied proof systems. Other
interesting examples of systems that easily prove such combinatorial
principles are the variants of Krishnamurthy’s _symmetric resolution_ [20, 32,
1, 30], obtained by augmenting resolution with rules that explicitly support
reasoning about symmetries. Buss and Thapen also proved an exponential size
lower bound for $\mathsf{RAT}^{-}$, separating $\mathsf{DRAT}^{-}$ and
$\mathsf{SPR}^{-}$ from it. Superpolynomial lower bounds for
$\mathsf{SPR}^{-}$ or even $\mathsf{SBC}^{-}$ are currently open.

####  1.2.2 SAT solving

As the use of SAT solvers in propositional theorem proving increased, it
became standard to expect a solver to produce a proof alongside an
unsatisfiability claim. Modern SAT solvers are based on conflict-driven clause
learning (CDCL) [26] and essentially search for resolution proofs. As a
result, the initial proof systems developed to help verify the outputs of CDCL
SAT solvers were based on resolution [12, 33]. However, most of the current
SAT solvers go beyond CDCL and employ an array of _inprocessing techniques_
[17] that transform the formula during the search. These techniques are often
not strongly sound, and resolution falls short for expressing them. Järvisalo,
Heule, and Biere [17] observed that $\mathsf{DRAT}$ simulated all of the
common techniques used at the time, and, following the implementation of a
practical verifier [34], $\mathsf{DRAT}$ became the de facto standard proof
system used in SAT solvers. Extended resolution could also be used for
verification; however, it is only known to simulate $\mathsf{DRAT}$ with
polynomial overhead [19, Section 4.5], whereas $\mathsf{DRAT}$ simulates
extended resolution with no overhead. There are also a few examples of
$\mathsf{DRAT}$ enabling significant gains over the smallest known extended
resolution proofs (see, e.g., [19, Table 1]), which is important for practical
purposes.

Another practical motivation for studying these systems is their potential
usefulness in proof search due to the surprising strength of the variants
without new variables. Recent works have introduced a SAT solving paradigm
called _satisfaction-driven clause learning_ (SDCL) [16, 14] that can fully
automatically discover small proofs of the pigeonhole principle. Its
usefulness remains limited, though, since it was observed to improve upon CDCL
only on specific classes of formulas. Exploiting the power of these systems
might be a promising avenue for the research that aims to improve the
performance of practical SAT solvers. To this end, it is important to
understand the relative strengths of these systems.

###  1.3 Results

$\mathsf{BC}^{\smash{-}}$$\mathsf{SBC}^{\smash{-}}$$\mathsf{RAT}^{\smash{-}}$$\mathsf{SPR}^{\smash{-}}$$\mathsf{GER}^{\smash{-}}$$\mathsf{DBC}^{\smash{-}}$$\mathsf{DSBC}^{\smash{-}}$$\mathsf{DRAT}^{\smash{-}}$$\mathsf{DSPR}^{\smash{-}}$
Figure 1: In the above diagram, the proof systems are placed in three-
dimensional space with $\mathsf{BC}^{-}$ at the origin. Moving away from the
origin along each axis corresponds to a particular way of generalizing a proof
system. For systems $P$ and $Q$, we use $P\mathrel{\leavevmode\hbox
to17.9pt{\vbox to3.6pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-1.79999pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{14.33336pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.70006pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}Q$ to denote that $P$
simulates $Q$; (and $P\mathrel{\leavevmode\hbox to17.9pt{\vbox
to3.6pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.79999pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {{}{}}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}}
}}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{5.50003pt}{0.0pt}\pgfsys@lineto{6.567pt}{1.42264pt}\pgfsys@lineto{7.63399pt}{0.0pt}\pgfsys@lineto{7.63399pt}{0.0pt}\pgfsys@lineto{14.33336pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.70006pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}Q$ to indicate an
“interesting” simulation, where $P$ is not simply a generalization of $Q$);
$P\mathrel{\leavevmode\hbox to17.9pt{\vbox
to3.67pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-1.83511pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{14.02979pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{13.82979pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}Q$ to denote that $P$
is exponentially separated from $Q$ (i.e., there exists an infinite sequence
of formulas admitting polynomial-size proofs in $P$ while requiring
exponential-size proofs in $Q$); and $P\mathrel{\leavevmode\hbox
to17.9pt{\vbox to8.5pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower-4.25pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{14.33336pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.70006pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}\pgfsys@beginscope\pgfsys@invoke{
} { \pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.5pt}\pgfsys@invoke{
}\color[rgb]{1,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,1}\pgfsys@color@gray@stroke{1}\pgfsys@invoke{
}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}{}\pgfsys@moveto{7.35pt}{-3.0pt}\pgfsys@lineto{8.54999pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{}\pgfsys@moveto{6.1pt}{-3.0pt}\pgfsys@lineto{7.29999pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} {}{{}}{}
{}{}{}\pgfsys@moveto{8.6pt}{-3.0pt}\pgfsys@lineto{9.79999pt}{3.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}{}{{}}
}}{{}}}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} }{{}{}}{{}{}}{{{{}{}{{}}
}}{{}} {{}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}Q$ to denote that $P$
both simulates $Q$ and is exponentially separated from $Q$. Arrows in red
indicate the relationships that are new in this paper. To reduce clutter, some
relationships that are implied by transitivity are not displayed (e.g.,
$\mathsf{DBC}^{-}$ simulates $\mathsf{RAT}^{-}$ and is exponentially separated
from it through $\mathsf{DRAT}^{-}$).

We prove some results concerning the relative strengths of $\mathsf{BC}^{-}$,
$\mathsf{RAT}^{-}$, $\mathsf{SBC}^{-}$, and $\mathsf{GER}^{-}$, continuing the
line of work [24, 15, 19, 6] on the proof complexity of generalizations of
$\mathsf{BC}^{-}$. Figure 1 summarizes the state of the proof complexity
landscape surrounding these systems after our results.

Our first main result is a two-way separation between $\mathsf{RAT}^{-}$ and
$\mathsf{GER}^{-}$.

######  Theorem 1.2.

There exists an infinite sequence $(\Gamma_{n})_{n=1}^{\infty}$ of formulas
such that $\Gamma_{n}$ admits $\mathsf{RAT}^{-}$ proofs of size $n^{O(1)}$ but
requires $\mathsf{GER}^{-}$ proofs of size $2^{\Omega(n)}$. Conversely, there
exists an infinite sequence $(\Delta_{n})_{n=1}^{\infty}$ of formulas such
that $\Delta_{n}$ admits $\mathsf{GER}^{-}$ proofs of size $n^{O(1)}$ but
requires $\mathsf{RAT}^{-}$ proofs of size $2^{\Omega(n)}$.

Since both $\mathsf{RAT}^{-}$ and $\mathsf{GER}^{-}$ are generalizations of
$\mathsf{BC}^{-}$, the above result also separates both systems from
$\mathsf{BC}^{-}$. It was already understood that $\mathsf{GER}^{-}$ is
between $\mathsf{BC}^{-}$ and $\mathsf{DBC}^{-}$ in strength, and
$\mathsf{GER}^{-}$ is in fact “strictly” between $\mathsf{BC}^{-}$ and
$\mathsf{DBC}^{-}$ by Theorem 1.2.

For both directions of the separation, we follow a strategy that exploits the
equivalence of $\mathsf{BC}^{-}$ (without new variables) to extended
resolution under _effective simulations_ [13, 27], which allow the translation
of the formula (in a satisfiability-preserving way) along with the proof when
moving between proof systems. In particular, Kullmann [24, Lemma 8.4] and Buss
and Thapen [6] observed that it is possible to incorporate new variables into
a formula $\Gamma$ in such a way that $\mathsf{BC}^{-}$, while still
technically only using the variables occurring in the formula, simulates an
extended resolution proof of $\Gamma$.

######  Lemma 1.3 ([6, Lemma 2.2]).

Suppose that a formula $\Gamma$ has an extended resolution proof of size $m$
and that $\Gamma$ and the set $X=\\{y\lor x_{1}\lor\dots\lor x_{m},\ y\\}$ of
clauses have no variables in common. Then $\Gamma\cup X$ has a
$\mathsf{BC}^{-}$ proof of size $O(m)$.

To separate $\mathsf{RAT}^{-}$ and $\mathsf{GER}^{-}$, we incorporate new
variables into formulas in ways that are useful to only one of the two
systems. We achieve this by “guarding” the new variables by clauses instead of
providing them as in Lemma 1.3. Recall that, for a clause to be redundant with
respect to a formula according to some syntactic criterion in this paper,
every clause in the formula has to satisfy a certain condition. We take
advantage of this fact to include the new variables within a strategically
chosen set $\mathcal{X}$ of guard clauses alongside an unsatisfiable formula
$\Gamma$. With a suitable choice of $\mathcal{X}$, we are able to impose
enough limitations upon the redundant clauses derivable in a system to ensure
that the new variables can essentially be ignored in a proof of
$\Gamma\cup\mathcal{X}$.

For each direction of the separation, when proving the upper bound for one of
the two systems, we show that it can efficiently work through the guard
clauses and use the new variables to simulate the extended resolution proof.
When proving the lower bound for the other system, we show essentially that it
is closed under restrictions444We use closure under restrictions here in the
quantitative sense described in Section 1. for the specific formulas and
partial assignments that we construct. (Neither system is closed under
restrictions in general.) In other words, the guard clauses make it impossible
for the system to efficiently “access” the new variables, thus preventing it
from achieving any speedup. This allows us to use the existing separations of
extended resolution from $\mathsf{RAT}^{-}$ and $\mathsf{GER}^{-}$ to separate
the two systems without needing to prove lower bounds entirely from scratch.
The main difficulty is in coming up with the appropriate ways of incorporating
new variables into formulas.

As our next main result, we separate $\mathsf{SBC}^{-}$ from
$\mathsf{RAT}^{-}$ (and hence $\mathsf{BC}^{-}$) with the same strategy. In
fact, we reuse the formulas separating $\mathsf{GER}^{-}$ from
$\mathsf{RAT}^{-}$ and show that $\mathsf{SBC}^{-}$ can also efficiently work
through the guard clauses in them, although in a different manner than
$\mathsf{GER}^{-}$.

######  Theorem 1.4.

There exists an infinite sequence $(\Gamma_{n})_{n=1}^{\infty}$ of formulas
such that $\Gamma_{n}$ admits $\mathsf{SBC}^{-}$ proofs of size $n^{O(1)}$ but
requires $\mathsf{RAT}^{-}$ proofs of size $2^{\Omega(n)}$.

Finally, we give polynomial-size $\mathsf{SBC}^{-}$ proofs of the pigeonhole
principle, which exponentially separates $\mathsf{SBC}^{-}$ from
$\mathsf{GER}^{-}$ by a lower bound due to Kullmann [24, Lemma 9.4].

######  Theorem 1.5.

There exists an infinite sequence $(\Gamma_{n})_{n=1}^{\infty}$ of formulas
such that $\Gamma_{n}$ admits $\mathsf{SBC}^{-}$ proofs of size $n^{O(1)}$ but
requires $\mathsf{GER}^{-}$ proofs of size $2^{\Omega(n)}$.

Along the way to our main results, we prove a partial simulation of
$\mathsf{RAT}^{-}$ by $\mathsf{BC}^{-}$. It is partial in the sense that the
size of the produced $\mathsf{BC}^{-}$ proof is not always a polynomial in the
size of the $\mathsf{RAT}^{-}$ proof (which is impossible due to Theorem 1.2).
It also has the property that, although the produced proof may sometimes be
small, the simulation cannot necessarily be carried out in time polynomial in
the size of the produced proof. This is because the simulation involves
generating satisfying assignments to certain formulas obtained in the process.
To our knowledge, all of the “natural” simulations between the commonly
studied proof systems are efficient, so the partial simulation of
$\mathsf{RAT}^{-}$ by $\mathsf{BC}^{-}$ is an odd example. Another notable
aspect of the simulation is that it directly informed the construction of the
formulas that we use for separating $\mathsf{RAT}^{-}$ from
$\mathsf{GER}^{-}$. We discuss this further at the end of Section 4. Due to
the technical nature of the simulation, we do not state it here in detail.

###  1.4 Open questions

We leave open the following.

######  Question 1.6.

Is $\mathsf{RAT}^{-}$ exponentially separated from $\mathsf{SBC}^{-}$?

######  Question 1.7.

Is $\mathsf{GER}^{-}$ exponentially separated from $\mathsf{SBC}^{-}$?

Answering these questions will complete the picture of the relative strengths
of the weakest generalizations of $\mathsf{BC}^{-}$ along each axis in Figure
1. However, we do not even have any superpolynomial lower bounds for
$\mathsf{SBC}^{-}$. If a separation of extended resolution from
$\mathsf{SBC}^{-}$ is shown, it might be possible to relatively easily
separate $\mathsf{RAT}^{-}$ and $\mathsf{GER}^{-}$ from $\mathsf{SBC}^{-}$ by
tailoring guarded extension variables that $\mathsf{SBC}^{-}$ cannot access
(in the manner of the current paper).

As an aside, the formulas that we use for the separations in this paper are
arguably “artificial” in that they do not encode any combinatorial principles.
Separations with “natural” formulas give more intuitive insight into the
relative capabilities of the proof systems being considered, so it is
desirable to reprove Theorems 1.2 and 1.4 using formulas that encode some
combinatorial principles. On the other hand, those artificial formulas enable
relatively simple and modular proofs of the separations. An interesting open
question is whether our strategy of separating two proof systems $P$ and $Q$,
both of which effectively simulate a strong system $R$, through syntactic
manipulations of formulas that separate $R$ from $P$ and $Q$ is more generally
applicable.555A slightly similar strategy gives a separation of linear
resolution from tree-like and regular resolution (and some other variants of
resolution) 5, Lemma 4.5; 3, Section 2.

Another desirable goal is to establish tighter connections between the more
commonly studied proof systems and the generalizations of $\mathsf{BC}^{-}$.
As mentioned earlier, Frege does not simulate $\mathsf{BC}^{-}$ unless it also
simulates extended Frege. Additionally, it is already known that bounded-depth
Frege does not simulate $\mathsf{BC}^{-}$ [6, Corollary 2.3]. We naturally
wonder about the converse direction.

######  Question 1.8.

Is there a subsystem of Frege stronger than resolution that $\mathsf{DBC}^{-}$
simulates?

##  2 Preliminaries

We denote the set of positive integers by $\mathbb{N}^{+}$. For
$n\in\mathbb{N}^{+}$, we let $[n]\coloneqq\\{1,\dots,n\\}$. For a sequence
$S=(x_{1},\dots,x_{n})$, its length is $n$ and we denote it by $\lvert
S\rvert$. We use $\langle x\rangle$ to compactly denote an infinite sequence
$(x_{n})_{n=1}^{\infty}$.

###  2.1 Propositional logic

For notation we mostly follow Buss and Thapen [6].

We use $0$ and $1$ to denote $\mathit{False}$ and $\mathit{True}$,
respectively. A _literal_ is a propositional variable or its negation. A set
of literals is _tautological_ if it contains a pair of complementary literals
$x$ and $\overline{x}$. A _clause_ is the disjunction of a nontautological set
of literals. We denote by $\mathbf{V}$, $\mathbf{L}$, and $\mathbf{C}$
respectively the sets of all variables, all literals, and all clauses. A
_conjunctive normal form formula_ (CNF) is a conjunction of clauses. We
identify clauses with sets of literals and CNFs with sets of clauses. In the
rest of this section we use $C$, $D$ to denote clauses and $\Gamma$, $\Delta$
to denote CNFs.

When we know $C\cup D$ to be nontautological, we write it as $C\lor D$. We
write $C\mathbin{\dot{\lor}}D$ to indicate a _disjoint disjunction_ , where
$C$ and $D$ have no variables in common. We sometimes write
$\Gamma\cup\\{C\\}$ as $\Gamma\land C$.

We denote by $\operatorname{var}(\Gamma)$ the set of all the variables
occurring in $\Gamma$. We say $C$ _subsumes_ $D$, denoted $C\sqsupseteq D$, if
either $D$ is tautological or $C\subseteq D$. For CNFs, we say $\Gamma$
subsumes $\Delta$, denoted $\Gamma\sqsupseteq\Delta$, if for all $D\in\Delta$
there exists some $C\in\Gamma$ such that $C\sqsupseteq D$. We take the
disjunction of a clause and a CNF as

$C\lor\Delta\coloneqq\\{C\lor D\mid D\in\Delta\text{ and }C\cup D\text{ is
nontautological}\\}.$

We say $\Gamma$ and $\Delta$ are _equisatisfiable_ , denoted
$\Gamma\equiv_{\mathrm{sat}}\Delta$, if they are either both satisfiable or
both unsatisfiable. With respect to $\Gamma$, a clause $C$ is _redundant_ if
$\Gamma\setminus\\{C\\}\equiv_{\mathrm{sat}}\Gamma\equiv_{\mathrm{sat}}\Gamma\cup\\{C\\}$.

A _partial assignment_ $\alpha$ is a partial function
$\alpha\colon\mathbf{V}\rightharpoonup\\{0,1\\}$, which also acts on literals
by letting $\alpha(\overline{x})\coloneqq\overline{\alpha(x)}$. We identify
$\alpha$ with the set $\\{p\in\mathbf{L}\mid\alpha(p)=1\\}$, consisting of all
the literals it satisfies. For a set $L$ of literals, we let
$\overline{L}\coloneqq\\{\overline{x}\mid x\in L\\}$. In particular, we use
$\overline{C}$ to denote the smallest partial assignment that falsifies all
the literals in $C$. We say $\alpha$ _satisfies_ $C$, denoted $\alpha\models
C$, if there exists some $p\in C$ such that $\alpha(p)=1$. We say $\alpha$
satisfies $\Gamma$ if for all $C\in\Gamma$ we have $\alpha\models C$. For $C$
that $\alpha$ does not satisfy, the _restriction_ of $C$ under $\alpha$ is

$C|_{\alpha}\coloneqq C\setminus\\{p\in C\mid\alpha(p)=0\\}.$

Extending the above to CNFs, the restriction of $\Gamma$ under $\alpha$ is

$\Gamma|_{\alpha}\coloneqq\\{C|_{\alpha}\mid C\in\Gamma\text{ and
}\alpha\not\models C\\}.$

###  2.2 Proof complexity

We recall the definition of a proof system (in the sense of Cook and Reckhow
[11]) and the basic notions of proof complexity, which can also be found in
the recent textbook by Krajíček [18, Chapter 1].

In the rest of this section we think of $\Gamma$ as a formula and $\Pi$ as a
proof, each encoded by a string over some finite alphabet.

######  Definition 2.1.

A _proof system_ is a polynomial-time computable binary relation $P$ such that
the following hold.

  * •

_Soundness:_ For all $\Gamma$ and $\Pi$, if $P(\Gamma,\Pi)$ holds then
$\Gamma$ is unsatisfiable.

  * •

_Completeness:_ For all unsatisfiable $\Gamma$, there exists some $\Pi$ such
that $P(\Gamma,\Pi)$ holds.

We call any $\Pi$ satisfying $P(\Gamma,\Pi)$ a _$P$ -proof_ of $\Gamma$.

Proof complexity is concerned with the sizes (or lengths) of proofs.666The
abstract definition of proof (or formula) size is based on the length of the
string that encodes the object; however, when studying concrete proof systems
it is standard to use coarser notions of size. For a resolution proof, the
common definition of size is the number of steps. It is tacitly understood
that a minimum-size resolution proof can be encoded by a string of length
polynomial in the size of the proof. For a proof system $P$ and a formula
$\Gamma$, we define

$\operatorname{size}_{P}(\Gamma)\coloneqq\min\\{\lvert\Pi\rvert\mid\Pi\text{
is a $P$-proof of }\Gamma\\}$

if $\Gamma$ is unsatisfiable and
$\operatorname{size}_{P}(\Gamma)\coloneqq\infty$ otherwise.

######  Definition 2.2.

A proof system $P$ _simulates_ $Q$ if for all unsatisfiable $\Gamma$ we have

$\operatorname{size}_{P}(\Gamma)=\operatorname{size}_{Q}(\Gamma)^{O(1)}.$

Additionally, $P$ _polynomially simulates_ $Q$ if there exists a polynomial-
time algorithm for converting a $Q$-proof of $\Gamma$ into a $P$-proof of
$\Gamma$.

######  Definition 2.3.

Proof systems $P$ and $Q$ are _equivalent_ if they simulate each other.
Additionally, $P$ and $Q$ are _polynomially equivalent_ if they polynomially
simulate each other.

We say $P$ is _exponentially separated_ from $Q$ if there exists some sequence
$\langle\Gamma\rangle$ of formulas such that
$\operatorname{size}_{P}(\Gamma_{n})=n^{O(1)}$ while
$\operatorname{size}_{Q}(\Gamma_{n})=2^{\Omega(n)}$. We call such
$\langle\Gamma\rangle$ _easy_ for $P$ and _hard_ for $Q$.

###  2.3 Resolution

######  Definition 2.4.

The _resolution rule_ is

$A\mathbin{\dot{\lor}}x$ $B\mathbin{\dot{\lor}}\overline{x}$ $A\lor B$ ,

where $A$, $B$ are clauses and $x$ is a variable. We call $A\lor B$ the
_resolvent_ of $A\lor x$ and $B\lor\overline{x}$ on $x$.

######  Definition 2.5.

The _weakening rule_ is

$A$ $A\lor B$ ,

where $A$ and $B$ are clauses. We call $A\lor B$ a _weakening_ of $A$.

We define a resolution proof in a slightly different form than usual: as a
sequence of CNFs instead of a sequence of clauses.

######  Definition 2.6.

A _resolution proof_ of a CNF $\Gamma$ is a sequence
$\Pi=(\Gamma_{1},\dots,\Gamma_{N}$) of CNFs such that $\Gamma_{1}=\Gamma$,
$\bot\in\Gamma_{N}$, and, for all $i\in[N-1]$, we have
$\Gamma_{i+1}=\Gamma_{i}\cup\\{C\\}$, where

  * •

$C$ is a resolvent of two clauses $D,E\in\Gamma_{i}$ or

  * •

$C$ is a weakening of some clause $D\in\Gamma_{i}$.

The size of $\Pi$ is $N$.

We write $\mathsf{Res}$ to denote the resolution proof system. A well known
fact is that resolution proofs are preserved under restrictions: if
$(\Gamma_{1},\Gamma_{2},\dots,\Gamma_{N})$ is a resolution proof of $\Gamma$,
then, for every partial assignment $\alpha$, the sequence
$(\Gamma_{1}|_{\alpha},\Gamma_{2}|_{\alpha},\dots,\Gamma_{N}|_{\alpha})$
contains a resolution proof of $\Gamma|_{\alpha}$. This implies in particular
the following.

######  Lemma 2.7.

For every CNF $\Gamma$ and every partial assignment $\alpha$, we have

$\operatorname{size}_{\mathsf{Res}}(\Gamma|_{\alpha})\leq\operatorname{size}_{\mathsf{Res}}(\Gamma).$

We next define a weakened version of resolution that comes up often in the
study of decision algorithms for satisfiability.

######  Definition 2.8.

A _unit propagation proof_ is a resolution proof where each use of the
resolution rule is of the form

$A\mathbin{\dot{\lor}}x$ $\overline{x}$ $A$ .

Unit propagation is not complete. With $\Gamma$, $\Delta$ CNFs and
$L=\\{p_{1},\dots,p_{k}\\}$ a set of literals, we define
$\Gamma\land\overline{L}\coloneqq\Gamma\land\overline{p_{1}}\land\dots\land\overline{p_{k}}$
and write

  * •

$\Gamma\vdash_{1}\bot$ to denote that there exists a unit propagation proof of
$\Gamma$,

  * •

$\Gamma\vdash_{1}L$ to denote
$\left(\Gamma\land\overline{L}\right)\vdash_{1}\bot$,

  * •

$\Gamma\vdash_{1}\Delta$ to denote that for all $D\in\Delta$ we have
$\Gamma\vdash_{1}D$.

Note that $\Gamma\vdash_{1}\Delta$ implies $\Gamma\models\Delta$. Moreover,
whether $\Gamma\vdash_{1}\Delta$ holds can be decided in polynomial time. This
makes it useful as a component in defining inference rules.

As in the case of resolution, unit propagation proofs are preserved under
restrictions.

######  Lemma 2.9.

For every CNF $\Gamma$, every set $L$ of literals, and every partial
assignment $\alpha$ such that $\alpha\not\models L$, if $\Gamma\vdash_{1}L$,
then $\Gamma|_{\alpha}\vdash_{1}L|_{\alpha}$.

###### Proof.

Suppose that $\left(\Gamma\land\overline{L}\right)\vdash_{1}\bot$. Since unit
propagation proofs are preserved under restrictions, we have
$\left.\kern-1.2pt\left(\Gamma\land\overline{L}\right)\right|_{\alpha}\vdash_{1}\bot$.
Unpacking the formula on the left-hand side gives

$\Gamma|_{\alpha}\land\left(\overline{L}\setminus\alpha\right)\vdash_{1}\bot.$
(5)

(We write $\overline{L}\setminus\alpha$ instead of $\overline{L}|_{\alpha}$
since $\alpha$ may satisfy $\overline{L}$.) Noting that $\alpha\not\models L$,
we have $\overline{L}\setminus\alpha=\overline{L|_{\alpha}}$. Along with 5,
this implies that $\Gamma|_{\alpha}\vdash_{1}L|_{\alpha}$. ∎

From this point on, we discuss some strengthenings of the resolution proof
system.

######  Definition 2.10.

Let $\Gamma$ be a CNF and $p$, $q$ be arbitrary literals. Consider a _new_
variable $x$ (i.e., not occurring in any one of $\Gamma$, $p$, $q$). We call

$\\{\overline{x}\lor p,\ \overline{x}\lor q,\
x\lor\overline{p}\lor\overline{q}\\}$

a set of _extension clauses_ for $\Gamma$. In this context, we refer to $x$ as
the _extension variable_.

######  Definition 2.11.

A CNF $\Lambda$ is an _extension_ for a CNF $\Gamma$ if there exists a
sequence $(\lambda_{1},\dots,\lambda_{t})$ such that
$\Lambda=\bigcup_{i=1}^{t}\lambda_{i}$, and, for all $i\in[t]$, we have that
$\lambda_{i}$ is a set of extension clauses for
$\Gamma\cup\bigcup_{j=1}^{i-1}\lambda_{j}$.

######  Definition 2.12.

An _extended resolution proof_ of a CNF $\Gamma$ is a pair $(\Lambda,\Pi)$,
where $\Lambda$ is an extension for $\Gamma$ and $\Pi$ is a resolution proof
of $\Gamma\cup\Lambda$. The size of $(\Lambda,\Pi)$ is defined to be
$\lvert\Lambda\rvert+\lvert\Pi\rvert$.

We write $\mathsf{ER}$ to denote the extended resolution proof system.

##  3 Inference rules

We recall the redundancy criteria that lead to the inference rules we use to
augment resolution proofs. The definitions are adapted from previous works
[24, 17, 21, 15, 6].

######  Definition 3.1.

A clause $C=p\mathbin{\dot{\lor}}C^{\prime}$ is a _blocked clause_ (BC) for
$p$ with respect to a CNF $\Gamma$ if, for every clause $D$ of the form
$\overline{p}\mathbin{\dot{\lor}}D^{\prime}$ in $\Gamma$, the set
$C^{\prime}\cup D^{\prime}$ is tautological.

A strict generalization of the notion of a blocked clause is a resolution
asymmetric tautology, defined as follows.

######  Definition 3.2.

A clause $C=p\mathbin{\dot{\lor}}C^{\prime}$ is a _resolution asymmetric
tautology_ (RAT) for $p$ with respect to a CNF $\Gamma$ if, for every clause
$D$ of the form $\overline{p}\mathbin{\dot{\lor}}D^{\prime}$ in $\Gamma$, we
have $\Gamma\vdash_{1}C^{\prime}\cup D^{\prime}$.

Another strict generalization of a blocked clause is a set-blocked
clause.777We define a set-blocked clause in a slightly different, although
equivalent, way compared with the original [21, Definition 4.1].

######  Definition 3.3.

A clause $C$ is a _set-blocked clause_ (SBC) for a nonempty $L\subseteq C$
with respect to a CNF $\Gamma$ if, for every clause $D\in\Gamma$ with
$D\cap\overline{L}\neq\varnothing$ and $D\cap L=\varnothing$, the set
$\bigl{(}C\setminus L\bigr{)}\cup\bigl{(}D\setminus\overline{L}\bigr{)}$ is
tautological.

We say $C$ is a BC with respect to $\Gamma$ if there exists a literal $p\in C$
for which $C$ is a BC with respect to $\Gamma$, and similarly for RAT and SBC.
Note that the above definitions do not prohibit BCs, RATs, or SBCs with
respect to $\Gamma$ from containing variables not occurring in $\Gamma$.

It was shown by Kullmann [24], Järvisalo, Heule, and Biere [17], and Kiesl,
Seidl, Tompits, and Biere [21] that BCs, RATs, and SBCs are redundant, which
makes it possible to use them to define proof systems.

######  Theorem 3.4.

If a clause $C$ is a BC, RAT, or SBC with respect to a CNF $\Gamma$, then
$\Gamma\setminus\\{C\\}\equiv_{\mathrm{sat}}\Gamma\equiv_{\mathrm{sat}}\Gamma\cup\\{C\\}$.

######  Definition 3.5.

A _blocked clauses proof_ of a CNF $\Gamma$ is a sequence
$\Pi=(\Gamma_{1},\dots,\Gamma_{N}$) of CNFs such that $\Gamma_{1}=\Gamma$,
$\bot\in\Gamma_{N}$, and, for all $i\in[N-1]$, we have
$\Gamma_{i+1}=\Gamma_{i}\cup\\{C\\}$, where either

  * •

$C$ is a resolvent of two clauses $D,E\in\Gamma_{i}$,

  * •

$C$ is a weakening of some clause $D\in\Gamma_{i}$, or

  * •

$C$ is a blocked clause with respect to $\Gamma_{i}$.

The size of $\Pi$ is $N$.

We write $\mathsf{BC}$ to denote the blocked clauses proof system.888In some
earlier works, $\mathsf{BC}$ and its generalizations are defined as
augmentations of the _reverse unit propagation_ ($\mathsf{RUP}$) proof system
[33] instead of resolution. $\mathsf{RUP}$ has a single inference rule, which
allows adding a clause $C$ to a CNF $\Gamma$ if $\Gamma\vdash_{1}C$.
Resolution simulates $\mathsf{RUP}$ with an overhead linear in the number of
variables (by Lemma 3.16), and the main results in this paper are not affected
by the differences in the definitions. Replacing “blocked clause” by
“resolution asymmetric tautology” in the above definition gives the resolution
asymmetric tautologies proof system, which we denote by $\mathsf{RAT}$.
Replacing it by “set-blocked clause” gives the set-blocked clauses proof
system, which we denote by $\mathsf{SBC}$.

$\mathsf{RAT}$ and $\mathsf{SBC}$ are two generalizations of $\mathsf{BC}$,
and we now define another, designed to overcome the dependence of the validity
of $\mathsf{BC}$ inferences on the order of clause additions [see 24, Section
1.3].

For a CNF $\Gamma$ and a set $V$ of variables, we let

$\operatorname{\mathbf{B}}_{V}(\Gamma)\coloneqq\\{C\in\mathbf{C}\mid C\text{
is a BC for a literal of some }x\in V\text{ with respect to }\Gamma\\}.$

We also let

  * •

$\operatorname{\mathbf{B}}(\Gamma)\coloneqq\operatorname{\mathbf{B}}_{\mathbf{V}}(\Gamma)$,

  * •

$\operatorname{\operatorname{\mathbf{B}}^{\mathrm{in}}}(\Gamma)\coloneqq\operatorname{\mathbf{B}}(\Gamma)\cap\Gamma$,

  * •

$\operatorname{\mathbf{B}}^{-}_{V}(\Gamma)\coloneqq\\{C\in\operatorname{\mathbf{B}}_{V}(\Gamma)\mid\operatorname{var}(C)\subseteq\operatorname{var}(\Gamma)\\}$,

  * •

$\operatorname{\mathbf{B}}^{-}(\Gamma)\coloneqq\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\Gamma)$.

Before proceeding, we observe the below result, which follows immediately from
the definition of a blocked clause.

######  Lemma 3.6.

For all CNFs $\Gamma$ and $\Delta$ such that $\Gamma\subseteq\Delta$, we have
$\operatorname{\mathbf{B}}(\Gamma)\supseteq\operatorname{\mathbf{B}}(\Delta)$.

Thus, we may assume without loss of generality that all of the blocked clause
additions in a $\mathsf{BC}$ proof are performed before any resolution steps.
(A similar assumption does not necessarily hold for $\mathsf{RAT}$ proofs.)

######  Definition 3.7.

A sequence $(C_{1},\dots,C_{m})$ of some clauses from a CNF $\Gamma$ is a
_maximal blocked sequence_ for $\Gamma$ if

  * •

for all $i\in[m]$ the clause $C_{i}$ is blocked with respect to
$\Gamma\setminus\bigcup_{j=1}^{i-1}\\{C_{j}\\}$ and

  * •

$\mathbf{B}^{\text{in}}\left(\Gamma\setminus\bigcup_{i=1}^{m}\\{C_{i}\\}\right)$
is empty.

For a CNF $\Gamma$, a maximal blocked sequence is unique up to the ordering of
its clauses [24, Lemma 6.1], which makes the following notion well defined.

######  Definition 3.8.

Let $(C_{1},\dots,C_{m})$ be a maximal blocked sequence for a CNF $\Gamma$.
The _kernel_ of $\Gamma$ is

$\ker(\Gamma)\coloneqq\Gamma\setminus\bigcup_{i=1}^{m}\\{C_{i}\\}.$

######  Definition 3.9.

A CNF $\Lambda$ is a _blocked extension_ for a CNF $\Gamma$ if
$\ker(\Gamma\cup\Lambda)=\ker(\Gamma)$.

######  Definition 3.10.

A _generalized extended resolution proof_ of a CNF $\Gamma$ is a pair
$(\Lambda,\Pi)$, where $\Lambda$ is a blocked extension for $\Gamma$ and $\Pi$
is a resolution proof of $\Gamma\cup\Lambda$. The size of $(\Lambda,\Pi)$ is
defined to be $\lvert\Lambda\rvert+\lvert\Pi\rvert$.

We write $\mathsf{GER}$ to denote the generalized extended resolution proof
system. The relationship between $\mathsf{GER}$ and $\mathsf{BC}$ is made
clear by the following characterization of blocked extensions.

######  Lemma 3.11 ([24, Lemma 6.5]).

A CNF $\Lambda$ is a blocked extension for a CNF $\Gamma$ if and only if there
exists a CNF $\Gamma^{\prime}\subseteq\Gamma$ and an ordering
$(C_{1},\dots,C_{m})$ of all the clauses in
$\Lambda\cup(\Gamma\setminus\Gamma^{\prime})$ such that for all $i\in[m]$ the
clause $C_{i}$ is blocked with respect to
$\Gamma^{\prime}\cup\bigcup_{j=1}^{i-1}\\{C_{j}\\}$.

This result gives a view of $\mathsf{GER}$ as a version of $\mathsf{BC}$ that
allows the _temporary_ deletion of clauses from the initial formula (i.e.,
clauses can be deleted as long as they are added back later).

In this paper, we study the variants of $\mathsf{BC}$, $\mathsf{RAT}$,
$\mathsf{SBC}$, and $\mathsf{GER}$ that disallow the use of new variables. We
say that a proof of a CNF $\Gamma$ is _without new variables_ if all the
variables occurring in the proof are in $\operatorname{var}(\Gamma)$. In the
case of $\mathsf{GER}$, this constraint applies to the blocked extension. We
use $\mathsf{BC}^{-}$, $\mathsf{RAT}^{-}$, $\mathsf{SBC}^{-}$, and
$\mathsf{GER}^{-}$ to denote the variants without new variables.

###  3.1 Useful facts

We conclude this section with a few standalone results that we will refer back
to later.

######  Lemma 3.12.

For every CNF $\Gamma$ such that $\ker(\Gamma)=\Gamma$, we have

$\operatorname{size}_{\mathsf{GER}^{-}}(\Gamma)=\operatorname{size}_{\mathsf{BC}^{-}}(\Gamma).$

###### Proof.

Since $\mathsf{GER}^{-}$ is a generalization of $\mathsf{BC}^{-}$, the
inequality
$\operatorname{size}_{\mathsf{GER}^{-}}(\Gamma)\leq\operatorname{size}_{\mathsf{BC}^{-}}(\Gamma)$
immediately holds for all $\Gamma$. For the other direction, suppose that
$\ker(\Gamma)=\Gamma$ and that $\Lambda$ is a blocked extension for $\Gamma$.
We claim that the clauses in $\Lambda$ can be derived in sequence from
$\Gamma$ in $\mathsf{BC}^{-}$. By the definition of a blocked extension, we
have $\ker(\Gamma\cup\Lambda)=\ker(\Gamma)=\Gamma$. Then, by the definition of
a kernel, we can order the clauses in $\Lambda$ into a maximal blocked
sequence $(C_{1},\dots,C_{m})$ for $\Gamma$. Finally, we can derive these
clauses from $\Gamma$ in the reverse order $(C_{m},\dots,C_{1})$ by a sequence
of blocked clause additions. ∎

######  Lemma 3.13.

For every CNF $\Gamma$, we have

$\operatorname{size}_{\mathsf{BC}^{-}}(\Gamma)\geq\operatorname{size}_{\mathsf{Res}}(\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma)).$

###### Proof.

Let $\Pi$ be a $\mathsf{BC}^{-}$ proof of $\Gamma$, and let $\beta$ be the set
of blocked clauses added in $\Pi$. Due to Lemma 3.6, we can rearrange $\Pi$ as
a resolution proof of $\Gamma\cup\beta$. Then, since adding clauses to a CNF
cannot increase the size of its shortest resolution proof, and since
$\beta\subseteq\operatorname{\mathbf{B}}^{-}(\Gamma)$, the result follows. ∎

######  Definition 3.14.

The _projection_ of a CNF $\Gamma$ onto a literal $p$ is the CNF

$\operatorname{proj}_{p}(\Gamma)\coloneqq\\{C\setminus\\{p\\}\mid
C\in\Gamma\text{ and }p\in C\\}.$

This definition plays a role in both our (partial) simulation of
$\mathsf{RAT}^{-}$ by $\mathsf{BC}^{-}$ and our $\mathsf{GER}^{-}$ lower
bounds. In particular, we use the following fact, which was already observed
by Kullmann [see 24, Section 4].

######  Lemma 3.15.

A clause $C=p\mathbin{\dot{\lor}}C^{\prime}$ is a BC for $p$ with respect to a
CNF $\Gamma$ if and only if the partial assignment $\overline{C^{\prime}}$
satisfies $\operatorname{proj}_{\overline{p}}(\Gamma)$.

###### Proof.

By the definition of a blocked clause, a clause
$C=p\mathbin{\dot{\lor}}C^{\prime}$ is a BC for $p$ with respect to $\Gamma$
if and only if for all $D\in\operatorname{proj}_{\overline{p}}(\Gamma)$ the
set $C^{\prime}\cup D$ is tautological. Since neither of $C^{\prime}$ and $D$
is tautological, $C^{\prime}\cup D$ is tautological if and only if
$\overline{C^{\prime}}\cap D\neq\varnothing$, which is equivalent to
$\overline{C^{\prime}}\models D$. ∎

The next result is essentially due to Chang [9, Theorem 1]. Although its
original form is slightly weaker, the exact statement below can be obtained by
a modification of Chang’s proof. We provide its proof in Appendix A for the
sake of completeness.

######  Lemma 3.16.

For every CNF $\Gamma$ and every clause $C$ such that $\Gamma\vdash_{1}C$,
there exists a resolution derivation $(\Gamma_{1},\dots,\Gamma_{N})$ with
$N\leq\lvert\operatorname{var}(\Gamma)\rvert+1$ such that $\Gamma_{1}=\Gamma$,
$C\in\Gamma_{N}$, and $\Gamma\cup\\{C\\}\sqsupseteq\Gamma_{N}$.

The following gives a simple condition under which we regain monotonicity.

######  Lemma 3.17 ([6, Lemma 1.20]).

Let $\Gamma$ and $\Delta$ be CNFs such that $\Gamma\subseteq\Delta$ and
$\Gamma\sqsupseteq\Delta$. If a clause is a BC, RAT, or SBC with respect to
$\Gamma$, then it is a BC, RAT, or SBC with respect to $\Delta$.

##  4 Partial simulation of $\mathsf{RAT}^{-}$ by $\mathsf{BC}^{-}$

We will show how to convert a RAT addition into a sequence of BC additions and
resolution steps. Assume that all the BCs and RATs in this section are without
new variables.

######  Definition 4.1.

The _nonblocking CNF_ of a clause $C$ for a literal $p\in C$ with respect to a
CNF $\Gamma$ is

$\operatorname{NB}^{\Gamma}_{p}(C)\coloneqq\left\\{D\setminus
C\mathrel{}\middle|\mathrel{}D\in\operatorname{proj}_{\overline{p}}(\Gamma)\text{
and }(C\setminus\\{p\\})\cup D\text{ is nontautological}\right\\}.$

As a consequence of the above definition, we have
$\operatorname{var}\left(\operatorname{NB}^{\Gamma}_{p}(C)\right)\cap\operatorname{var}(C)=\varnothing$.

We say an assignment $\alpha$ _minimally satisfies_ a CNF $\Gamma$, denoted
$\alpha\models_{\mathrm{min}}\Gamma$, if $\alpha$ satisfies $\Gamma$ while no
proper subset $\alpha^{\prime}\subsetneq\alpha$ satisfies $\Gamma$. We let

$\mu(\Gamma)\coloneqq\left\\{E\in\mathbf{C}\mathrel{}\middle|\mathrel{}\overline{E}\models_{\mathrm{min}}\Gamma\right\\}.$

Since two different minimally satisfying assignments cannot contain one
another, no clause $E\in\mu(\Gamma)$ is contained in a different clause
$E^{\prime}\in\mu(\Gamma)$.

######  Example 4.2.

Let $\Gamma=\\{x,\ y\lor\overline{z}\\}$. This CNF has two minimally
satisfying assignments: $\\{x,\,y\\}$ and $\\{x,\,\overline{z}\\}$. We thus
have $\mu(\Gamma)=\\{\overline{x}\lor\overline{y},\ \overline{x}\lor z\\}$.

Noting that $\Gamma\cup\mu(\Gamma)$ is unsatisfiable for every CNF $\Gamma$,
we let

$s(\Gamma)\coloneqq\lvert\mu(\Gamma)\rvert+\operatorname{size}_{\mathsf{Res}}(\Gamma\cup\mu(\Gamma)).$

When $\Gamma$ is unsatisfiable, we simply have
$s(\Gamma)=\operatorname{size}_{\mathsf{Res}}(\Gamma)$.

######  Theorem 4.3.

Let $C=p\mathbin{\dot{\lor}}C^{\prime}$ be a RAT for $p$ with respect to a CNF
$\Gamma$. There exists a $\mathsf{BC}^{-}$ derivation
$(\Gamma_{1},\dots,\Gamma_{N})$ such that $\Gamma_{1}=\Gamma$,
$C\in\Gamma_{N}$, and $\Gamma\cup\\{C\\}\sqsupseteq\Gamma_{N}$, where, letting
$\Sigma=\operatorname{NB}^{\Gamma}_{p}(C)$ and letting
$n=\lvert\operatorname{var}(\Gamma)\rvert$, we have

$N\leq\lvert\Sigma\rvert(n+1)+s(\Sigma).$

###### Proof.

Since $C$ is a RAT for $p$, for all $D\in\operatorname{NB}^{\Gamma}_{p}(C)$ we
have $\Gamma\vdash_{1}C^{\prime}\mathbin{\dot{\lor}}D$, which implies in
particular that $\Gamma\vdash_{1}C\mathbin{\dot{\lor}}D$. Then, using Lemma
3.16, for all $D\in\operatorname{NB}^{\Gamma}_{p}(C)$ we derive
$C\mathbin{\dot{\lor}}D$ from $\Gamma$ in resolution using at most $n+1$
steps. More formally, we derive
$\Gamma^{\prime}\cup\left(C\mathbin{\dot{\lor}}\operatorname{NB}^{\Gamma}_{p}(C)\right)$
from $\Gamma$, where $\Gamma^{\prime}$ is the set of intermediate clauses,
guaranteed by Lemma 3.16 to satisfy $\\{C\\}\sqsupseteq\Gamma^{\prime}$.

We proceed differently depending on the satisfiability of
$\operatorname{NB}^{\Gamma}_{p}(C)$.

Case 1

($\operatorname{NB}^{\Gamma}_{p}(C)$ is unsatisfiable.) There exists a
resolution proof

$\Pi=(\Delta_{1},\dots,\Delta_{m}),$

where $\Delta_{1}=\operatorname{NB}^{\Gamma}_{p}(C)$ and $\bot\in\Delta_{m}$.
Suppose $\Pi$ is a minimum-size proof, so it does not use weakening. Consider
the sequence

$\Pi^{\prime}=(C\lor\Delta_{1},\dots,C\lor\Delta_{m}).$

This sequence is a valid resolution derivation of $C$ from
$C\mathbin{\dot{\lor}}\operatorname{NB}^{\Gamma}_{p}(C)$, seen as follows:

  * •

By the definition of $\operatorname{NB}^{\Gamma}_{p}(C)$, it has no variables
in common with $C$. Since we assumed that $\Pi$ does not use weakening, no
subsequent CNF in $\Pi$ has any variables in common with $C$ either.

Let $i\in[m-1]$. The sequence $\Pi$ is a resolution proof, so we have
$\Delta_{i+1}=\Delta_{i}\cup\\{E\\}$, where $E$ is a resolvent of some
$F,G\in\Delta_{i}$. Since $\Delta_{i}$ has no variables in common with $C$, it
is not possible to resolve $F$ and $G$ on a variable of $C$. Then the clause
$C\mathbin{\dot{\lor}}E$ is a resolvent of $C\mathbin{\dot{\lor}}F$ and
$C\mathbin{\dot{\lor}}G$, which are in $C\lor\Delta_{i}$. This proves by
induction that $\Pi^{\prime}$ is a valid resolution derivation.

  * •

Finally, since $\bot\in\Delta_{m}$, we have $C\in(C\lor\Delta_{m})$.

Thus, resolution can derive $C$ from $\Gamma$ in at most
$\left\lvert\operatorname{NB}^{\Gamma}_{p}(C)\right\rvert(n+1)+\operatorname{size}_{\mathsf{Res}}\left(\operatorname{NB}^{\Gamma}_{p}(C)\right)$
steps.

Case 2

($\operatorname{NB}^{\Gamma}_{p}(C)$ is satisfiable.) Let
$\Psi=\Gamma\cup\Gamma^{\prime}\cup\left(C\mathbin{\dot{\lor}}\operatorname{NB}^{\Gamma}_{p}(C)\right)$
(i.e., the current CNF). Since $C\sqsupseteq(\Psi\setminus\Gamma)$, the
literal $\overline{p}$ does not occur in $\Psi\setminus\Gamma$. Then we have
$\operatorname{proj}_{\overline{p}}(\Psi)=\operatorname{proj}_{\overline{p}}(\Gamma)$,
and, consequently,
$\operatorname{NB}^{\Psi}_{p}(C)=\operatorname{NB}^{\Gamma}_{p}(C)$.

Let $E$ be a clause such that
$\operatorname{var}(E)\cap\operatorname{var}(C)=\varnothing$. By Lemma 3.15,
the clause $p\mathbin{\dot{\lor}}C^{\prime}\mathbin{\dot{\lor}}E$ is a BC for
$p$ with respect to $\Psi$ if and only if the partial assignment
$\overline{C^{\prime}\mathbin{\dot{\lor}}E}$ satisfies
$\operatorname{proj}_{\overline{p}}(\Psi)$. By the definition of a nonblocking
CNF, $\overline{C^{\prime}}$ already satisfies
$\operatorname{proj}_{\overline{p}}(\Psi)\setminus\operatorname{NB}^{\Psi}_{p}(C)$,
so $p\mathbin{\dot{\lor}}C^{\prime}\mathbin{\dot{\lor}}E$ is a BC for $p$ with
respect to $\Psi$ if and only if $\overline{E}$ satisfies
$\operatorname{NB}^{\Psi}_{p}(C)$.

Let us write $\mu$ for $\mu\left(\operatorname{NB}^{\Psi}_{p}(C)\right)$. All
clauses in $C\mathbin{\dot{\lor}}\mu$ are blocked for $p$ with respect to
$\Psi$, and the addition of each such clause of the form
$C\mathbin{\dot{\lor}}E$ rules out, for
$C\mathbin{\dot{\lor}}\operatorname{NB}^{\Psi}_{p}(C)$, every partial
assignment $\alpha$ containing $\overline{C\cup E}$. Then we have

$\left(C\mathbin{\dot{\lor}}\operatorname{NB}^{\Psi}_{p}(C)\right)\cup(C\mathbin{\dot{\lor}}\mu)\models
C,$

where every partial assignment containing $\overline{C}$ falsifies the left-
hand side (i.e., $\operatorname{NB}^{\Psi}_{p}(C)\cup\mu$ is unsatisfiable).
Also, no clause $E\in\mu$ contains $\overline{p}$ and no clause $E\in\mu$ is a
subset of a different clause $E^{\prime}\in\mu$. This implies in particular
that, for every subset $\mu^{\prime}\subseteq\mu$ and for every clause
$E\in\mu\setminus\mu^{\prime}$, if
$\overline{E}\models\operatorname{NB}^{\Psi}_{p}(C)$, then
$\overline{E}\models\operatorname{NB}^{\Psi}_{p}(C)\cup\mu^{\prime}$. We thus
derive $C\mathbin{\dot{\lor}}\mu$ from $\Psi$ by a sequence of blocked clause
additions.

As in the previous case, attaching $C$ to a resolution proof of
$\operatorname{NB}^{\Psi}_{p}(C)\cup\mu$ gives a resolution derivation of $C$,
so we derive $C$ from
$\left(C\mathbin{\dot{\lor}}\operatorname{NB}^{\Psi}_{p}(C)\right)\cup(C\mathbin{\dot{\lor}}\mu)$
in resolution.

In the end, $\mathsf{BC}^{-}$ can derive $C$ from $\Gamma$ in at most

$\left\lvert\operatorname{NB}^{\Gamma}_{p}(C)\right\rvert(n+1)+\lvert\mu\rvert+\operatorname{size}_{\mathsf{Res}}\left(\operatorname{NB}^{\Gamma}_{p}(C)\cup\mu\right)$

steps. ∎

Given a $\mathsf{RAT}^{-}$ proof, we can apply the above theorem to
recursively replace the earliest RAT addition in the proof by a
$\mathsf{BC}^{-}$ derivation. The intermediate clauses in the derivation
replacing the addition of a RAT $C$ are all subsumed by $C$, which ensures by
Lemma 3.17 that the validity of later RAT additions are preserved. We can thus
translate an entire $\mathsf{RAT}^{-}$ proof to a $\mathsf{BC}^{-}$ proof.

In the above simulation, when $\operatorname{NB}^{\Gamma}_{p}(C)$ is
unsatisfiable, we do not use any blocked clause additions. By Lemma 3.15, no
blocked clause for $p$ exists, and since the RAT addition by itself only gives
useful information about the clauses containing $\overline{p}$, a simulation
where we add a clause that is blocked for a different literal needs to be more
sophisticated. In particular, such a simulation is unlikely to be _local_ in
the sense of the output consisting of a sequence of derivations that each
simulate a single step in the input. (Most simulations in proof complexity are
local.) Assuming that the above simulation is the best possible, if every RAT
addition in a $\mathsf{RAT}^{-}$ proof $\Pi$ has an unsatisfiable nonblocking
CNF, then $\mathsf{BC}^{-}$ essentially falls back to refuting the nonblocking
CNFs for locally simulating $\Pi$. This observation hints at the
transformation in 6 for separating $\mathsf{RAT}^{-}$ from $\mathsf{GER}^{-}$.

##  5 Incomparability of $\mathsf{RAT}^{-}$ and $\mathsf{GER}^{-}$

We now show that $\mathsf{RAT}^{-}$ is exponentially separated from
$\mathsf{GER}^{-}$ and vice versa, which also exponentially separates both
systems from $\mathsf{BC}^{-}$. For both directions, we follow a strategy
similar at a high level to the one that Kullmann [24, Lemma 8.4] used to prove
an exponential separation of $\mathsf{BC}^{-}$ from resolution.

Let $P$ and $Q$ be proof systems (without new variables) that simulate
$\mathsf{BC}^{-}$. To separate $P$ from $Q$, we take a sequence
$\langle\Gamma\rangle$ of CNFs separating $\mathsf{ER}$ from $Q$ and we
incorporate extension variables into the formulas in a way that allows $P$ to
simulate the $\mathsf{ER}$ proof while preventing $Q$ from achieving any
speedup. This strategy is made possible by the fact that $\mathsf{BC}^{-}$
effectively simulates $\mathsf{ER}$. See also the discussion by Buss and
Thapen [6, Section 2.2].

From this point on, given a CNF $\Gamma$, we use $(\Lambda^{*},\Pi^{*})$ to
denote a minimum-size $\mathsf{ER}$ proof of $\Gamma$, where $\Lambda^{*}$ is
the union of a sequence of $t(\Gamma)\coloneqq\lvert\Lambda^{*}\rvert/3$ sets
of extension clauses such that the $i$th set $\lambda_{i}$ is of the form

$\\{\overline{x_{i}}\lor p_{i},\ \overline{x_{i}}\lor q_{i},\
x_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}\\}.$

Thus, we implicitly reserve $\left\\{x_{1},\dots,x_{t(\Gamma)}\right\\}$ as
the set of extension variables used in $\Lambda^{*}$. We assume without loss
of generality that the variables of $p_{i}$ and $q_{i}$ are in
$\operatorname{var}(\Gamma)\cup\\{x_{1},\dots,x_{i-1}\\}$ for all
$i\in[t(\Gamma)]$.

###  5.1 Exponential separation of $\mathsf{RAT}^{-}$ from $\mathsf{GER}^{-}$

Let $\Gamma$ be a CNF and $(\Lambda^{*},\Pi^{*})$ be a minimum-size
$\mathsf{ER}$ proof of $\Gamma$ as described above. Consider the
transformation

$\mathcal{G}(\Gamma)\coloneqq\Gamma\cup\bigcup_{i=1}^{t(\Gamma)}\bigl{[}(x_{i}\lor\Gamma)\cup(\overline{x_{i}}\lor\Gamma)\bigr{]},$
(6)

where $x_{1},\dots,x_{t(\Gamma)}$ are the extension variables used in
$\Lambda^{*}$. When $\Gamma$ is unsatisfiable, each extension variable above
is “locked” behind the projection $\Gamma$, which $\mathsf{RAT}^{-}$ can
overcome but $\mathsf{BC}^{-}$ cannot.

######  Lemma 5.1.

For every CNF $\Gamma$, we have

$\operatorname{size}_{\mathsf{RAT}^{-}}(\mathcal{G}(\Gamma))\leq\operatorname{size}_{\mathsf{ER}}(\Gamma).$

###### Proof.

We will show that the minimum-size $\mathsf{ER}$ proof $(\Lambda^{*},\Pi^{*})$
of $\Gamma$ directly gives a $\mathsf{RAT}^{-}$ proof of $\mathcal{G}(\Gamma)$
of the same size.

We write $t$ for $t(\Gamma)$. Let $(\lambda_{1},\dots,\lambda_{t})$ be the
sequence of $t$ sets of extension clauses that make up $\Lambda^{*}$. Consider
an arbitrary $i\in[t]$, and suppose that we have derived
$\bigcup_{j=1}^{i-1}\lambda_{j}$ from $\mathcal{G}(\Gamma)$ by a sequence of
RAT additions, so the current CNF is
$\Delta=\mathcal{G}(\Gamma)\cup\bigcup_{j=1}^{i-1}\lambda_{j}$. We will
introduce the clauses in

$\lambda_{i}=\\{\overline{x_{i}}\lor p_{i},\ \overline{x_{i}}\lor q_{i},\
x_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}\\}$

by a sequence of RAT additions. Note that, since $\lambda_{i}$ is a set of
extension clauses for $\Gamma\cup\bigcup_{j=1}^{i-1}\lambda_{j}$, so far the
variable $x_{i}$ occurs only in $\mathcal{G}(\Gamma)\setminus\Gamma$.

  1. 1.

The clause $\overline{x_{i}}\lor p_{i}$ is a RAT for $\overline{x_{i}}$ with
respect to $\Delta$ because all earlier occurrences of $x_{i}$ are clauses of
the form $x_{i}\lor D$, where $D\in\Gamma$. We thus require
$\Delta\vdash_{1}\\{p_{i}\\}\cup D$ for all $D\in\Gamma$. This is indeed the
case since we actually have $D\in\Delta$ by the construction of
$\mathcal{G}(\Gamma)$, which implies $\Delta\vdash_{1}\\{p_{i}\\}\cup D$.

  2. 2.

The clause $\overline{x_{i}}\lor q_{i}$ is similarly a RAT for
$\overline{x_{i}}$ with respect to $\Delta\cup\\{\overline{x_{i}}\lor
p_{i}\\}$.

  3. 3.

The clause $x_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}$ is similarly a RAT
for $x_{i}$ with respect to $\Delta$. Moreover, it is a BC for $x_{i}$ with
respect to $\\{\overline{x_{i}}\lor p_{i},\ \overline{x_{i}}\lor q_{i}\\}$
since $\\{p_{i},\,\overline{p_{i}},\,\overline{q_{i}}\\}$ and
$\\{q_{i},\,\overline{p_{i}},\,\overline{q_{i}}\\}$ are both tautological. As
a result, $x_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}$ is a RAT with
respect to $\Delta\cup\\{\overline{x_{i}}\lor p_{i},\ \overline{x_{i}}\lor
q_{i}\\}$.

It follows by induction that we can derive $\Lambda^{*}$ from
$\mathcal{G}(\Gamma)$ in $\mathsf{RAT}^{-}$. Since $\Pi^{*}$ is a resolution
proof of $\Gamma\cup\Lambda^{*}$, and since $\mathcal{G}(\Gamma)$ contains
$\Gamma$, we also have a resolution proof of
$\mathcal{G}(\Gamma)\cup\Lambda^{*}$. Thus, we have a $\mathsf{RAT}^{-}$ proof
of $\mathcal{G}(\Gamma)$ of size
$\lvert\Lambda^{*}\rvert+\lvert\Pi^{*}\rvert=\operatorname{size}_{\mathsf{ER}}(\Gamma)$.
∎

As a consequence of the above, if a sequence $\langle\Gamma\rangle$ of CNFs is
easy for $\mathsf{ER}$, then, independent of whether $\langle\Gamma\rangle$ is
easy or hard for $\mathsf{RAT}^{-}$, the sequence
$\mathcal{G}(\langle\Gamma\rangle)\coloneqq(\mathcal{G}(\Gamma_{1}),\mathcal{G}(\Gamma_{2}),\dots)$
is easy for $\mathsf{RAT}^{-}$. In contrast, the following result implies that
the extension variables added by $\mathcal{G}$ are of no use to
$\mathsf{BC}^{-}$.

######  Lemma 5.2.

For every CNF $\Gamma$, we have

$\operatorname{size}_{\mathsf{BC}^{-}}(\mathcal{G}(\Gamma))\geq\operatorname{size}_{\mathsf{Res}}(\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma)).$

###### Proof.

When $\Gamma$ is satisfiable, the inequality holds trivially, so suppose that
$\Gamma$ is unsatisfiable.

Applying Lemma 3.13 to $\mathcal{G}(\Gamma)$, we have

$\operatorname{size}_{\mathsf{BC}^{-}}(\mathcal{G}(\Gamma))\geq\operatorname{size}_{\mathsf{Res}}\left(\mathcal{G}(\Gamma)\cup\operatorname{\mathbf{B}}^{-}(\mathcal{G}(\Gamma))\right).$
(7)

We claim that no clause in
$\operatorname{\mathbf{B}}^{-}(\mathcal{G}(\Gamma))$ is blocked for a literal
of any of the variables in $X=\left\\{x_{1},\dots,x_{t(\Gamma)}\right\\}$. To
see this, consider a clause $C$ of the form $x\mathbin{\dot{\lor}}C^{\prime}$,
where $x\in X$. If $C$ is blocked for $x$ with respect to
$\mathcal{G}(\Gamma)$, then $\overline{C^{\prime}}$ is a satisfying assignment
to $\operatorname{proj}_{\overline{x}}(\mathcal{G}(\Gamma))=\Gamma$ by Lemma
3.15. Since $\Gamma$ is unsatisfiable, no such assignment exists. Therefore,
$C$ cannot be blocked for $x$, which leaves us with

$\operatorname{\mathbf{B}}^{-}(\mathcal{G}(\Gamma))=\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma)).$
(8)

Furthermore, since $\Gamma\subseteq\mathcal{G}(\Gamma)$, every clause in
$\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))$
has to be blocked in particular with respect to $\Gamma$. This requires
$\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))$
to consist of clauses of the form $C\mathbin{\dot{\lor}}D$, where
$C\in\operatorname{\mathbf{B}}^{-}(\Gamma)$ and
$\operatorname{var}(D)\subseteq X$ (with $D$ possibly empty). In light of
this, consider a partial assignment $\alpha$ such that

$\alpha(z)=\begin{cases}1&\text{if }z\in X\\\
\text{undefined}&\text{otherwise}.\end{cases}$

It is straightforward to see that $\mathcal{G}(\Gamma)|_{\alpha}=\Gamma$.
Additionally, for every clause $C\mathbin{\dot{\lor}}D$ (of the above form) in
$\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))$,
the restriction $(C\mathbin{\dot{\lor}}D)|_{\alpha}$ is either $1$ or $C$. We
thus have

$\left.\kern-1.2pt\left(\mathcal{G}(\Gamma)\cup\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))\right)\right|_{\alpha}=\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma).$
(9)

Putting 7, LABEL:, 8, LABEL:, and 9 together, we finally obtain

$\displaystyle\operatorname{size}_{\mathsf{BC}^{-}}(\mathcal{G}(\Gamma))$
$\displaystyle\geq\operatorname{size}_{\mathsf{Res}}\left(\mathcal{G}(\Gamma)\cup\operatorname{\mathbf{B}}^{-}(\mathcal{G}(\Gamma))\right)$
$\displaystyle=\operatorname{size}_{\mathsf{Res}}\left(\mathcal{G}(\Gamma)\cup\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))\right)$
$\displaystyle\geq\operatorname{size}_{\mathsf{Res}}\left(\left.\kern-1.2pt\left(\mathcal{G}(\Gamma)\cup\operatorname{\mathbf{B}}^{-}_{\operatorname{var}(\Gamma)}(\mathcal{G}(\Gamma))\right)\right|_{\alpha}\right)$
(Lemma 2.7)
$\displaystyle=\operatorname{size}_{\mathsf{Res}}\left(\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma)\right),$

which is the desired inequality. ∎

For certain CNFs, the above result carries over to $\mathsf{GER}^{-}$.

######  Lemma 5.3.

For every CNF $\Gamma$ such that $\ker(\Gamma)=\Gamma$, we have

$\operatorname{size}_{\mathsf{GER}^{-}}(\mathcal{G}(\Gamma))\geq\operatorname{size}_{\mathsf{Res}}(\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma)).$

###### Proof.

Suppose $\ker(\Gamma)=\Gamma$. We will show that
$\operatorname{\operatorname{\mathbf{B}}^{\mathrm{in}}}(\mathcal{G}(\Gamma))=\varnothing$.
A clause $C$ in
$\operatorname{\operatorname{\mathbf{B}}^{\mathrm{in}}}(\mathcal{G}(\Gamma))$
belongs to either $\Gamma$ or $\mathcal{G}(\Gamma)\setminus\Gamma$, and we
handle the two cases separately.

Case 1

($C\in\Gamma$.) If $C$ is blocked with respect to $\mathcal{G}(\Gamma)$, then,
since $\Gamma\subseteq\mathcal{G}(\Gamma)$, it is blocked with respect to
$\Gamma$ as well, which contradicts $\ker(\Gamma)=\Gamma$.

Case 2

($C\in\mathcal{G}(\Gamma)\setminus\Gamma$.) Since
$C\in\mathcal{G}(\Gamma)\setminus\Gamma$, it is of the form
$p\mathbin{\dot{\lor}}C^{\prime}$, where $C^{\prime}\in\Gamma$ and $p$ is a
literal of some variable in $\left\\{x_{1},\dots,x_{t(\Gamma)}\right\\}$. The
clause $C$ is clearly not blocked for $p$ with respect to
$\mathcal{G}(\Gamma)$ since there exists a clause of the form
$\overline{p}\mathbin{\dot{\lor}}C^{\prime}$ in $\mathcal{G}(\Gamma)$ but
$C^{\prime}\cup C^{\prime}$ is not tautological. The clause $C$ is not blocked
for any literal in $C^{\prime}$ with respect to $\mathcal{G}(\Gamma)$ either
since this implies that $C^{\prime}$ is blocked with respect to $\Gamma$,
which contradicts $\ker(\Gamma)=\Gamma$.

We thus have $\ker(\mathcal{G}(\Gamma))=\mathcal{G}(\Gamma)$. Now, using
Lemmas 3.12 and 5.2, we have

$\operatorname{size}_{\mathsf{GER}^{-}}(\mathcal{G}(\Gamma))=\operatorname{size}_{\mathsf{BC}^{-}}(\mathcal{G}(\Gamma))\geq\operatorname{size}_{\mathsf{Res}}(\Gamma\cup\operatorname{\mathbf{B}}^{-}(\Gamma)).\qed$

To prove the separation, we invoke the above results with $\Gamma$ as the
_pigeonhole principle_ , which states that every “pigeon” $i\in[n+1]$ is
mapped to some “hole” $k\in[n]$ and that no two distinct pigeons $i,j\in[n+1]$
are mapped to the same hole. It is defined for $n\in\mathbb{N}^{+}$ as

$\mathrm{PHP}_{n}\coloneqq\bigcup_{i\in[n+1]}\left\\{p_{i,1}\lor\dots\lor
p_{i,n}\right\\}\cup\bigcup_{\begin{subarray}{c}i,j\in[n+1],\;i\neq j\\\
k\in[n]\end{subarray}}\\{\overline{p_{i,k}}\lor\overline{p_{j,k}}\\},$

where we call the first set of clauses the _pigeon axioms_ and the second set
the _hole axioms_.

######  Theorem 5.4.

$\mathsf{RAT}^{-}$ is exponentially separated from $\mathsf{GER}^{-}$.

###### Proof.

Cook [10] constructed polynomial-size $\mathsf{ER}$ proofs of
$\mathrm{PHP}_{n}$, which implies by Lemma 5.1 that

$\operatorname{size}_{\mathsf{RAT}^{-}}(\mathcal{G}(\mathrm{PHP}_{n}))=n^{O(1)}.$

Kullmann [24, Theorem 2] proved that
$\operatorname{size}_{\mathsf{Res}}(\mathrm{PHP}_{n}\cup\operatorname{\mathbf{B}}^{-}(\mathrm{PHP}_{n}))=2^{\Omega(n)}$.
Noting that $\ker(\mathrm{PHP}_{n})=\mathrm{PHP}_{n}$ for all
$n\in\mathbb{N}^{+}$, we apply Lemma 5.3 to obtain

$\operatorname{size}_{\mathsf{GER}^{-}}(\mathcal{G}(\mathrm{PHP}_{n}))=2^{\Omega(n)}.$

Thus, $\mathcal{G}(\langle\mathrm{PHP}\rangle)$ exponentially separates
$\mathsf{RAT}^{-}$ from $\mathsf{GER}^{-}$. ∎

###  5.2 Exponential separation of $\mathsf{GER}^{-}$ from $\mathsf{RAT}^{-}$

We proceed in a similar way to the previous section. Let $\Gamma$ be a CNF and
$(\Lambda^{*},\Pi^{*})$ be a minimum-size $\mathsf{ER}$ proof of $\Gamma$.
Take a set

$\left\\{y_{1},\dots,y_{t(\Gamma)}\right\\}\subseteq\mathbf{V}\setminus\operatorname{var}(\Gamma\cup\Lambda^{*})$

of $t(\Gamma)$ distinct variables. Consider the transformation

$\mathcal{H}(\Gamma)\coloneqq\Gamma\cup\bigcup_{i=1}^{t(\Gamma)}\\{\overline{x_{i}}\lor
y_{i},\ x_{i}\lor\overline{y_{i}}\\},$ (10)

where $x_{1},\dots,x_{t(\Gamma)}$ are the extension variables used in
$\Lambda^{*}$. As before, only one of the two systems can make any use of the
extension variables incorporated into the formula. This time, the temporary
deletion available to $\mathsf{GER}^{-}$ makes the difference.

######  Lemma 5.5.

For every CNF $\Gamma$, we have

$\operatorname{size}_{\mathsf{GER}^{-}}(\mathcal{H}(\Gamma))\leq\operatorname{size}_{\mathsf{ER}}(\Gamma).$

###### Proof.

Let $(\Lambda^{*},\Pi^{*})$ be the minimum-size $\mathsf{ER}$ proof of
$\Gamma$. We will show that the clauses in
$\Lambda^{*}\cup(\mathcal{H}(\Gamma)\setminus\Gamma)$ can be derived from
$\Gamma$ in some sequence by blocked clause additions, which implies by Lemma
3.11 that $\Lambda^{*}$ is a blocked extension for $\mathcal{H}(\Gamma)$.

Recall that extension clauses can be derived in sequence by blocked clause
additions. Then, since $\Lambda^{*}$ is an extension for $\Gamma$, we derive
$\Lambda^{*}$ by such a sequence. Next, from $\Gamma\cup\Lambda^{*}$, we
derive the clauses in $\mathcal{H}(\Gamma)\setminus\Gamma$. Let us write $t$
for $t(\Gamma)$. Consider the sequence

$(\overline{x_{1}}\lor y_{1},\ \dots,\ \overline{x_{t}}\lor y_{t},\
x_{1}\lor\overline{y_{1}},\ \dots,\ x_{t}\lor\overline{y_{t}}).$

For each $i\in[t]$, the $i$th clause $\overline{x_{i}}\lor y_{i}$ in the first
half of the sequence is blocked for $y_{i}$ since $\overline{y_{i}}$ does not
occur in any of the earlier clauses. Similarly, the $i$th clause
$x_{i}\lor\overline{y_{i}}$ in the second half of the sequence is blocked for
$\overline{y_{i}}$ since the only earlier occurrence of $y_{i}$ is the clause
$\overline{x_{i}}\lor y_{i}$ and $\\{x_{i},\,\overline{x_{i}}\\}$ is
tautological. As a result, $\Lambda^{*}$ is a blocked extension for
$\mathcal{H}(\Gamma)$.

Since $\Pi^{*}$ is a resolution proof of $\Gamma\cup\Lambda^{*}$, and since
$\mathcal{H}(\Gamma)$ contains $\Gamma$, we also have a resolution proof of
$\mathcal{H}(\Gamma)\cup\Lambda^{*}$. Thus, we have a $\mathsf{GER}^{-}$ proof
of $\mathcal{H}(\Gamma)$ of size
$\lvert\Lambda^{*}\rvert+\lvert\Pi^{*}\rvert=\operatorname{size}_{\mathsf{ER}}(\Gamma)$.
∎

######  Lemma 5.6.

Let $\Gamma$ be a CNF, and let $n=\lvert\operatorname{var}(\Gamma)\rvert$. We
have

$\operatorname{size}_{\mathsf{RAT}^{-}}(\mathcal{H}(\Gamma))\geq\frac{\operatorname{size}_{\mathsf{RAT}^{-}}(\Gamma)}{n+1}.$

###### Proof.

We write $t$ for $t(\Gamma)$. Let
$V=\operatorname{var}(\mathcal{H}(\Gamma)\setminus\Gamma)$ (i.e., the set of
variables added by $\mathcal{H}$), and let $\alpha$ be a partial assignment
such that

$\alpha(z)=\begin{cases}1&\text{if }z\in V\\\
\text{undefined}&\text{otherwise}.\end{cases}$

We claim that, for all $N\in\mathbb{N}^{+}$, given a $\mathsf{RAT}^{-}$
derivation

$\Pi=(\Delta_{1},\dots,\Delta_{N})$

with $\Delta_{1}=\mathcal{H}(\Gamma)$, there exists a $\mathsf{RAT}^{-}$
derivation

$\Pi^{\prime}=(\Psi_{1},\dots,\Psi_{N^{\prime}})$

with $N^{\prime}\leq N\cdot(\lvert\operatorname{var}(\Gamma)\rvert+1)$ such
that

  * •

$\Delta_{1}|_{\alpha}=\Gamma=\Psi_{1}$,

  * •

$\Delta_{N}|_{\alpha}\subseteq\Psi_{N^{\prime}}$, and

  * •

$\Delta_{N}|_{\alpha}\sqsupseteq\Psi_{N^{\prime}}$.

The second condition above implies in particular that if $\bot\in\Delta_{N}$,
then $\bot\in\Psi_{N^{\prime}}$. This in turn implies the desired statement,
since it means that if $\mathcal{H}(\Gamma)$ has a $\mathsf{RAT}^{-}$ proof of
size $N$, then $\Gamma$ has a $\mathsf{RAT}^{-}$ proof of size at most
$N\cdot(\lvert\operatorname{var}(\Gamma)\rvert+1)$.

We proceed by induction. For a derivation $\Pi=(\Delta_{1})$ of size $1$ with
$\Delta_{1}=\mathcal{H}(\Gamma)$, the derivation
$\Pi^{\prime}=(\Delta_{1}|_{\alpha})$ satisfies the conditions above. Let
$\Pi=(\Delta_{1},\dots,\Delta_{m})$ be a $\mathsf{RAT}^{-}$ derivation with
$\Delta_{1}=\mathcal{H}(\Gamma)$. Suppose that
$\Pi^{\prime}=(\Psi_{1},\dots,\Psi_{m^{\prime}})$ is a $\mathsf{RAT}^{-}$
derivation with $m^{\prime}\leq
m\cdot(\lvert\operatorname{var}(\Gamma)\rvert+1)$ satisfying the above
conditions. Let $C$ be a clause that is derived from $\Delta_{m}$ either by
resolution, weakening, or RAT addition. We will show that there exists a
$\mathsf{RAT}^{-}$ derivation from $\Psi_{m^{\prime}}|_{\alpha}$ of a CNF that
contains and is subsumed by $(\Delta_{m}\cup\\{C\\})|_{\alpha}$. For
simplicity, we will establish this for $\Delta_{m}|_{\alpha}$ instead of
$\Psi_{m^{\prime}}|_{\alpha}$, with the understanding that the containment and
the subsumption conditions above imply by Lemma 3.17 that the same derivation
can be made also from $\Psi_{m^{\prime}}|_{\alpha}$. There exists a trivial
derivation when $\alpha\models C$ since it implies that
$(\Delta_{m}\cup\\{C\\})|_{\alpha}=\Delta_{m}|_{\alpha}$, so suppose that
$\alpha\not\models C$. As a consequence, $\alpha$ does not satisfy any subset
of $C$.

From this point on, we write $\Delta$ instead of $\Delta_{m}$ to reduce
clutter.

Case 1

($C$ is a resolvent of $D,E\in\Delta$ on $v$.) Without loss of generality,
suppose that $v\in D$ and $\overline{v}\in E$.

Case 1.1

($v\in V$.) We have $E|_{\alpha}=(E\setminus\\{\overline{v}\\})|_{\alpha}$.
Since $(E\setminus\\{\overline{v}\\})\subseteq C$, we have
$E|_{\alpha}\in\Delta|_{\alpha}$ and $E|_{\alpha}\subseteq C|_{\alpha}$, so
$C|_{\alpha}$ is derived from $\Delta|_{\alpha}$ by weakening.

Case 1.2

($v\notin V$.) Since $(D\setminus\\{v\\})\subseteq C$ and
$(E\setminus\\{\overline{v}\\})\subseteq C$, and since $\alpha$ does not set
$v$, we have $D|_{\alpha}\in\Delta|_{\alpha}$ and
$E|_{\alpha}\in\Delta|_{\alpha}$. Moreover, $C|_{\alpha}$ is a resolvent of
$D|_{\alpha}\in\Delta|_{\alpha}$ and $E|_{\alpha}\in\Delta|_{\alpha}$, so
$C|_{\alpha}$ is derived from $\Delta|_{\alpha}$ by resolution.

Case 2

($C$ is a weakening of a clause $D\in\Delta$.) Since $D\subseteq C$, we have
$D|_{\alpha}\in\Delta|_{\alpha}$ and $D|_{\alpha}\subseteq C|_{\alpha}$, so
$C|_{\alpha}$ is derived from $\Delta|_{\alpha}$ by weakening.

Case 3

($C$ is a RAT for $p\in C$ with respect to $\Delta$.) Since we assumed
$\alpha\not\models C$, there are two possibilities: either $\overline{p}\in V$
or $\operatorname{var}(p)\notin V$.

Case 3.1

($\overline{p}\in V$.) Either $p=\overline{x_{i}}$ or $p=\overline{y_{i}}$ for
some $i\in[t]$. Suppose $p=\overline{x_{i}}$. (The case for
$p=\overline{y_{i}}$ is symmetric.) Since $C$ is a RAT for $\overline{x_{i}}$
with respect to $\Delta$, and since $x_{i}\lor\overline{y_{i}}\in\Delta$, we
have
$\Delta\vdash_{1}(C\setminus\\{\overline{x_{i}}\\})\cup\\{\overline{y_{i}}\\}$.
By Lemma 2.9, we also have

$\Delta|_{\alpha}\vdash_{1}\left.\kern-1.2pt\bigl{(}(C\setminus\\{\overline{x_{i}}\\})\cup\\{\overline{y_{i}}\\}\bigr{)}\right|_{\alpha},$

which simplifies to

$\Delta|_{\alpha}\vdash_{1}C|_{\alpha}.$

By Lemma 3.16, there exists a resolution derivation of $C|_{\alpha}$ from
$\Delta|_{\alpha}$ of size
$\lvert\operatorname{var}(\Delta|_{\alpha})\rvert+1\leq\lvert\operatorname{var}(\Gamma)\rvert+1$.
Moreover, the final CNF in this derivation is subsumed by
$\Delta|_{\alpha}\cup{C|_{\alpha}}=(\Delta\cup\\{C\\})|_{\alpha}$ as desired.

Case 3.2

($\operatorname{var}(p)\notin V$.) The clause $C$ is of the form
$C^{\prime}\mathbin{\dot{\lor}}p$ with $\operatorname{var}(p)\notin V$. Since
$C$ is a RAT for $p$ with respect to $\Delta$, for every clause $D\in\Delta$
of the form $D^{\prime}\mathbin{\dot{\lor}}\overline{p}$, we have
$\Delta\vdash_{1}C^{\prime}\cup D^{\prime}$. We will show that $C|_{\alpha}$
is a RAT with respect to $\Delta|_{\alpha}$. Every clause $D\in\Delta$ such
that $\alpha\models D$ simply disappears from $\Delta|_{\alpha}$, so such
clauses are irrelevant when determining whether $C|_{\alpha}$ is a RAT with
respect to $\Delta|_{\alpha}$. On the other hand, for $D\in\Delta$ of the form
$D^{\prime}\mathbin{\dot{\lor}}\overline{p}$ such that $\alpha\not\models D$,
we have $\Delta|_{\alpha}\vdash_{1}(C^{\prime}\cup D^{\prime})|_{\alpha}$ by
Lemma 2.9. Thus, $C|_{\alpha}$ is a RAT for $p$ with respect to
$\Delta|_{\alpha}$. ∎

Let $n=2^{k}$ for $k\in\mathbb{N}^{+}$. For a propositional variable $x$, let
us write $x\neq 0$ and $x\neq 1$ to denote the literals $x$ and
$\overline{x}$, respectively. To prove the separation, we invoke the above
results with $\Gamma$ as the _bit pigeonhole principle_ , which states that
for all $i,j\in[n+1]$ such that $i\neq j$ the binary strings $p^{i}_{1}\dots
p^{i}_{k}$ and $p^{j}_{1}\dots p^{j}_{k}$ are different. It is defined for $n$
as

$\mathrm{BPHP}_{n}\coloneqq\bigcup_{\begin{subarray}{c}i,j\in[n+1],\;i\neq
j\\\
(h_{1},\dots,h_{k})\in\\{0,1\\}^{k}\end{subarray}}\left(\bigvee_{\ell=1}^{k}p^{i}_{\ell}\neq
h_{\ell}\lor\bigvee_{\ell=1}^{k}p^{j}_{\ell}\neq h_{\ell}\right).$

######  Theorem 5.7.

$\mathsf{GER}^{-}$ is exponentially separated from $\mathsf{RAT}^{-}$.

###### Proof.

Buss and Thapen [6, Theorem 4.4] gave polynomial-size proofs of
$\mathrm{BPHP}_{n}$ in $\mathsf{SPR}^{-}$, which $\mathsf{ER}$ simulates. By
Lemma 5.5, we have

$\operatorname{size}_{\mathsf{GER}^{-}}(\mathcal{H}(\mathrm{BPHP}_{n}))=n^{O(1)}.$

They [6, Theorem 5.4] also proved that
$\operatorname{size}_{\mathsf{RAT}^{-}}(\mathrm{BPHP}_{n})=2^{\Omega(n)}$.
Applying Lemma 5.6 gives

$\operatorname{size}_{\mathsf{RAT}^{-}}(\mathcal{H}(\mathrm{BPHP}_{n}))=2^{\Omega(n)}.$

Thus, $\mathcal{H}(\langle\mathrm{BPHP}\rangle)$ exponentially separates
$\mathsf{GER}^{-}$ from $\mathsf{RAT}^{-}$. ∎

Theorem 1.2 follows directly from Theorems 5.4 and 5.7.

##  6 Exponential separation of $\mathsf{SBC}^{-}$ from $\mathsf{RAT}^{-}$

Recall the transformation in 10, which we used to construct formulas
separating $\mathsf{GER}^{-}$ from $\mathsf{RAT}^{-}$. We had

$\mathcal{H}(\Gamma)=\Gamma\cup\bigcup_{i=1}^{t(\Gamma)}\\{\overline{x_{i}}\lor
y_{i},\ x_{i}\lor\overline{y_{i}}\\},$

where $x_{1},\dots,x_{t(\Gamma)}$ are the extension variables used in a
minimum-size $\mathsf{ER}$ proof $(\Lambda^{*},\Pi^{*})$ of $\Gamma$. We prove
below that $\mathsf{SBC}^{-}$ can use those variables and simulate the
$\mathsf{ER}$ proof of $\Gamma$, so deletion is not the only way to overcome
the obstacles in $\mathcal{H}(\Gamma)$ that prevent $\mathsf{RAT}^{-}$ from
gaining any speedup.

######  Lemma 6.1.

For every CNF $\Gamma$, we have

$\operatorname{size}_{\mathsf{SBC}^{-}}(\mathcal{H}(\Gamma))\leq
2\cdot\operatorname{size}_{\mathsf{ER}}(\Gamma).$

###### Proof.

We write $t$ for $t(\Gamma)$. Let $(\lambda_{1},\dots,\lambda_{t})$ be the
sequence of $t$ sets of extension clauses that make up $\Lambda^{*}$. For each
$i\in[t]$, we will first derive the clauses in

$\lambda_{i}^{\prime}\coloneqq\\{\overline{x_{i}}\lor\overline{y_{i}}\lor
p_{i},\ \overline{x_{i}}\lor\overline{y_{i}}\lor q_{i},\ x_{i}\lor
y_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}\\}$

by a sequence of SBC additions. Consider an arbitrary $i\in[t]$, and suppose
that we have derived $\bigcup_{j=1}^{i-1}\lambda_{j}^{\prime}$ from
$\mathcal{H}(\Gamma)$ by a sequence of SBC additions, so the current CNF is
$\Delta=\mathcal{H}(\Gamma)\cup\bigcup_{j=1}^{i-1}\lambda_{j}^{\prime}$.

  1. 1.

The clause $E_{i}^{1}\coloneqq\overline{x_{i}}\lor\overline{y_{i}}\lor p_{i}$
is an SBC for $L=\\{\overline{x_{i}},\,\overline{y_{i}}\\}$ with respect to
$\Delta$ because $\overline{x_{i}}\lor y_{i}$ and $x_{i}\lor\overline{y_{i}}$
are the only clauses in $\Delta$ that intersect with $\overline{L}$, and both
of these clauses also intersect with $L$ (i.e., there is nothing to check).

  2. 2.

The clause $E_{i}^{2}\coloneqq\overline{x_{i}}\lor\overline{y_{i}}\lor q_{i}$
is similarly an SBC for $L=\\{\overline{x_{i}},\,\overline{y_{i}}\\}$ with
respect to $\Delta$. Furthermore, we have
$E_{i}^{1}\cap\overline{L}=\varnothing$, so $E_{i}^{2}$ is an SBC with respect
to $\Delta\cup\left\\{E_{i}^{1}\right\\}$.

  3. 3.

The clause $E_{i}^{3}\coloneqq x_{i}\lor
y_{i}\lor\overline{p_{i}}\lor\overline{q_{i}}$ is similarly an SBC for
$M=\\{x_{i},\,y_{i}\\}$ with respect to $\Delta$. It is also an SBC for $M$
with respect to $\left\\{E_{i}^{1},E_{i}^{2}\right\\}$ since
$\bigl{(}E_{i}^{3}\setminus
M\bigr{)}\cup\bigl{(}E_{i}^{1}\setminus\overline{M}\bigr{)}=\\{\overline{p_{i}},\,\overline{q_{i}},\,p_{i}\\}$
and $\bigl{(}E_{i}^{3}\setminus
M\bigr{)}\cup\bigl{(}E_{i}^{2}\setminus\overline{M}\bigr{)}=\\{\overline{p_{i}},\,\overline{q_{i}},\,q_{i}\\}$
are both tautological. As a result, $E_{i}^{3}$ is an SBC with respect to
$\Delta\cup\left\\{E_{i}^{1},E_{i}^{2}\right\\}$.

It follows by induction that we can derive
$\bigcup_{i=1}^{t}\lambda_{i}^{\prime}$ from $\mathcal{H}(\Gamma)$ in
$\mathsf{SBC}^{-}$. For each $i\in[t]$, resolving $E_{i}^{1}$ and $E_{i}^{2}$
against $\overline{x_{i}}\lor y_{i}$ and resolving $E_{i}^{3}$ against
$x_{i}\lor\overline{y_{i}}$ gives $\lambda_{i}$, thus we can derive
$\Lambda^{*}$ from $\mathcal{H}(\Gamma)$ in $\mathsf{SBC}^{-}$. Since
$\Pi^{*}$ is a resolution proof of $\Gamma\cup\Lambda^{*}$, and since
$\mathcal{H}(\Gamma)$ contains $\Gamma$, we also have a resolution proof of
$\mathcal{H}(\Gamma)\cup\Lambda^{*}$. In the end, we have an
$\mathsf{SBC}^{-}$ proof of $\mathcal{H}(\Gamma)$ of size at most
$2\lvert\Lambda^{*}\rvert+\lvert\Pi^{*}\rvert\leq
2\cdot\operatorname{size}_{\mathsf{ER}}(\Gamma)$. ∎

It is now straightforward to deduce Theorem 1.4 by invoking Lemmas 5.6 and 6.1
with $\Gamma$ as the bit pigeonhole principle (in the manner of the proof of
Theorem 5.7).

##  7 Exponential separation of $\mathsf{SBC}^{-}$ from $\mathsf{GER}^{-}$

We now give polynomial-size $\mathsf{SBC}^{-}$ proofs of $\mathrm{PHP}_{n}$.
More specifically, we observe that the $\mathsf{SPR}^{-}$ proofs of
$\mathrm{PHP}_{n}$ constructed by Buss and Thapen [6, Theorem 4.3] are in fact
valid $\mathsf{SBC}^{-}$ proofs, so the proof below closely follows theirs.
(No knowledge of $\mathsf{SPR}^{-}$ is required to follow this section.)

######  Lemma 7.1.

$\operatorname{size}_{\mathsf{SBC}^{-}}(\mathrm{PHP}_{n})=n^{O(1)}$.

###### Proof.

We essentially formalize in $\mathsf{SBC}^{-}$ a short inductive proof of
$\mathrm{PHP}_{n}$, which assumes without loss of generality that the smallest
pigeon is mapped to the smallest hole, derives from this assumption a renamed
instance of $\mathrm{PHP}_{n-1}$, and inductively repeats these steps until
deriving a trivial contradiction.

Recall that $\mathrm{PHP}_{n}$ consists of the clauses $P_{i}\coloneqq
p_{i,1}\lor\dots\lor p_{i,n}$ and
$H_{i,j,k}\coloneqq\overline{p_{i,k}}\lor\overline{p_{j,k}}$ for $i,j\in[n+1]$
and $k\in[n]$ with $i\neq j$.

For $i\in[n-1]$, $j\in[n+1]$, and $k\in[n]$ such that $j,k>i$, let

$C_{i,j,k}\coloneqq\overline{p_{i,k}}\lor\overline{p_{j,i}}\lor\left(\bigvee_{\begin{subarray}{c}\ell\in[n+1]\\\
\ell\neq
i\end{subarray}}p_{\ell,k}\right)\lor\left(\bigvee_{\begin{subarray}{c}\ell\in[n+1]\\\
\ell\neq j\end{subarray}}p_{\ell,i}\right).$

Also, for $i\in[n-1]$, let

$\Lambda_{i}\coloneqq\\{C_{i,j,k}\mid j\in[n+1],\ k\in[n],\text{ and
}j,k>i\\}.$

We will first show that, for all $i\in[n-1]$, from
$\Psi_{i-1}\coloneqq\mathrm{PHP}_{n}\cup\bigcup_{\ell=1}^{i-1}\Lambda_{\ell}$
we can derive the clauses in $\Lambda_{i}$ in any order by a sequence of set-
blocked clause additions, which implies that we can obtain $\Psi_{n-1}$ from
$\mathrm{PHP}_{n}$ in $\mathsf{SBC}^{-}$. Afterwards, we will give a
polynomial-size resolution derivation of the empty clause from $\Psi_{n-1}$,
concluding the proof.

For every clause $C_{i,j,k}\in\Lambda_{i}$ and every subset
$\Lambda_{i}^{\prime}\subseteq\Lambda_{i}\setminus\\{C_{i,j,k}\\}$, we claim
that $C_{i,j,k}$ is an SBC for
$L=\\{\overline{p_{i,k}},\,\overline{p_{j,i}},\,p_{i,i},\,p_{j,k}\\}\subseteq
C_{i,j,k}$ with respect to $\Psi_{i-1}\cup\Lambda_{i}^{\prime}$. This requires
us to show that for all $D\in\Psi_{i-1}\cup\Lambda_{i}^{\prime}$ with
$D\cap\overline{L}\neq\varnothing$ and $D\cap L=\varnothing$ the set
$\bigl{(}C_{i,j,k}\setminus
L\bigr{)}\cup\bigl{(}D\setminus\overline{L}\bigr{)}$ is tautological. There
are three cases.

Case 1

($D\in\mathrm{PHP}_{n}$.) If $D$ is a clause in $\mathrm{PHP}_{n}$ such that
$D\cap\overline{L}\neq\varnothing$ and $D\cap L=\varnothing$, then either
$D=H_{i,i^{\prime},i}$ for some $i^{\prime}\in[n+1]$ such that $i^{\prime}\neq
j$ or $D=H_{j,j^{\prime},k}$ for some $j^{\prime}\in[n+1]$ such that
$j^{\prime}\neq i$. If $D=H_{i,i^{\prime},i}$, then we have
$p_{i^{\prime},i}\in C_{i,j,k}\setminus L$ and $\overline{p_{i^{\prime},i}}\in
D\setminus\overline{L}$, so the union of the two sets is tautological. The
argument for the case of $D=H_{j,j^{\prime},k}$ is similar.

Case 2

($D\in\bigcup_{\ell=1}^{i-1}\Lambda_{\ell}$.) Let
$D=C_{i^{\prime},j^{\prime},k^{\prime}}$ be an arbitrary clause in
$\bigcup_{\ell=1}^{i-1}\Lambda_{\ell}$, where $i^{\prime}<i$ and
$j^{\prime},k^{\prime}>i^{\prime}$. A simple inspection shows that we have
$D\cap\overline{L}\neq\varnothing$ if and only if $k^{\prime}=i$ or
$k^{\prime}=k$. If $k^{\prime}=i$, then $p_{i,i}\in D$. Noting that
$i^{\prime}\neq j$, if $k^{\prime}=k$, then $p_{j,k}\in D$. Either way, $D\cap
L=\varnothing$ fails to hold, so there exists no
$D\in\bigcup_{\ell=1}^{i-1}\Lambda_{\ell}$ such that
$D\cap\overline{L}\neq\varnothing$ and $D\cap L=\varnothing$.

Case 3

($D\in\Lambda_{i}^{\prime}$.) Let $D=C_{i,j^{\prime},k^{\prime}}$ be an
arbitrary clause in $\Lambda_{i}^{\prime}$, where $j^{\prime},k^{\prime}>i$.
It is straightforward to see that we have $p_{i,i}\in D$ unless
$j^{\prime}=i$. Then, since $j^{\prime}>i$, there exists no
$D\in\Lambda_{i}^{\prime}$ such that $D\cap L=\varnothing$.

Thus, we obtain $\Psi_{n-1}$ from $\mathrm{PHP}_{n}$ in $\mathsf{SBC}^{-}$,
and now we construct a resolution proof of $\Psi_{n-1}$. First, for each
$(i,j,k)$ such that $C_{i,j,k}$ is defined, we resolve $C_{i,j,k}$ against the
axioms for the holes $k$ and $i$ to derive
$\overline{p_{i,k}}\lor\overline{p_{j,i}}$. Then, for each $i\in[n]$ and
$j\in[n+1]$ such that $j>i$, we derive the clause $\overline{p_{j,i}}$ by
induction on $i$ as follows: Fix $i$ and $j$ such that $j>i$. Let

$\Delta_{i,j}\coloneqq\\{\overline{p_{i,k}}\mid k\in[n]\text{ and
}k<i\\}\cup\\{\overline{p_{i,i}}\lor\overline{p_{j,i}}\\}\cup\\{\overline{p_{i,k}}\lor\overline{p_{j,i}}\mid
k\in[n]\text{ and }k>i\\},$

where we have the clauses in the first set from the induction hypothesis, the
second set from $\mathrm{PHP}_{n}$, and the third set from resolving
$C_{i,j,k}$ against the hole axioms in the previous step. Resolving each
clause in $\Delta_{i,j}$ against the pigeon axiom $P_{i}$ thus gives
$\overline{p_{j,i}}$. Finally, we resolve for each $i\in[n]$ the clause
$\overline{p_{n+1,i}}$ against $P_{n+1}$ to derive the empty clause. ∎

Kullmann [24, Lemma 9.4] showed that
$\operatorname{size}_{\mathsf{GER}^{-}}(\mathrm{PHP}_{n})=2^{\Omega(n)}$, so
Theorem 1.5 follows by Lemma 7.1.

## Acknowledgments

We thank Jakob Nordström for useful discussions and the ITCS reviewers for
their comments.

## References

  * AU [00] Noriko H. Arai and Alasdair Urquhart.  Local symmetries in propositional logic.  In Proceedings of the 9th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), number 1847 in Lecture Notes in Computer Science, pages 40–51. Springer, 2000.
  * BCB [20] Lee A. Barnett, David Cerna, and Armin Biere.  Covered clauses are not propagation redundant.  In Proceedings of the 10th International Joint Conference on Automated Reasoning (IJCAR), number 12166 in Lecture Notes in Computer Science, pages 32–47. Springer, 2020.
  * BJ [16] Sam Buss and Jan Johannsen.  On linear resolution.  Journal on Satisfiability, Boolean Modeling and Computation, 10(1):23–35, 2016.
  * Bla [37] Archie Blake.  Canonical Expressions in Boolean Algebra.  PhD thesis, The University of Chicago, 1937.
  * BP [07] Joshua Buresh-Oppenheim and Toniann Pitassi.  The complexity of resolution refinements.  The Journal of Symbolic Logic, 72(4):1336–1352, 2007.
  * BT [21] Sam Buss and Neil Thapen.  DRAT and propagation redundancy proofs without new variables.  Logical Methods in Computer Science, 17(2:12), 2021.
  * CCT [87] William Cook, Collette R. Coullard, and György Turán.  On the complexity of cutting-plane proofs.  Discrete Applied Mathematics, 18(1):25–38, 1987.
  * CEI [96] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo.  Using the Groebner basis algorithm to find proofs of unsatisfiability.  In Proceedings of the 28th Symposium on Theory of Computing (STOC), pages 174–183. Association for Computing Machinery, 1996.
  * Cha [70] Chin-Liang Chang.  The unit proof and the input proof in theorem proving.  Journal of the ACM, 17(4):698–707, 1970.
  * Coo [76] Stephen A. Cook.  A short proof of the pigeon hole principle using extended resolution.  ACM SIGACT News, 8(4):28–32, 1976.
  * CR [79] Stephen A. Cook and Robert A. Reckhow.  The relative efficiency of propositional proof systems.  The Journal of Symbolic Logic, 44(1):36–50, 1979.
  * GN [03] Evgueni Goldberg and Yakov Novikov.  Verification of proofs of unsatisfiability for CNF formulas.  In Proceedings of the Design, Automation and Test in Europe Conference (DATE), pages 886–891. IEEE Computer Society, 2003.
  * HHU [07] Alexander Hertel, Philipp Hertel, and Alasdair Urquhart.  Formalizing dangerous SAT encodings.  In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT), number 4501 in Lecture Notes in Computer Science, pages 159–172. Springer, 2007.
  * HKB [19] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere.  Encoding redundancy for satisfaction-driven clause learning.  In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), number 11427 in Lecture Notes in Computer Science, pages 41–58. Springer, 2019.
  * HKB [20] Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere.  Strong extension-free proof systems.  Journal of Automated Reasoning, 64(3):533–554, 2020.
  * HKSB [17] Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere.  PRuning through satisfaction.  In Proceedings of the 13th Haifa Verification Conference (HVC), number 10629 in Lecture Notes in Computer Science, pages 179–194. Springer, 2017.
  * JHB [12] Matti Järvisalo, Marijn J. H. Heule, and Armin Biere.  Inprocessing rules.  In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR), number 7364 in Lecture Notes in Computer Science, pages 355–370. Springer, 2012.
  * Kra [19] Jan Krajíček.  Proof Complexity.  Cambridge University Press, 2019.
  * KRHB [20] Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule, and Armin Biere.  Simulating strong practical proof systems with extended resolution.  Journal of Automated Reasoning, 64(7):1247–1267, 2020.
  * Kri [85] Balakrishnan Krishnamurthy.  Short proofs for tricky formulas.  Acta Informatica, 22(3):253–275, 1985.
  * KSTB [18] Benjamin Kiesl, Martina Seidl, Hans Tompits, and Armin Biere.  Local redundancy in SAT: Generalizations of blocked clauses.  Logical Methods in Computer Science, 14(4:3), 2018.
  * Kul [97] Oliver Kullmann.  Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms.  In Satisfiability Problem: Theory and Applications, number 35 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 261–313. American Mathematical Society, 1997.
  * [23] Oliver Kullmann.  New methods for 3-SAT decision and worst-case analysis.  Theoretical Computer Science, 223(1–2):1–72, 1999.
  * [24] Oliver Kullmann.  On a generalization of extended resolution.  Discrete Applied Mathematics, 96–97:149–176, 1999.
  * LS [91] László Lovász and Alexander Schrijver.  Cones of matrices and set-functions and 0–1 optimization.  SIAM Journal on Optimization, 1(2):166–190, 1991.
  * MS [99] João P. Marques-Silva and Karem A. Sakallah.  GRASP: A search algorithm for propositional satisfiability.  IEEE Transactions on Computers, 48(5):506–521, 1999.
  * PS [10] Toniann Pitassi and Rahul Santhanam.  Effectively polynomial simulations.  In Proceedings of the 1st Innovations in Computer Science (ICS), pages 370–382. Tsinghua University Press, 2010.
  * PY [84] Christos H. Papadimitriou and Mihalis Yannakakis.  The complexity of facets (and some facets of complexity).  Journal of Computer and System Sciences, 28(2):244–259, 1984.
  * Rob [65] John A. Robinson.  A machine-oriented logic based on the resolution principle.  Journal of the ACM, 12(1):23–41, 1965.
  * Sze [05] Stefan Szeider.  The complexity of resolution with generalized symmetry rules.  Theory of Computing Systems, 38(2):171–188, 2005.
  * Tse [68] Grigori S. Tseitin.  On the complexity of derivation in propositional calculus.  Zapiski Nauchnykh Seminarov LOMI, 8:234–259, 1968.
  * Urq [99] Alasdair Urquhart.  The symmetry rule in propositional logic.  Discrete Applied Mathematics, 96–97:177–193, 1999.
  * Van [08] Allen Van Gelder.  Verifying RUP proofs of propositional unsatisfiability.  In Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM), 2008.
  * WHH [14] Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr.  DRAT-trim: Efficient checking and trimming using expressive clausal proofs.  In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT), number 8561 in Lecture Notes in Computer Science, pages 422–429. Springer, 2014.

##  Appendix A Proof of Lemma 3.16

Let us recall the statement of the result before proceeding with its proof.

See 3.16

###### Proof.

We assume without loss of generality that
$\operatorname{var}(C)\subseteq\operatorname{var}(\Gamma)$ since any variable
of $C$ not occurring in $\Gamma$ can be ignored in a unit propagation proof of
$\Gamma\land\overline{C}$. Also, if $\bot\in\Gamma$, then the statement
trivially follows since we can derive any clause by a single use of the
weakening rule, so suppose $\bot\notin\Gamma$.

Assuming $\Gamma\vdash_{1}C$, we will show that there exists a resolution
derivation that is as desired and, additionally, is of a particular shape.
Specifically, the derivation will start by a possible use of the weakening
rule, followed only by uses of the resolution rule such that one of the two
premises is a clause in $\Gamma$. This is called an _input resolution proof_.
Figure 2 shows the shape of an input resolution proof viewed as a tree.

$D_{1}$$D_{1}^{\prime}$$D_{2}$$D_{3}$$D_{m-1}$$C$$D_{m}$ Figure 2: In the
above tree for a resolution proof, each node corresponds to a clause, with
incoming arrows indicating the premises from which it is derived. When we have
$D_{1},\dots,D_{m}\in\Gamma$ and $D_{1}\subseteq D_{1}^{\prime}$, the tree
represents an input resolution proof that derives $C$ from $\Gamma$.

We proceed by induction on the number of variables of $\Gamma$. Let $\Gamma$
be a CNF with a single variable, say $x$. Let $C$ be a clause, and suppose
that $\Gamma\vdash_{1}C$. Then the clause $C$ is either $x$, $\overline{x}$,
or $\bot$. In the first two cases, $\Gamma\vdash_{1}C$ implies that
$C\in\Gamma$, so the derivation $(\Gamma)$ is as desired. In the last case,
$\Gamma\vdash_{1}\bot$ implies that $\Gamma=\\{x,\ \overline{x}\\}$, so a
single use of the resolution rule gives the derivation
$(\Gamma,\Gamma\cup\\{\bot\\})$ as desired.

Let $n\in\mathbb{N}^{+}$, and suppose that the statement holds for all
formulas and clauses with $n$ variables. Consider a CNF $\Gamma$ with
$\lvert\operatorname{var}(\Gamma)\rvert=n+1$. Let $C$ be a clause, and suppose
that $\Gamma\vdash_{1}C$. Since
$\left(\Gamma\land\overline{C}\right)\vdash_{1}\bot$, the CNF
$\Gamma\land\overline{C}$ must have some clause containing a single literal,
say $p$ (otherwise the unit propagation rule cannot be used at all). Let
$\alpha$ be the partial assignment that only sets $\alpha(p)=1$. There are two
cases.

Case 1

($\alpha\models C$.) We have $p\in C$, which implies that $\overline{p}\notin
C$ since $C$ is a clause. As a result, $p\notin\overline{C}$, but we know that
$\\{p\\}\in\left(\Gamma\land\overline{C}\right)$, so it must be the case that
$\\{p\\}\in\Gamma$. Then we can derive $C$ from $\Gamma$ by a single use of
the weakening rule, so the derivation $(\Gamma,\Gamma\cup\\{C\\})$ is as
desired.

Case 2

($\alpha\not\models C$.) By Lemma 2.9, we have
$\Gamma|_{\alpha}\vdash_{1}C|_{\alpha}$. Since
$\lvert\operatorname{var}(\Gamma|_{\alpha})\rvert=n$, the induction hypothesis
guarantees the existence of an input resolution derivation
$\Pi=(\Gamma_{1},\dots,\Gamma_{N})$ with $N\leq n+1$ such that
$\Gamma_{1}=\Gamma|_{\alpha}$, $C|_{\alpha}\in\Gamma_{N}$, and
$\Gamma|_{\alpha}\cup\\{C|_{\alpha}\\}\sqsupseteq\Gamma_{N}$. For every leaf
$D$ in the tree for $\Pi$, either $D\in\Gamma$ or
$D\lor\overline{p}\in\Gamma$, so we define

$f(D)\coloneqq\begin{cases}D&\text{if }D\in\Gamma\\\
D\lor\overline{p}&\text{if }D\lor\overline{p}\in\Gamma.\end{cases}$

We modify $\Pi$ by first replacing each leaf $D$ by $f(D)$ and then
recursively replacing each inner node $E$ by $E\lor\overline{p}$ if one of its
premises has been changed. The result corresponds to a valid input resolution
derivation $\Pi^{\prime}=(\Gamma_{1}^{\prime},\dots,\Gamma_{N}^{\prime})$ such
that $\Gamma_{1}^{\prime}=\Gamma$, $C^{\prime}\in\Gamma_{N}^{\prime}$, and
$\Gamma\cup\\{C|_{\alpha}\\}\sqsupseteq\Gamma_{N}^{\prime}$, where either
$C^{\prime}=C|_{\alpha}$ or $C^{\prime}=C|_{\alpha}\lor\overline{p}$.
Moreover, we have either $C|_{\alpha}=C$ or
$C|_{\alpha}=C\setminus\\{\overline{p}\\}$. We make a final modification to
$\Pi^{\prime}$ according to the following table:

|  $C^{\prime}=C|_{\alpha}$ |  $C^{\prime}=C|_{\alpha}\lor\overline{p}$
---|---|---
$C|_{\alpha}=C$ |  Nothing to do, because $\Pi^{\prime}$ is already as desired. |  Resolve $C^{\prime}$ against $\\{p\\}\in\Gamma$, where $\\{p\\}\in\Gamma$ holds due to $\overline{p}\notin C$ and $\\{p\\}\in\left(\Gamma\land\overline{C}\right)$.
$C|_{\alpha}=C\setminus\\{\overline{p}\\}$ |  Modify $\Pi^{\prime}$ to make sure that the clause derived by the initial use of the weakening rule (inserting one if weakening was not used) contains $\overline{p}$, followed by the same modification for all of the clauses corresponding to the inner nodes of the proof tree.

In any case, we increase the size of $\Pi^{\prime}$ by at most one and end up
with the desired derivation of size at most
$n+2=\lvert\operatorname{var}(\Gamma)\rvert+1$. ∎