17212 LABEL:LastPageSep. 07, 2019Apr. 23, 2021

*A preliminary version [BT19] of this paper appeared in the Proceedings of the 2019 Conference on Theory and Applications of Satisfiability Testing (SAT).

# DRAT and Propagation Redundancy Proofs
Without New Variables*

Sam Bussa  aDepartment of Mathematics, University of California, San Diego, La
Jolla, CA 92093–0112, USA<EMAIL_ADDRESS>and  Neil Thapenb  bInstitute of
Mathematics of the Czech Academy of Sciences, Prague, Czech Republic
<EMAIL_ADDRESS>
###### Abstract.

We study the complexity of a range of propositional proof systems which allow
inference rules of the form: from a set of clauses $\Gamma$ derive the set of
clauses $\Gamma\cup\\{C\\}$ where, due to some syntactic condition,
$\Gamma\cup\\{C\\}$ is satisfiable if $\Gamma$ is, but where $\Gamma$ does not
necessarily imply $C$. These inference rules include BC, RAT, SPR and PR
(respectively short for _blocked clauses_ , _resolution asymmetric
tautologies_ , _subset propagation redundancy_ and _propagation redundancy_),
which arose from work in satisfiability (SAT) solving. We introduce a new,
more general rule SR (_substitution redundancy_).

If the new clause $C$ is allowed to include new variables then the systems
based on these rules are all equivalent to extended resolution. We focus on
restricted systems that do not allow new variables. The systems with deletion,
where we can delete a clause from our set at any time, are denoted
${{\hbox{\rm DBC}}^{-}}$, ${{\hbox{\rm DRAT}}^{-}}$, ${{\hbox{\rm
DSPR}}^{-}}$, ${{\hbox{\rm DPR}}^{-}}$ and ${{\hbox{\rm DSR}}^{-}}$. The
systems without deletion are ${{\hbox{\rm BC}}^{-}}$, ${{\hbox{\rm
RAT}}^{-}}$, ${{\hbox{\rm SPR}}^{-}}$, ${{\hbox{\rm PR}}^{-}}$ and
${{\hbox{\rm SR}}^{-}}$.

With deletion, we show that DRAT-, DSPR- and DPR- are equivalent. By earlier
work of Kiesl, Rebola-Pardo and Heule [KRPH18], they are also equivalent to
DBC-. Without deletion, we show that SPR- can simulate PR- provided only short
clauses are inferred by SPR inferences. We also show that many of the well-
known “hard” principles have small SPR- refutations. These include the
pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin
tautologies and clique-coloring tautologies. SPR- can also handle or-fication
and xor-ification, and lifting with an index gadget. Our final result is an
exponential size lower bound for RAT- refutations, giving exponential
separations between RAT- and both DRAT- and SPR-.

###### Key words and phrases:

DRAT, extension, pigeonhole principle, proof logging, propagation redundancy,
propositional proofs, resolution, satisfiability

This work was initiated on a visit of the first author to the Czech Academy of
Sciences in July 2018, supported by ERC advanced grant 339691 (FEALORA). The
first author was also supported by Simons Foundation grant 578919. The second
author was partially supported by GA ČR project 19–05497S. The Institute of
Mathematics of the Czech Academy of Sciences is supported by RVO:67985840.

##  1\. Introduction

SAT solvers are routinely used for a range of large-scale instances of
satisfiability. It is widely realized that when a solver reports that a SAT
instance $\Gamma$ is unsatisfiable, it should also produce a _proof_ that it
is unsatisfiable. This is of particular importance as SAT solvers become
increasingly complex, combining many techniques, and thus are more subject to
software bugs or even design problems.

The first proof systems proposed for SAT solvers were based on reverse unit
propagation (RUP, or $\vdash_{1}$ in the notation of this paper) inferences
[GN03, Van08] as this is sufficient to handle both resolution inferences and
the usual CDCL clause learning schemes. However, RUP inferences only support
logical implication, and in particular do not accommodate many “inprocessing”
rules. Inprocessing rules support inferences which do not respect logical
implication; instead they only guarantee _equisatisfiability_ where the
(un)satisfiability of the set of clauses is preserved [JHB12]. Inprocessing
inferences have been formalized in terms of sophisticated inference rules
including DRAT (_deletion, reverse asymmetric tautology_), PR (_propagation
redundancy_), SPR (_subset PR_) in a series of papers including [JHB12,
HHJW13b, HHJW13a, WHHJ14] — see Section 1.2 for definitions. These inference
rules can be viewed as introducing clauses that hold “without loss of
generality” [RS18], and thus preserve (un)satisfiability. An important feature
of these systems is that they can be used both as proof systems to verify
unsatisfiability, and as inference systems to facilitate searching for either
a satisfying assignment or a proof of unsatisfiability.111The deletion rule is
very helpful to improve proof search and can extend the power of the
inferences rules, see Corollary 34; however, it must be used carefully to
preserve equisatisfiabity. The present paper only considers _refutation
systems_ , and thus the deletion rule can be used without restriction.

The DRAT system is very powerful as it can simulate extended resolution
[Kul99b, KRPH18]. This simulation is straightforward, but depends on DRAT’s
ability to introduce new variables; we simply show that the usual extension
axioms are RAT. However, there are a number of results [HB18, HKSB17, HKB17,
HKB19] indicating that DRAT and PR are still powerful when restricted to use
few new variables, or even no new variables. In particular, [HKSB17, HKB17,
HKB19] showed that the pigeonhole principle clauses have short (polynomial
size) refutations in the PR proof system. The paper [HKSB17] showed that
Satisfaction Driven Clause Learning (SDCL) can discover PR proofs of the
pigeonhole principle automatically; in the application studied by [HKSB17],
the SDCL search appears to have exponential runtime, but is much more
efficient than the usual CDCL search. There are at present no broadly
applicable proof search heuristics for how to usefully introduce new variables
with the extension rule. It is possible however that there are useful
heuristics for searching for proofs that do not use new variables in DRAT and
PR and related systems. For these reasons, DRAT and PR and related systems
(even when new variables are not allowed) hold the potential for substantial
improvements in the power of SAT solvers.

The present paper extends the theoretical knowledge of these proof systems
viewed as refutation systems. We pay particular attention to proof systems
that do not allow new variables. The remainder of Section 1 introduces the
proof systems BC (_blocked clauses_), RAT, SPR, PR and SR (_substitution
redundancy_). (Only SR is new to this paper.) These systems have variants
which allow deletion, called DBC, DRAT, DSPR, DPR and DSR. There are also
variants of all these systems restricted to not allow new variables: we denote
these with a superscript “$-$” as ${{\hbox{\rm BC}}^{-}}$, ${{\hbox{\rm
DBC}}^{-}}$, ${{\hbox{\rm RAT}}^{-}}$, ${{\hbox{\rm DRAT}}^{-}}$, etc.

Section 2 studies the relation between these systems and extended resolution.
We show in particular that any proof system containing ${{\hbox{\rm BC}}^{-}}$
and closed under restrictions simulates extended resolution. Here a proof
system ${\mathcal{P}}$ is said to _simulate_ a proof system ${\mathcal{Q}}$ if
any $\mathcal{Q}$-proof can be converted, in polynomial time, into a
${\mathcal{P}}$-proof of the same result. Two systems are _equivalent_ if they
simulate each other; otherwise they are _separated_. We also show that the
systems discussed above all have equivalent canonical NP pairs (a coarser
notion of equivalence).

Section 3 extends known results that ${{\hbox{\rm DBC}}^{-}}$ simulates
${{\hbox{\rm DRAT}}^{-}}$ [KRPH18] and that DRAT, limited to only one extra
variable, simulates ${{\hbox{\rm DPR}}^{-}}$ [HB18]. Theorem 16 proves that
${{\hbox{\rm DRAT}}^{-}}$ simulates ${{\hbox{\rm DPR}}^{-}}$. As a
consequence, ${{\hbox{\rm DBC}}^{-}}$ can also simulate ${{\hbox{\rm
DPR}}^{-}}$. We then give a partial simulation of ${{\hbox{\rm PR}}^{-}}$ by
${{\hbox{\rm SPR}}^{-}}$ — our size bound is exponential in the size of the
“discrepancy” of the PR inferences, but in many cases, the discrepancy will be
logarithmic or even smaller.

Section 4 proves new polynomial upper bounds on the size of ${{\hbox{\rm
SPR}}^{-}}$ proofs for many of the “hard” tautologies from proof complexity.
(Recall that ${{\hbox{\rm SPR}}^{-}}$ allows neither deletion nor the use of
new variables.) These include the pigeonhole principle, the bit pigeonhole
principle, the parity principle, the clique-coloring principle, and the
Tseitin tautologies. We also show that obfuscation by or-fication, xor-
ification and lifting with a indexing gadget do not work against ${{\hbox{\rm
SPR}}^{-}}$. Prior results gave ${{\hbox{\rm SPR}}^{-}}$ proofs for the
pigeonhole principle (PHP) [HKB17, HKB19], and ${{\hbox{\rm PR}}^{-}}$ proofs
for the Tseitin tautologies and the 2–1 PHP [HB18]. These results raise the
question of whether ${{\hbox{\rm SPR}}^{-}}$ (with no new variables!) can
simulate Frege systems, for instance. Some possible principles that might
separate ${{\hbox{\rm SPR}}^{-}}$ from Frege systems are the graph PHP
principle, 3-XOR tautologies and the even coloring principle; these are
discussed at the end of Section 4. However, the even coloring principle does
have short ${{\hbox{\rm DSPR}}^{-}}$ proofs, and it is plausible that the
graph PHP principle has short ${{\hbox{\rm SPR}}^{-}}$ proofs.

Section 5 shows that ${{\hbox{\rm RAT}}^{-}}$ (with neither new variables nor
deletion) cannot simulate either ${{\hbox{\rm DRAT}}^{-}}$ (without new
variables, but with deletion) or ${{\hbox{\rm SPR}}^{-}}$ (with neither new
variables nor deletion). This follows from a size lower bound for ${{\hbox{\rm
RAT}}^{-}}$ proofs of the bit pigeonhole principle (${\mathrm{BPHP}}$). We
first prove a width lower bound, by showing that any RAT inference in a small-
width refutation of ${\mathrm{BPHP}}$ can be replaced with a small-width
resolution derivation, and then derive the size bound. We use that
${\mathrm{BPHP}}$ behaves well when the sign of a variable is flipped.

The known relationships between these systems, including our results, are
summarized in Figure 1. Recall that e.g. BC is the full system, ${{\hbox{\rm
DBC}}^{-}}$ is the system with deletion but no new variables, and ${{\hbox{\rm
BC}}^{-}}$ is the system with neither deletion nor new variables. An arrow
shows that the upper system simulates the lower one. Equivalence $\equiv$
indicates that the systems simulate each other. The arrow from ${{\hbox{\rm
PR}}^{-}}$ and ${{\hbox{\rm SPR}}^{-}}$ is marked $*$ to indicate that there
is a simulation in the other direction under the additional assumption that
the discrepancies (see Definition 3.2) of PR inferences are logarithmically
bounded.

${\hbox{\rm ER}}\equiv{\hbox{\rm SR}}\equiv{\hbox{\rm PR}}\equiv{\hbox{\rm
SPR}}\equiv{\hbox{\rm RAT}}\equiv{\hbox{\rm BC}}$${{{\hbox{\rm
DSR}}^{-}}}$${{\hbox{\rm DPR}}^{-}}\equiv{{\hbox{\rm
DSPR}}^{-}}\equiv{{\hbox{\rm DRAT}}^{-}}\equiv{{\hbox{\rm
DBC}}^{-}}$${{{\hbox{\rm SR}}^{-}}}$${{{\hbox{\rm PR}}^{-}}}$${{{\hbox{\rm
SPR}}^{-}}}$${{{\hbox{\rm RAT}}^{-}}}$${{{\hbox{\rm
BC}}^{-}}}$${\mathrm{Res}}$$\scriptstyle{~{}*}$$\scriptstyle{~{}\not\equiv}$$\scriptstyle{~{}\not\equiv}$
Figure 1. Relationships between proof systems.

We summarize the rules underlying these systems in Table 1. The details and
the necessary definitions are in Section 1.2 below — in particular see Theorem
1.4 for this definition of RAT.

BC | (a restriction of RAT) | _blocked clause_
---|---|---
RAT |  $\tau$ is $\alpha$ with one variable flipped | _reverse asymmetric tautology_
SPR |  $\tau$ is a partial assignment, ${\hbox{{dom}}}(\tau)\\!=\\!{\hbox{{dom}}}(\alpha)$ | _subset propagation redundant_
PR |  $\tau$ is a partial assignment | _propagation redundant_
SR | no extra conditions | _substitution redundant_
Table 1. Summary of rules of inference.

As presented here the rules (except for BC) have the form: derive $C$ from
$\Gamma$, if there is a substitution $\tau$ satisfying
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ plus the conditions shown,
where $\alpha$ is  $C$ . The implication $\vdash_{1}$ is defined below in
terms of reverse unit propagation (RUP).

We remark that the question of whether new variables help reasoning with
blocked clause inferences was already studied by Kullmann in the context of
the system Generalized Extended Resolution (GER) [Kul99b]. As far as we know,
GER does not correspond exactly to any of the systems we consider. [Kul99b]
showed thatallowing new variables does not reduce GER proof length when the
blocked clause rule is restricted to introducing clauses of length at most
two.

###  1.1. Preliminaries

We use the usual conventions for clauses, variables, literals, truth
assignments, satisfaction, etc. Var and Lit denote the sets of all variables
and all literals. A set of literals is called _tautological_ if it contains a
pair of complementary literals $p$ and  $p$ . A _clause_ is a non-
tautological222 Disallowing tautological clauses makes the rest of the
definitions more natural. In particular, we can identify clauses with the
negations of partial assignments. set of literals; we use $C,D,\ldots$ to
denote clauses. The empty clause is denoted $\perp$, and is always false.
${\mathrm{0}}$ and ${\mathrm{1}}$ denote respectively _False_ and _True_ ; and
${\mathrm{0}}$ and  ${\mathrm{1}}$ are respectively $1$ and $0$. We use both
$C\cup D$ or $C\lor D$ to denote unions of clauses, but usually write $C\lor
D$ when the union is a clause. The notation $C=D\,\dot{\lor}\,E$ indicates
that $C=D\lor E$ is a clause and $D$ and $E$ have no variables in common. If
$\Gamma$ is a set of clauses, $C\lor\Gamma$ is the set $\\{C\lor
D:\text{$D\in\Gamma$ and $C\lor D$ is a clause}\\}$.

A _partial assignment_ $\tau$ is a mapping with domain a set of variables and
range contained in $\\{{\mathrm{0}},{\mathrm{1}}\\}$. It acts on literals by
letting $\tau(\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}})=\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$\tau(p)$}}$. It is called a _total assignment_ if it sets all
variables. We sometimes identify a partial assignment $\tau$ with the set of
unit clauses asserting that $\tau$ holds. For $C$ a clause,  $C$ denotes the
partial assignment whose domain is the variables of $C$ and which asserts that
$C$ is false. For example, if $C=x\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$y$}}\lor z$ then, depending on context,  $C$ will denote
either the set containing the three unit clauses  $x$ and $y$ and  $z$ , or
the partial assignment $\alpha$ with domain
${\hbox{{dom}}}(\alpha)=\\{x,y,z\\}$ such that $\alpha(x)={\mathrm{0}}$,
$\alpha(y)={\mathrm{1}}$ and $\alpha(z)={\mathrm{0}}$.

A _substitution_ generalizes the notion of a partial assignment by allowing
variables to be mapped also to literals. Formally, a substitution $\sigma$ is
a map from ${\hbox{{Var}}}\cup\\{{\mathrm{0}},{\mathrm{1}}\\}$ to
${\hbox{{Lit}}}\cup\\{{\mathrm{0}},{\mathrm{1}}\\}$ which is the identity on
$\\{{\mathrm{0}},{\mathrm{1}}\\}$. Note that a substitution may cause
different literals to become identified.333[Sze03] defined a notion of
“homomorphisms” that is similar to substitutions. Substitutions, however,
allow variables to be mapped also to constants. Our SR inference, defined
below, uses $\vdash_{1}$; this was not used with homomorphisms in [Sze03]. A
partial assignment $\tau$ can be viewed as a substitution, by defining
$\tau(x)=x$ for all variables $x$ outside the domain of $\tau$. The _domain_
of a substitution $\sigma$ is the set of variables $x$ for which
$\sigma(x)\neq x$.

Suppose $C$ is a clause and $\sigma$ is a substitution (or a partial assigment
viewed as a substitution). Let $\sigma(C)=\\{\sigma(p):p\in C\\}$. We say
$\sigma$ _satisfies_ $C$, written $\sigma\vDash C$, if $1\in\sigma(C)$ or
$\sigma(C)$ is tautological. When $\sigma\nvDash C$, the _restriction_
$C_{{{|}}\sigma}$ is defined by letting $C_{{{|}}\sigma}$ equal
$\sigma(C)\setminus\\{{\mathrm{0}}\\}$. Thus $C_{{{|}}\sigma}$ is a clause
expressing the meaning of $C$ under $\sigma$. For $\Gamma$ a set of clauses,
the restriction of $\Gamma$ under $\sigma$ is

$\Gamma_{{{|}}\sigma}~{}=~{}\\{\,C_{{{|}}\sigma}:\text{ $C\in\Gamma$ and
$\sigma\nvDash C$ }\\}.$

The composition of two substitutions is denoted $\tau\circ\pi$, meaning that
$(\tau\circ\pi)(x)=\tau(\pi(x))$, and in particular $(\tau\circ\pi)(x)=\pi(x)$
if $\pi(x)\in\\{{\mathrm{0}},{\mathrm{1}}\\}$. For partial assignments $\tau$
and $\pi$, this means that
${\hbox{{dom}}}(\tau\circ\pi)={\hbox{{dom}}}(\tau)\cup{\hbox{{dom}}}(\pi)$ and

$(\tau\circ\pi)(x)~{}=~{}\left\\{\begin{array}[]{ll}\pi(x){}{}{}{}&\hbox{if
$x\in{\hbox{{dom}}}(\pi)$}\\\ \tau(x)&\hbox{if
$x\in{\hbox{{dom}}}(\tau)\setminus{\hbox{{dom}}}(\pi)$.}\end{array}\right.$

######  Lemma 1.

For a set of clauses $\Gamma$ and substitutions $\tau$ and $\pi$,
$\Gamma_{{{|}}\tau\circ\pi}={(\Gamma_{{{|}}\pi})}_{{{|}}\tau}$. In particular,
$\tau\vDash\Gamma_{{{|}}\pi}$ if and only if $\tau\circ\pi\vDash\Gamma$.

######  Proof 1.1.

Notice $\tau\circ\pi\vDash C$ if and only if $\pi\vDash C$ or $(\pi\not\vDash
C\wedge\tau\vDash C_{{{|}}\pi})$. Thus

$\displaystyle{(\Gamma_{{{|}}\pi})}_{{{|}}\tau}$
$\displaystyle=\big{\\{}{(C_{{{|}}\pi})}_{{{|}}\tau}:C\in\Gamma,\
\pi\not\vDash C,\ \tau\not\vDash C_{{{|}}\pi}\big{\\}}$
$\displaystyle=\big{\\{}\tau\circ\pi(C)\setminus\\{0\\}:C\in\Gamma,\
\pi\not\vDash C,\ \tau\not\vDash C_{{{|}}\pi}\big{\\}}$
$\displaystyle=\big{\\{}C_{{{|}}\tau\circ\pi}:C\in\Gamma,\
\tau\circ\pi\not\vDash C\big{\\}}=\Gamma_{{{|}}\tau\circ\pi}.$

A set of clauses $\Gamma$ _semantically implies_ a clause $C$, written
$\Gamma\vDash C$, if every total assignment satisfying $\Gamma$ also satisfies
$C$. As is well-known, $\Gamma\vDash C$ holds if and only if there is a
_resolution derivation_ of some $C^{\prime}\subseteq C$; that is, $C^{\prime}$
is derived from $\Gamma$ using _resolution inferences_ of the form

$\ignorespaces\ignorespaces\ignorespaces\leavevmode\lower
55.88887pt\hbox{\vbox{\hbox{\hbox{\hskip 4.0pt\hbox{$p\,\dot{\lor}\,D$}\hskip
4.0pt}\hbox{\hskip 14.45377pt}\hbox{\hskip 4.0pt\hbox{$\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p$}}\,\dot{\lor}\,E$}\hskip 4.0pt}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 0.0pt\lower-0.2pt\hbox{}\hbox
to69.2536pt{\xleaders\hrule\hfill}\lower-0.2pt\hbox{}}\vskip
2.0pt\nointerlineskip\hbox{\hskip 16.81366pt\hbox{\hbox{\hskip
4.0pt\hbox{$D\lor E$}\hskip 4.0pt}}}}}\ignorespaces.$ (1)

If the derived clause $C^{\prime}$ is the empty clause $\perp$, then the
derivation is called a _resolution refutation_ of $\Gamma$. By the soundness
and completeness of resolution, $\Gamma\vDash\perp$, that is, $\Gamma$ is
unsatisfiable, if and only if there is a resolution refutation of $\Gamma$.

If either $D$ or $E$ is empty, then the resolution inference (1) is an
instance of _unit propagation_. A refutation using only such inferences is
called a _unit propagation refutation_. Recall that we can write  $C$ for the
set of unit clauses $\\{\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}:p\in C\\}$.

We write $\Gamma\vdash_{1}\bot$ to denote that there is a unit propagation
refutation of $\Gamma$. We define $\Gamma\vdash_{1}C$ to mean
$\Gamma\cup\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}\vdash_{1}\bot$.
For a set of clauses $\Delta$, we write $\Gamma\vdash_{1}\Delta$ to mean
$\Gamma\vdash_{1}C$ for every $C\in\Delta$.

######  Fact 2.

If $\Gamma\vdash_{1}\bot$ and $\alpha$ is any partial assignment or
substitution, then $\Gamma_{{{|}}\alpha}\vdash_{1}\bot$.

In the literature, when $\Gamma\vdash_{1}C$ then $C$ is said to be derivable
from $\Gamma$ by _reverse unit propagation_ (RUP), or is called an _asymmetric
tautology_ (AT) with respect to $\Gamma$ [Van08, JHB12, HHJW13b]. Of course,
$\Gamma\vdash_{1}C$ implies that $\Gamma\vDash C$. The advantage of working
with $\vdash_{1}$ is that there is a simple polynomial time algorithm to
determine whether $\Gamma\vdash_{1}C$. We have the following basic property of
$\vdash_{1}$ (going back to [Cha70]):

######  Lemma 3.

If $C$ is derivable from $\Gamma$ by a single resolution inference, then
$\Gamma\vdash_{1}C$. Conversely, if $\Gamma\vdash_{1}C$, then some
$C^{\prime}\subseteq C$ has a resolution derivation from $\Gamma$ of length at
most $n$, where $n$ is the total number of literals occurring in clauses in
$\Gamma$.

######  Proof 1.2.

First suppose that $C=D\lor E$ and clauses $p\,\dot{\lor}\,D$ and
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\,\dot{\lor}\,E$ appear in
$\Gamma$. Then by resolving these with the unit clauses in  $C$ we can derive
the two unit clauses $p$ and  $p$ , then resolve these together to get the
empty clause.

Now suppose that $\Gamma\vdash_{1}C$. Then there is a unit propagation
derivation of $\bot$ from $\Gamma\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$C$}}$, which is of length at most $n$. Removing all
resolutions against unit clauses  $p$ for $p\in C$, this can be turned into a
resolution derivation of $C$ or of some $C^{\prime}\subseteq C$ from $\Gamma$.

######  Lemma 4.

Let $C\lor D$ be a clause (so $C\cup D$ is not tautological), and set
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$. Then

$\Gamma_{{{|}}\alpha}\vdash_{1}D\setminus
C\quad\Longleftrightarrow\quad\Gamma_{{{|}}\alpha}\vdash_{1}D\quad\Longleftrightarrow\quad\Gamma\vdash_{1}C\lor
D.$

######  Proof 1.3.

The left-to-right directions are immediate from the definitions, since
$\Gamma_{{{|}}\alpha}$ is derivable from $\Gamma\cup\alpha$ using unit
propagation. To show that $\Gamma\vdash_{1}C\lor D$ implies
$\Gamma_{{{|}}\alpha}\vdash_{1}D\setminus C$, suppose
$\Gamma\cup\alpha\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$D$}}\vdash_{1}\bot$ and apply Fact 2.

###  1.2. Inference rules

We will describe a series if inference rules which can be used to add a clause
$C$ to a set of clauses $\Gamma$. In increasing order of strength the rules
are

$\rm{\hbox{\rm BC}}\leftarrow{\hbox{\rm RAT}}\leftarrow{\hbox{\rm
SPR}}\leftarrow{\hbox{\rm PR}}\leftarrow{\hbox{\rm SR}}.$

We will show that in each case the sets $\Gamma$ and $\Gamma\cup\\{C\\}$ are
_equisatisfiable_ , that is, either they are both satisfiable or both
unsatisfiable. The definitions follow [JHB12, HHJW13b, HKB19], except for the
new notion SR of “substitution redundancy”.444M. Heule [personal
communication, 2018] has independently formulated an inference rule
“permutation redundancy” (${\pi\hbox{\rm PR}}$) which allows only
substitutions which set some variables to constants and acts as a permutation
on the remaining literals. This is a special case of SR; but unlike SR,
${\pi\hbox{\rm PR}}$ does not allow identifying distinct literals. However, we
do not know the strength of ${{\pi\hbox{\rm PR}}^{-}}$ relative to
${{\hbox{\rm SR}}^{-}}$ (even if deletion is allowed for both systems). All of
these rules can be viewed as allowing the introduction of clauses that hold
“without loss of generality” [RS18]. The rules are summarized in a table
earlier in this section.

Let $\Gamma$ be a set of clauses and $C$ a clause with a distinguished literal
$p$, so that $C$ has the form $p\,\dot{\lor}\,C^{\prime}$.

[[Kul97, Kul99a]] The clause $C$ is a _blocked clause_ (BC) with respect to
$p$ and $\Gamma$ if, for every clause $D$ of the form $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p$}}\,\dot{\lor}\,D^{\prime}$ in $\Gamma$,
the set $C^{\prime}\cup D^{\prime}$ is tautological.

Notice that the condition “$C^{\prime}\cup D^{\prime}$ is tautological” above
would be equivalent to $\emptyset\vdash_{1}C^{\prime}\vee D^{\prime}$, except
that our notation does not allow us to write the expression $C^{\prime}\vee
D^{\prime}$ if $C^{\prime}\cup D^{\prime}$ is tautological, since it is not a
clause. Since  $p$ does not appear in $C^{\prime}$ or $D^{\prime}$, it would
also be equivalent to $\emptyset\vdash_{1}\penalty 10000p\vee\penalty
10000C^{\prime}\vee\penalty 10000D^{\prime}$. Compare with the definition of
RAT below.

[[JHB12, HB18, WHHJ14]] A clause $C$ is a _resolution asymmetric tautology_
(RAT) with respect to $p$ and $\Gamma$ if, for every clause $D$ of the form
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\,\dot{\lor}\,D^{\prime}$
in $\Gamma$, either $C^{\prime}\cup D^{\prime}$ is tautological or

$\Gamma\vdash_{1}p\lor C^{\prime}\lor D^{\prime}.$

Here we write $p\lor C^{\prime}$ instead of $C$ to emphasize that we include
the literal $p$ (some definitions of RAT omit it). Clearly, being BC implies
being RAT.

######  Example 5 ([Kul99b]).

Let $\Gamma$ be a set of clauses in which the variable $x$ does not occur, but
the variables $p$ and $q$ may occur. Consider the three clauses

$x\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q$}}\quad\quad\quad\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor p\quad\quad\quad\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor q$

which together express that $x\leftrightarrow(p\wedge q)$. Let
$\Gamma_{1}\subset\Gamma_{2}\subset\Gamma_{3}$ be $\Gamma$ with the three
clauses above successively added. Then $x\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$q$}}$
is BC with respect to $\Gamma$ and $x$, because no clause in $\Gamma$ contains
$x$ , so there is nothing to check. The second clause $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor p$ is BC with respect to
$\Gamma_{1}$ and  $x$ because the only clause in $\Gamma_{1}$ containing $x$
is $x\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q$}}$, and resolving this with $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor p$ gives a tautological conclusion.
The third clause $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor q$
is BC with respect to $\Gamma_{2}$ and  $x$ in a similar way.

It follows from the example that we can use the BC rule to simulate extended
resolution if we are allowed to introduce new variables; see Section 2.1.

We say the clause $C$ is RAT with respect to $\Gamma$ if it is RAT with
respect to $p$ and $\Gamma$ for some literal $p$ in $C$, and similarly for BC.

[[Kul99b, JHB12]] If $C$ is BC or RAT with respect to $\Gamma$, then $\Gamma$
and $\Gamma\cup\\{C\\}$ are equisatisfiable.

######  Proof 1.4.

It suffices to show that if $\Gamma$ is satisfiable, then so is
$\Gamma\cup\\{C\\}$. Let $\tau$ be any total assignment satisfying $\Gamma$.
We may assume $\tau\vDash\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$,
as otherwise we are done. Let $\tau^{\prime}$ be $\tau$ with the value of
$\tau(p)$ switched to satisfy $p$. Then $\tau^{\prime}$ satisfies $C$, along
with every clause in $\Gamma$ which does not contain  $p$ . Let
$D=\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}\,\dot{\lor}\,D^{\prime}$ be any clause in $\Gamma$ which
contains  $p$ . It follows from the RAT assumption that $\Gamma\vDash C\lor
D^{\prime}$, so $\tau\vDash D^{\prime}$ since $\tau\vDash\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$C$}}$. Hence $\tau^{\prime}\vDash
D^{\prime}$ and thus $\tau^{\prime}\vDash D$. This shows that
$\tau^{\prime}\vDash\Gamma\cup\\{C\\}$.

For the rest of this section, let $\alpha$ be the partial assignment  $C$ . In
a moment we will introduce the rules SPR, PR and SR. These are variants of a
common form, and we begin by showing that RAT can also be expressed in a
similar way (in the literature this form of RAT is called _literal propagation
redundant_ or LPR).

[[HKB19]] A clause $C$ is RAT with respect to $p$ and $\Gamma$ if and only if
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ where $\tau$ is the partial
assignment identical to $\alpha$ except at $p$, with $\tau(p)=1$.

######  Proof 1.5.

First suppose that $C$ satifies the second condition. Consider any clause $D$
of the form $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}\,\dot{\lor}\,D^{\prime}$ in $\Gamma$. We need to show
that either $C\cup D^{\prime}$ is tautological or $\Gamma\vdash_{1}C\lor
D^{\prime}$. Suppose $C\cup D^{\prime}$ is not tautological. Then
$\alpha\not\vDash D^{\prime}$, $\tau\not\vDash D$, and by Lemma 4 it is enough
to show $\Gamma_{{{|}}\alpha}\vdash_{1}D^{\prime}$. But this now follows from
$\Gamma_{{{|}}\alpha}\vdash_{1}D_{{{|}}\tau}$, since
$D_{{{|}}\tau}={D^{\prime}}_{{{|}}\alpha}\subseteq D^{\prime}$.

Now suppose $C$ is RAT with respect to $p$ and $\Gamma$. Consider any
$D\in\Gamma$ such that $\tau\not\vDash D$ and thus
$D_{{{|}}\tau}\in\Gamma_{{{|}}\tau}$. We must show that
$\Gamma_{{{|}}\alpha}\vdash_{1}D_{{{|}}\tau}$. If $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p$}}\notin D$ this is trivial, since then
$D_{{{|}}\tau}=D_{{{|}}\alpha}\in\Gamma_{{{|}}\alpha}$. Otherwise
$D=\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}\,\dot{\lor}\,D^{\prime}$, where $\alpha\not\vDash
D^{\prime}$ since $\tau\not\vDash D$, so $C\cup D^{\prime}$ is not
tautological. By the RAT property, $\Gamma\vdash_{1}C\lor D^{\prime}$. By
Lemma 4 this implies $\Gamma_{{{|}}\alpha}\vdash_{1}D^{\prime}\setminus C$.
But $D^{\prime}\setminus C={D^{\prime}}_{{{|}}\alpha}=D_{{{|}}\tau}$.

[[HKB19]] A clause $C$ is _subset propagation redundant_ (SPR) with respect to
$\Gamma$ if there is a partial assignment $\tau$ with
${\hbox{{dom}}}(\tau)={\hbox{{dom}}}(\alpha)$ such that $\tau\vDash C$ and
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$.

[[HKB19]] A clause $C$ is _propagation redundant_ (PR) with respect to
$\Gamma$ if there is a partial assignment $\tau$ such that $\tau\vDash C$ and
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}.$

A clause $C$ is _substitution redundant_ (SR) with respect to $\Gamma$ if
there is a substitution $\tau$ such that $\tau\vDash C$ and
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$.

######  Example 6 (based on [HKB19]).

Let $\Gamma$ be the pigeonhole principle $\mathrm{PHP}_{n}$ (see Section 4.1)
in variables $p_{i,j}$ expressing that pigeon $i$ goes to hole $j$. Let $C$ be
the clause $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{1,0}$}}\vee
p_{0,0}$ so that $\alpha$ is the partial assignment $p_{1,0}\wedge\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{0,0}$}}$.

Let $\pi$ be the substitution which swaps pigeons $0$ and $1$; that is,
$\pi(p_{0,j})=p_{1,j}$ and $\pi(p_{1,j})=p_{0,j}$ for every hole $j$, and
$\pi$ is otherwise the identity. Notice that, by the symmetries of the
pigeonhole principle, $\Gamma_{{{|}}\pi}=\Gamma$ and thus
$\Gamma_{{{|}}\alpha}={(\Gamma_{{{|}}\pi})}_{{{|}}\alpha}=\Gamma_{{{|}}\alpha\circ\pi}$.
Let $\tau=\alpha\circ\pi$, so $\tau$ is the same as $\pi$ except that
$\tau(p_{0,0})=1$ and $\tau(p_{1,0})=0$.

Then $\tau\vDash C$ and $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$
(since they are the same set of clauses). Hence we have shown that $C$ is SR
with respect to $\Gamma$.

We go on to sketch a polynomial size ${{\hbox{\rm DSR}}^{-}}$ refutation of
$\Gamma$, that is, one that uses SR inferences, resolution and deletion but
introduces no new variables (see Section 1.4 below). Resolve $C$ with the hole
axiom $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{1,0}$}}\vee\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{0,0}$}}$ to derive the unit clause  $p_{1,0}$ . Delete $C$,
so that we are now working with the set of clauses $\Gamma\cup\\{\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{1,0}$}}\\}$. Let $C^{\prime}$ be the
clause $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{2,0}$}}\vee p_{0,0}$
and let $\alpha^{\prime}$ be its negation $p_{2,0}\wedge\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{0,0}$}}$. Let $\pi^{\prime}$ be the
substitution which swaps pigeons $0$ and $2$ and let
$\tau^{\prime}=\alpha^{\prime}\circ\pi^{\prime}$. As before
$\tau^{\prime}\vDash C^{\prime}$ and ${(\Gamma\cup\\{\vbox{\hrule
height=0.5pt\kern
1.07639pt\hbox{$p_{1,0}$}}\\})}_{{{|}}\alpha^{\prime}}\vdash_{1}{(\Gamma\cup\\{\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{1,0}$}}\\})}_{{{|}}\tau^{\prime}}$, since
neither $\alpha^{\prime}$ nor $\tau^{\prime}$ affects $p_{1,0}$ so these are
again the same set of clauses. Hence we may derive $C^{\prime}$ by a SR
inference, then resolve with the hole axiom $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{2,0}$}}\vee\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{0,0}$}}$ to get  $p_{2,0}$ .

Carrying on in this way, we eventually derive $\Gamma\cup\\{\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{1,0}$}}\\}\cup\dots\cup\\{\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{n-1,0}$}}\\}$. We now resolve each unit
clause  $p_{i,0}$ with the pigeon axiom for pigeon $i$, for $i=1,\dots,n-1$.
After some deletions, we are left with clauses asserting that pigeons
$1,\dots,n-1$ map injectively to holes $1,\dots,n-2$. This is essentially
$\mathrm{PHP}_{n-1}$. We carry on inductively to derive $\mathrm{PHP}_{n-2}$
etc. and can easily derive a contradiction when we get to $\mathrm{PHP}_{2}$.

Section 4.1 contains a more careful version of this argument, refuting
$\mathrm{PHP}_{n}$ using SPR inferences and no deletion.

######  Theorem 7.

If $C$ is SR with respect to $\Gamma$, then $\Gamma$ and $\Gamma\cup\\{C\\}$
are equisatisfiable. Hence the same is true for SPR and PR.

Theorem 7 trivially implies the same statement for BC and RAT (this was
Theorem 5 above).

######  Proof 1.6.

Again it is sufficient to show that if $\Gamma$ is satisfiable, then so is
$\Gamma\cup\\{C\\}$. Suppose we have a substitution $\tau$ such that
$\tau\vDash C$ and $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$. Let
$\pi$ be any total assignment satisfying $\Gamma$. If $\pi\vDash C$ then we
are done. Otherwise $\pi\vDash\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$C$}}$, so $\pi\supseteq\alpha$ and $\pi$ satisfies
$\Gamma_{{{|}}\alpha}$ by Lemma 1. Thus, by the assumption,
$\pi\vDash\Gamma_{{{|}}\tau}$. Therefore $\pi\circ\tau\vDash\Gamma$ by Lemma
1, and $\pi\circ\tau\vDash C$ since $\tau\vDash C$.

This proof of Theorem 7 still goes through if we replace
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ with the weaker assumption
that $\Gamma_{{{|}}\alpha}\vDash\Gamma_{{{|}}\tau}$. The advantage of using
$\vdash_{1}$ is that it is efficiently checkable. Consequently, the conditions
of being BC, RAT, SPR, PR or SR with respect to $\Gamma$ are all polynomial-
time checkable, as long as we include the partial assignment or substitution
$\tau$ as part of the input.

###  1.3. Proof systems with new variables

This section introduces proof systems based on the BC, RAT, SPR, PR and SR
inferences. Some of the systems also allow the use of the deletion rule: these
systems are denoted DBC, DRAT, etc. All the proof systems are _refutation
systems_. They start with a set of clauses $\Gamma$, and successively derive
sets $\Gamma_{i}$ of clauses, first $\Gamma_{0}=\Gamma$, then
$\Gamma_{1},\Gamma_{2},\ldots,\Gamma_{m}$ until reaching a set $\Gamma_{m}$
containing the empty clause. It will always be the case that if $\Gamma_{i}$
is satisfiable, then $\Gamma_{i+1}$ is satisfiable. Since the empty clause
$\perp$ is in $\Gamma_{m}$, this last set is not satisfiable. This suffices to
show that $\Gamma$ is not satisfiable.

A BC, RAT, SPR, PR or SR proof (a refutation) of $\Gamma$ is a sequence
$\Gamma_{0},\ldots,\Gamma_{m}$ such that $\Gamma_{0}=\Gamma$,
$\perp\in\Gamma_{m}$ and each $\Gamma_{i+1}=\Gamma_{i}\cup\\{C\\}$, where
either

  * •

$\Gamma_{i}\vdash_{1}C$ or

  * •

$C$ is BC, RAT, SPR, PR, or SR (respectively) with respect to $\Gamma_{i}$.

For BC or RAT steps, the proof must specify which $p$ is used, and for SPR, PR
or SR, it must specify which $\tau$.

There is no constraint on the variables that appear in clauses $C$ introduced
in BC, RAT, etc. steps. They are free to include new variables that did not
occur in $\Gamma_{0},\dots,\Gamma_{i}$.

A DBC, DRAT, DSPR, DPR or DSR proof allows the same rules of inference
(respectively) as Definition 1.3, plus the _deletion_ inference rule:

  * •

$\Gamma_{i+1}=\Gamma_{i}\setminus\\{C\\}$ for some $C\in\Gamma_{i}$.

Resolution can be simulated by RUP inferences (Lemma 3), so all the systems
introduced in this and the next subsection simulate resolution. Furthermore,
by Theorems 5 and 7, they are sound. Since the inferences are defined using
$\vdash_{1}$, they are polynomial time verifiable, as the description of
$\tau$ is included with every SPR, PR or SR inference. Hence they are all
proof systems in the sense of Cook-Reckhow [CR74, CR79].

The deletion rule deserves more explanation. First, we allow _any_ clause to
be deleted, even the initial clauses from $\Gamma$. So it is possible that
$\Gamma_{i}$ is unsatisfiable but $\Gamma_{i+1}$ is satisfiable after a
deletion. For us, this is okay since we focus on refuting sets of
unsatisfiable clauses, not on finding satisfying assignments of satisfiable
sets of clauses. SAT solvers generally wish to maintain the equisatisfiability
property: they use deletion extensively to prune the search time, but are
careful only to perform deletions that preserve both satisfiability and
unsatisfiability, generally as justified by the BC or RAT rules. Since
applying RAT, or more generally PR or SR, can change the satisfying
assignment, a SAT solver may also need to keep a proof log with information
about how to reverse the steps of the proof once a satisfying assignment is
found (see [JHB12]).

Second, deletion is important for us because the property of being BC, RAT
etc. involves a universal quantification over the current set of clauses
$\Gamma_{i}$. So deletion can make the systems more powerful, as removing
clauses from $\Gamma_{i}$ can make more inferences possible. For example, the
unit clause $x$ is BC with respect to the set $\\{x\lor y\\}$, since the
literal  $x$ does not appear, but is not even SR with respect to the set
$\\{x\lor y,\,\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\\}$, since
$\\{x\lor y,\,\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\\}$ and
$\\{x\lor y,\,\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}},\,x\\}$ are
not equisatisfiable. An early paper on this by Kullmann [Kul99b] exploited
deletions to generalize the power of BC inferences.

As we will show in Section 2, all the systems defined so far are equivalent to
extended resolution, because of the ability to freely introduce new variables.
The main topic of the paper is the systems we introduce next, which lack this
ability.

###  1.4. Proof systems without new variables

A BC refutation of $\Gamma$ _without new variables_ , or, for short, a
${{\hbox{\rm BC}}^{-}}$ refutation of $\Gamma$, is a BC refutation of $\Gamma$
in which only variables from $\Gamma$ appear. The systems ${{\hbox{\rm
RAT}}^{-}}$, ${{\hbox{\rm PR}}^{-}}$ etc. and ${{\hbox{\rm DBC}}^{-}}$,
${{\hbox{\rm DRAT}}^{-}}$, ${{\hbox{\rm DPR}}^{-}}$ etc. are defined
similarly.

There is an alternative natural definition of “without new variables”, which
requires not just that a refutation of $\Gamma$ uses only variables that are
used in $\Gamma$, but also that once a variable has been eliminated from all
clauses through the use of deletion, it may not be reused subsequently in the
refutation. An equivalent way to state this is that a clause $C$ inferred by a
BC, RAT, SPR, PR or SR inference cannot involve any variable which does not
occur in the _current_ set of clauses.

This stronger definition is in fact essentially equivalent to Definition 1.4,
for a somewhat trivial reason. More precisely, any refutation that satisfies
Definition 1.4 can be converted into a refutation that satisfies the stronger
condition with at worst a polynomial increase in the size of the refutation.
We state the proof for ${{\hbox{\rm DBC}}^{-}}$, but the same argument works
verbatim for the other systems ${{\hbox{\rm DRAT}}^{-}}$, ${{\hbox{\rm
DSPR}}^{-}}$, ${{\hbox{\rm DPR}}^{-}}$ and ${{\hbox{\rm DSR}}^{-}}$.

Suppose $\Pi$ is a ${{\hbox{\rm DBC}}^{-}}$ refutation of $\Gamma$ in the
sense of Definition 1.3, and consider a variable $x$. Suppose $x$ is present
in $\Gamma=\Gamma_{0}$ and in $\Gamma_{i}$, is not present in $\Gamma_{i+1}$
through $\Gamma_{j}$, but is present again in $\Gamma_{j+1}$. The derivation
of $\Gamma_{i+1}$ from $\Gamma_{i}$ deleted a single clause $x\lor C$; for
definiteness we assume this clause contains $x$ positively. The derivation of
$\Gamma_{j+1}$ introduced a clause $x\lor D$ with a BC inference; we may
assume without loss of generality that $x$ occurs with the same sign in $x\lor
D$ as in $x\lor C$, since otherwise the sign of $x$ could be changed
throughout the refutation from $\Gamma_{j+1}$ onwards.

The refutation $\Pi$ is modified as follows. Before deleting the clause $x\lor
C$, infer the unit clause $x$ by a BC inference; this is valid trivially,
since  $x$ does not occur in $\Gamma_{i}$. Then continue the derivation with
the unit clause $x$ added to $\Gamma_{i},\ldots,\Gamma_{j}$. Since there are
no other uses of $x$ in $\Gamma_{i},\ldots,\Gamma_{j}$, these steps in the
refutation remain valid (by part (b) of Lemma 8 below). Upon reaching
$\Gamma_{j}$, infer $x\lor D$ with a BC inference relative to the variable
$x$. This is allowed since  $x$ does not appear in $\Gamma_{j}$. Then delete
the unit clause $x$ to obtain again $\Gamma_{j+1}$. Repeating this for every
gap in $\Pi$ where $x$ disappears, and then doing the same construction for
every variable, yields a ${{\hbox{\rm DBC}}^{-}}$ refutation that satisfies
the stronger condition.

###  1.5. Two useful lemmas

We conclude this subsection with two technical lemmas, which we will use in
several places to simplify the construction of proofs.

All the inference rules BC, RAT, SPR, PR and SR are “non-monotone”, in the
sense that it is possible that
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ holds but
$\Gamma^{\prime}_{{{|}}\alpha}\vdash_{1}\Gamma^{\prime}_{{{|}}\tau}$ fails,
for $\Gamma\subseteq\Gamma^{\prime}$. In particular, adding more clauses to
$\Gamma$ may invalidate a BC, RAT, SPR, PR or SR inference. Conversely,
removing clauses from $\Gamma$ may allow new clauses to be inferred by one of
these inferences. This is one reason for the importance of the deletion rule.

The next lemma is a useful technical tool that will sometimes let us avoid
using deletion. It states conditions under which the extra clauses in
$\Gamma^{\prime}$ do not invalidate a RAT, SPR, PR or SR inference.555The
conclusion of Lemma 8 is true also for BC inferences.

A clause $C$ _subsumes_ a clause $D$ if $C\subseteq D$. A set $\Gamma$ of
clauses _subsumes_ a set $\Gamma^{\prime}$ if each clause of $\Gamma^{\prime}$
is subsumed by some clause of $\Gamma$.

######  Lemma 8.

Suppose $\alpha$ and $\tau$ are substitutions and
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ holds. Also suppose
$\Gamma\subseteq\Gamma^{\prime}$.

  1. (1)

If $\Gamma$ subsumes $\Gamma^{\prime}$, then
$\Gamma^{\prime}_{{{|}}\alpha}\vdash_{1}\Gamma^{\prime}_{{{|}}\tau}$.

  2. (2)

If $\Gamma^{\prime}$ is $\Gamma$ plus one or more clauses involving only
variables that are not in the domain of either $\alpha$ or $\tau$, then
$\Gamma^{\prime}_{{{|}}\alpha}\vdash_{1}\Gamma^{\prime}_{{{|}}\tau}$.

Consequently, in either case, if $C$ can be inferred from $\Gamma$ by a RAT,
SPR, PR or SR rule, then $C$ can also be inferred from $\Gamma^{\prime}$ by
the same rule.

######  Proof 1.7.

We prove (a). Suppose $D\in\Gamma^{\prime}$ and $\tau\not\vDash D$. We must
show $\Gamma^{\prime}_{{{|}}\alpha}\vdash_{1}D_{{{|}}\tau}$. Let $E\in\Gamma$
with $E\subseteq D$. Then $\tau\not\vDash E$, so by assumption
$\Gamma_{{{|}}\alpha}\vdash_{1}E_{{{|}}\tau}$. Also $E_{{{|}}\tau}\subseteq
D_{{{|}}\tau}$, so $\Gamma_{{{|}}\alpha}\vdash_{1}D_{{{|}}\tau}$. It follows
that $\Gamma^{\prime}_{{{|}}\alpha}\vdash_{1}D_{{{|}}\tau}$, since
$\Gamma\subseteq\Gamma^{\prime}$.

The proof of (b) is immediate from the definitions.

Our last lemma gives a kind of normal form for propagation redundancy. Namely,
it implies that when $C$ is PR with respect to $\Gamma$, we may assume without
loss of generality that ${\hbox{{dom}}}(\tau)$ includes
${\hbox{{dom}}}(\alpha)$. We will use this later to show a limited simulation
of PR by SPR.

######  Lemma 9.

Suppose $C$ is PR with respect to $\Gamma$, witnessed by a partial assignment
$\tau$. Then we have
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\alpha\circ\tau}$, where $\alpha$
is the partial assignment  $C$ .

######  Proof 1.8.

Let $\pi=\alpha\circ\tau$. Suppose $E\in\Gamma$ is such that $\pi\not\vDash
E$. We must show that $\Gamma_{{{|}}\alpha}\vdash_{1}E_{{{|}}\pi}$. We can
decompose $E$ as $E_{1}\lor E_{2}\lor E_{3}$ where $E_{1}$ contains the
literals in ${\hbox{{dom}}}(\tau)$, $E_{2}$ contains the literals in
${\hbox{{dom}}}(\alpha)\setminus{\hbox{{dom}}}(\tau)$ and $E_{3}$ contains the
remaining literals. Then $E_{{{|}}\tau}=E_{2}\lor E_{3}$ and by the PR
assumption $\Gamma_{{{|}}\alpha}\vdash_{1}E_{{{|}}\tau}$, so there is a
derivation $\Gamma_{{{|}}\alpha}\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E_{2}$}}\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E_{3}$}}\vdash_{1}\bot$. But neither $\Gamma_{{{|}}\alpha}$
nor  $E_{3}$ contain any variables from ${\hbox{{dom}}}(\alpha)$, so the
literals in  $E_{2}$ are not used in this derivation. Hence
$\Gamma_{{{|}}\alpha}\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E_{3}$}}\vdash_{1}\bot$, which completes the proof since
$E_{3}=E_{{{|}}\pi}$.

##  2\. Relations with extended resolution

###  2.1. With new variables

It is known that RAT, and even BC, can simulate extended resolution if new
variables are allowed [Kul99b]. In extended resolution for any variables $p,q$
we are allowed to introduce a new variable $x$ together with three clauses
expressing that $x\leftrightarrow(p\wedge q)$. As shown in Example 5, we can
instead introduce these clauses using BC inferences. Thus all the systems
described above which allow new variables simulate extended resolution. The
converse holds as well:

######  Theorem 10.

The system ER simulates DSR, and hence every other system above.

######  Proof 2.1.

(Sketch) It is known that the theorem holds for DPR in place of DSR. Namely,
[KRPH18] gives an explicit simulation of DRAT by extended resolution, and
[HB18] gives an explicit simulation of DPR by DRAT. Thus extended resolution
simulates DPR.

We sketch a direct proof of the simulation of DSR by extended resolution.
Suppose $\Gamma_{0},\ldots,\Gamma_{m}$ is a DSR proof and in particular
$\Gamma_{i+1}=\Gamma_{i}\cup\\{C\\}$ is introduced by an SR inference from
$\Gamma_{i}$ with a substitution $\tau$. Let $x_{1},\dots,x_{s}$ be all
variables occurring in $\Gamma_{i+1}$ including any new variables introduced
in $C$. Using the extension rule, introduce new variables
$x_{1}^{\prime},\ldots,x_{s}^{\prime}$ along with extension variables and
extension axioms expressing

$x_{j}^{\prime}~{}{\leftrightarrow}~{}(x_{j}\land C)\lor(\tau(x_{j})\land\lnot
C).$

Here $\tau(x_{j})$ stands for a fixed symbol from
${\hbox{{Lit}}}\cup\\{0,1\\}$. Let $\Gamma_{i+1}(\vec{x}/\vec{x}^{\prime})$ be
the set of clauses obtained from $\Gamma_{i}$ by replacing each variable
$x_{j}$ with $x_{j}^{\prime}$. It can be proved using only resolution, using
the extension axioms, that if all clauses in $\Gamma_{i}$ hold then all
clauses in $\Gamma_{i+1}(\vec{x}/\vec{x}^{\prime})$ hold. The extended
resolution proof then proceeds inductively on $i$ using the new variables
$x_{j}^{\prime}$ in place of the old variables $x_{j}$.

Another way to prove the full theorem is via the theories of bounded
arithmetic $S^{1}_{2}$ [Bus86] and PV [Coo75]. Namely, suppose we are given a
DSR proof $\Gamma_{0},\ldots,\Gamma_{m}$ and a satisfying assignment $\pi_{0}$
for $\Gamma_{0}$. By induction, there exists a satisfying assignment $\pi_{i}$
for each $\Gamma_{i}$. The inductive step, for an SR rule deriving
$\Gamma_{i+1}=\Gamma_{i}\cup\\{C\\}$, witnessed by a substitution $\tau$, is
to set $\pi_{i+1}=\pi_{i}$ if $\pi_{i}\vDash C$ and otherwise to set
$\pi_{i+1}=\pi_{i}\circ\tau$, as in the proof of Theorem 7. The inductive
hypothesis can be written as a $\Sigma^{b}_{1}$ formulas and the induction has
$m$ steps, so this is formally $\Sigma^{b}_{1}$ length-induction (or
$\Sigma^{b}_{1}$-LIND) which is available in $S^{1}_{2}$. Thus $S^{1}_{2}$ can
prove the soundness of DSR. By conservativity of $S^{1}_{2}$ over PV [Bus86],
the theory PV also proves the soundness of DSR. A fundamental property of PV
is that PV proofs translate into uniform families of polynomial size extended
resolution refutations [Coo75]. Thus ER efficiently proves the soundness of
DSR. It follows that ER simulates DSR.

###  2.2. Without new variables

In the systems without the ability to freely add new variables, we can still
imitate extended resolution by adding dummy variables to the formula we want
to refute. This was observed already in [Kul99b].

For $m\geq 1$, define $X^{m}$ to be the set consisting of only the two clauses

$y\lor x_{1}\lor\dots\lor x_{m}\qquad\hbox{and}\qquad y.$

######  Lemma 11.

Suppose $\Gamma$ has an ER refutation $\Pi$ of size $m$, and that $\Gamma$ and
$X^{m}$ have no variables in common. Then $\Gamma\cup X^{m}$ has a
${{\hbox{\rm BC}}^{-}}$-refutation $\Pi^{*}$ of size $O(m)$, which can
furthermore be constructed from $\Pi$ in polynomial time.

######  Proof 2.2.

We describe how to change $\Pi$ into $\Pi^{*}$. We first rename all extension
variables to use names from $\\{x_{1},\dots,x_{m}\\}$ and replace all
resolution steps with $\vdash_{1}$ inferences. Now consider an extension rule
in $\Pi$ which introduces the three extension clauses (5) expressing $x_{i}\
{\leftrightarrow}\ (p\land q)$, where we may assume that $p$ and $q$ are
either variables of $\Gamma$ or from $\\{x_{1},\dots,x_{i-1}\\}$. We simulate
this by introducing successively the three clauses

$x_{i}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q$}}\quad\quad\quad\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}_{i}\lor p\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$y$}}\quad\quad\quad\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}_{i}\lor q\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$y$}}$

using the BC rule. The first clause, $x_{i}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$q$}}$,
is BC with respect to $x_{i}$, because $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{i}$ has not appeared yet. The second clause is BC with
respect to  $x_{i}$ , because $x_{i}$ appears only in two earlier clauses,
namely $y\lor x_{1}\lor\dots\lor x_{m}$, which contains $y$, and
$x_{i}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q$}}$, which contains  $p$ . In both cases
the resolvent with $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{i}\lor p\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$y$}}$ is tautological. The third clause is similar. The unit
clause $y$ is in $X^{m}$, so we can then derive the remaining two needed
extension clauses $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}_{i}\lor
p$ and $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}_{i}\lor q$ by two
$\vdash_{1}$ inferences.

In the terminology of [PS10], Lemma 11 shows that ${{\hbox{\rm BC}}^{-}}$
_effectively simulates_ ER, in that we are allowed to transform the formula as
well as the refutation when we move from ER to ${{\hbox{\rm BC}}^{-}}$.

The next corollary is essentially from [Kul99b]. It shows how to use the lemma
to construct examples of usually-hard formulas which have short proofs in
${{\hbox{\rm BC}}^{-}}$. (We will give less artificial examples of short
${{\hbox{\rm SPR}}^{-}}$ proofs in Section 4.) Let $m(n)$ be the polynomial
size upper bound on ER refutations of the pigeonhole principle
$\mathrm{PHP}_{n}$ which follows from [CR79] — see Section 4.1 for the
definition of the $\mathrm{PHP}_{n}$ clauses.

######  Corollary 12.

The set of clauses $\mathrm{PHP}_{n}\cup X^{m(n)}$ has polynomial size proofs
in ${{\hbox{\rm BC}}^{-}}$, but requires exponential size proofs in constant
depth Frege.

######  Proof 2.3.

The upper bound follows from Lemma 11. For the lower bound, let $\Pi$ be a
refutation in depth-$d$ Frege. Then we can restrict $\Pi$ by setting $y=1$ to
obtain a depth-$d$ refutation of $\mathrm{PHP}_{n}$ of the same size. By
[KPW95, PBI93], this must have exponential size.

The same argument can give a more general result. A propositional proof system
${\mathcal{P}}$ is _closed under restrictions_ if, given any
${\mathcal{P}}$-refutation of $\Gamma$ and any partial assignment $\rho$, we
can construct a ${\mathcal{P}}$-refutation of $\Gamma_{{{|}}\rho}$ in
polynomial time. ([BKS04] called such systems “natural”.) Most of the
commonly-studied proof systems such as resolution, Frege, etc. are closed
under restrictions. On the other hand, it follows from results in this paper
that ${{\hbox{\rm BC}}^{-}}$ and ${{\hbox{\rm RAT}}^{-}}$ are not closed under
restrictions. To see this, let $\Gamma$ be ${\mathrm{BPHP}}_{n}\cup X^{m(n)}$
where ${\mathrm{BPHP}}_{n}$ is the bit pigeonhole principle (see Section 4.2)
and $m$ is a suitable function. Then $\Gamma$ has short ${{\hbox{\rm
BC}}^{-}}$ refutations, since ${\mathrm{BPHP}}_{n}$ has short refutations in
ER. But ${\mathrm{BPHP}}_{n}$ is a restriction of $\Gamma$, as in Corollary
12, and has no short ${{\hbox{\rm RAT}}^{-}}$ refutations by Theorem 33 below.

######  Theorem 13.

Let ${\mathcal{P}}$ be any propositional proof system which is closed under
restrictions. If ${\mathcal{P}}$ simulates ${{\hbox{\rm BC}}^{-}}$, then
${\mathcal{P}}$ simulates ER.

######  Proof 2.4.

Suppose $\Gamma$ has a refutation $\Pi$ in ER of length $m$. Take a copy of
$X^{m}$ in disjoint variables from $\Gamma$. By Lemma 11 we can construct a
${{\hbox{\rm BC}}^{-}}$-refutation of $\Gamma\cup X^{m}$. Since
${\mathcal{P}}$ simulates ${{\hbox{\rm BC}}^{-}}$, we can then construct a
${\mathcal{P}}$-refutation of $\Gamma\cup X^{m}$. Let $\rho$ be the
restriction which just sets $y=1$, so that ${(\Gamma\cup
X^{m})}_{{{|}}\rho}=\Gamma$. By the assumption that ${\mathcal{P}}$ is closed
under restrictions, we can construct a ${\mathcal{P}}$ refutation of $\Gamma$.
All constructions are polynomial time.

######  Corollary 14.

If the Frege proof system simulates ${{\hbox{\rm BC}}^{-}}$, then Frege and ER
are equivalent.

Hence it is unlikely that Frege simulates ${{\hbox{\rm BC}}^{-}}$, since Frege
is expected to be strictly weaker than ER.

###  2.3. Canonical NP pairs

The notion of _disjoint NP pairs_ was first introduced by Grollmann and Selman
[GS88]. Razborov [Raz94] showed how a propositional proof system
${\mathcal{P}}$ gives rise to a canonical disjoint NP pair, which gives a
measure of the strength of the system. It is known that if a propositional
proof system ${\mathcal{P}}_{1}$ simulates a system ${\mathcal{P}}_{2}$, then
there is a many-one reduction from the canonical NP pair for
${\mathcal{P}}_{2}$ to the canonical NP pair for ${\mathcal{P}}_{1}$ [Raz94,
Pud03]. We can use Lemma 11 to prove that the systems ${{\hbox{\rm BC}}^{-}}$
through ${{\hbox{\rm DSR}}^{-}}$ cannot be distinguished from each other or ER
by their canonical NP pairs, even though they do not all simulate each other.

A _disjoint NP pair_ is a pair $(U,V)$ of NP sets such that $U\cap
V=\emptyset$. A _many-one reduction_ from a disjoint NP pair $(U,V)$ to a
disjoint NP pair $(U^{\prime},V^{\prime})$ is a polynomial time function $f$
mapping $U$ to $U^{\prime}$ and mapping $V$ to $V^{\prime}$.

To motivate this definition a little, a disjoint NP pair $(U,V)$ is said to be
_polynomially separable_ if there is a polynomial time function $f$ which,
given $x\in U\cup V$, correctly identifies whether $x\in U$ or $x\in V$.
Clearly if $(U,V)$ is many-one reducible to $(U^{\prime},V^{\prime})$, then if
$(U^{\prime},V^{\prime})$ is polynomially separable so is $(U,V)$.

${\mathrm{SAT}}$ is the set of pairs $(\Gamma,1^{m})$ such that $\Gamma$ is a
satisfiable set of clauses and $m\geq 1$ is an arbitrary integer. Let
${\mathcal{P}}$ be a propositional proof system for refuting sets of clauses.
Then ${\mathrm{REF}}({\mathcal{P}})$ is the set of pairs $(\Gamma,1^{m})$ such
that $\Gamma$ has a ${\mathcal{P}}$-refutation of length at most $m$. Notice
that ${\mathrm{SAT}}$ and ${\mathrm{REF}}({\mathcal{P}})$ are both NP. We
define the _canonical disjoint NP pair_ , or _canonical NP pair_ , associated
with ${\mathcal{P}}$ to be $({\mathrm{REF}}({\mathcal{P}}),{\mathrm{SAT}})$.

The canonical NP pair for a proof system ${\mathcal{P}}$ defines the following
problem. Given a pair $(\Gamma,1^{m})$, the soundness of ${\mathcal{P}}$
implies that it is impossible that both (a) $\Gamma$ is satisfiable and (b)
$\Gamma$ has a proof in ${\mathcal{P}}$ of length $\leq m$. The promise
problem is to identify one of (a) and (b) which does _not_ hold. (If neither
(a) nor (b) holds, then either answer may be given.)

######  Theorem 15.

There are many-one reductions in both directions between the canonical NP pair
for ER and the canonical NP pairs for all the systems in Section 1.3.

######  Proof 2.5.

As a simulation implies a reduction between canonical NP pairs, all we need to
show is a reduction of the canonical NP pair for ER to the canonical NP pair
for the weakest system ${{\hbox{\rm BC}}^{-}}$, that is, of
$({\mathrm{REF}}({\hbox{\rm ER}}),{\mathrm{SAT}})$ to
$({\mathrm{REF}}({{\hbox{\rm BC}}^{-}}),{\mathrm{SAT}})$. Suppose
$(\Gamma,1^{m})$ is given as a query to $({\mathrm{REF}}({\hbox{\rm
ER}}),{\mathrm{SAT}})$. We must produce some $\Gamma^{*}$ and $m^{*}$ such
that

  1. (1)

$\Gamma^{*}$ is satisfiable if $\Gamma$ is,

  2. (2)

$\Gamma^{*}$ has a ${{\hbox{\rm BC}}^{-}}$-refutation of size $m^{*}$ if
$\Gamma$ has an ER-refutation of size $m$, and

  3. (3)

$m^{*}$ is bounded by a polynomial in $m$.

We use Lemma 11, letting $\Gamma^{*}$ be $\Gamma\cup X^{m}$ for $X^{m}$ in
variables disjoint from $\Gamma$, and letting $m^{*}$ be the bound on the size
of the ${{\hbox{\rm BC}}^{-}}$-refutation of $\Gamma^{*}$.

##  3\. Simulations

###  3.1. ${{\hbox{\rm DRAT}}^{-}}$ simulates ${{\hbox{\rm DPR}}^{-}}$

The following relations were known between ${{\hbox{\rm DBC}}^{-}}$,
${{\hbox{\rm DRAT}}^{-}}$ and ${{\hbox{\rm DPR}}^{-}}$.

[[KRPH18]] ${{\hbox{\rm DBC}}^{-}}$ simulates ${{\hbox{\rm DRAT}}^{-}}$.
(Hence they are equivalent).

[[HB18]] Suppose $\Gamma$ has a DPR refutation $\Pi$. Then it has a DRAT
refutation constructible in polynomial time from $\Pi$, using at most one
variable not appearing in $\Pi$.

We prove:

######  Theorem 16.

${{\hbox{\rm DRAT}}^{-}}$ simulates ${{\hbox{\rm DPR}}^{-}}$.

Hence the systems ${{\hbox{\rm DBC}}^{-}}$, ${{\hbox{\rm DRAT}}^{-}}$,
${{\hbox{\rm DSPR}}^{-}}$ and ${{\hbox{\rm DPR}}^{-}}$ are all equivalent. The
theorem relies on the following main lemma used in the proof of Theorem 3.1.
We include a proof for completeness.

[[HB18]] Suppose $C$ is PR with respect to $\Gamma$. Then there is a
polynomial size DRAT derivation of $\Gamma\cup\\{C\\}$ from $\Gamma$, using at
most one variable not appearing in $\Gamma$ or $C$.

######  Proof 3.1.

We have $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$, where
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$ and $\tau\vDash
C$. Let $x$ be a new variable. We describe the construction step-by-step.

_Step 1._ For each $D\in\Gamma$ which is not satisfied by $\tau$, derive
$D_{{{|}}\tau}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}$ by RAT
on  $x$ . This is possible, as $x$ does not appear anywhere yet.

_Step 2._ Derive $C\lor x$ by RAT on $x$. The only clauses in which  $x$
appears are those of the form $D_{{{|}}\tau}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}$ introduced in step 1, and from Lemma 4 and the
assumption that $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ we have
that $\Gamma\vdash_{1}D_{{{|}}\tau}\lor C$.

_Step 3._ For each $E\in\Gamma$ satisfied by $\tau$, derive $E\lor x$ by a
$\vdash_{1}$ step and delete $E$.

_Step 4._ For each literal $p$ in $\tau$, derive $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor p$ by RAT on $p$. To see that this
satisfies the RAT condition, consider any clause
$G=G^{\prime}\,\dot{\lor}\,\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p$}}$ with which $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}\lor p$ could be resolved. If $\tau\vDash G$, then by
steps 2 and 3 above, $G$ must also contain $x$, so the resolvent
$G^{\prime}\cup\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}$ is a
tautology. If $\tau\not\vDash G$, then $G$ must be one of the clauses
$D\in\Gamma$ or $D_{{{|}}\tau}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}$ from step 1, which means that we have already derived
$G_{{{|}}\tau}\lor\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}$, which
subsumes the resolvent $G^{\prime}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}$.

_Step 5._ Consider each clause $E\lor x$ introduced in step 2 or 3. In either
case $\tau\vDash E$, so $E$ contains some literal $p$ in $\tau$. Therefore we
can derive $E$ by resolving $E\lor x$ with $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}\lor p$. Thus we derive $C$ and all clauses from $\Gamma$
deleted in step 3.

Finally delete all the new clauses except for $C$.

Let $\Gamma$ be a set of clauses and $x$ any variable. Then $\Gamma^{(x)}$
consists of every clause in $\Gamma$ which does not mention $x$, together with
every clause of the form $E\lor F$ where both $x\,\dot{\lor}\,E$ and
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\,\dot{\lor}\,F$ are in
$\Gamma$.

In other words, $\Gamma^{(x)}$ is formed from $\Gamma$ by doing all possible
resolutions with respect to $x$ and then deleting all clauses containing
either $x$ or  $x$ . (This is exactly like the first step of the Davis-Putnam
procedure. In [Kul99b] the notation $\mathrm{DP}_{x}$ is used instead of
$\Gamma^{(x)}$.)

######  Lemma 17.

There is a polynomial size DRAT derivation of $\Gamma$ from $\Gamma^{(x)}$,
using only variables from $\Gamma$.

######  Proof 3.2.

We first derive every clause of the form $E\,\dot{\lor}\,x$ in $\Gamma$, by
RAT on $x$. As  $x$ has not appeared yet, the RAT condition is satisfied. Then
we derive each clause of the form $F\,\dot{\lor}\,\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}$ in $\Gamma$, by RAT on  $x$ . The only
possible resolutions are with clauses of the form $E\,\dot{\lor}\,x$ which we
have just introduced, but in this case either $E\cup F$ is tautological or
$E\lor F$ is in $\Gamma^{(x)}$ so $\Gamma^{(x)}\vdash_{1}\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor F\lor E$. Finally we delete all
clauses not in $\Gamma$.

The next two lemmas show that, under suitable conditions, if we can derive $C$
from $\Gamma$ in ${{\hbox{\rm DPR}}^{-}}$, then we can derive it from
$\Gamma^{(x)}$. We will use a kind of normal form for PR inferences. Say that
a clause $C$ is ${\hbox{\rm PR}}_{0}$ with respect to $\Gamma$ if there is a
partial assignment $\tau$ such that $\tau\vDash C$, all variables in $C$ are
in ${\hbox{{dom}}}(\tau)$, and

$C\lor\Gamma_{{{|}}\tau}\subseteq\Gamma.$ (2)

(Recall that the notation $C\lor\Gamma_{{{|}}\tau}$ means the set of clauses
$C\lor D$ for $D\in\Gamma_{{{|}}\tau}$.) The ${\hbox{\rm PR}}_{0}$ inference
rule lets us derive $\Gamma\cup\\{C\\}$ from $\Gamma$ when (2) holds. Letting
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$ it is easy to see
that (2) implies $\Gamma_{{{|}}\tau}\subseteq\Gamma_{{{|}}\alpha}$, so in
particular $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$, and hence this
is a special case of the PR rule.

######  Lemma 18.

Any PR inference can be replaced with a ${\hbox{\rm PR}}_{0}$ inference
together with polynomially many $\vdash_{1}$ and deletion steps, using no new
variables.

######  Proof 3.3.

Suppose $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$, where
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$ and $\tau\vDash
C$. By Lemma 9 we may assume that
${\hbox{{dom}}}(\alpha)\subseteq{\hbox{{dom}}}(\tau)$ so
${\hbox{{dom}}}(\tau)$ contains all variables in $C$. Let
$\Delta=C\lor\Gamma_{{{|}}\tau}$ and $\Gamma^{*}=\Gamma\cup\Delta$. Note that
$\Delta_{{{|}}\tau}$ is empty, as $\tau$ satisfies $C$. This implies that
$C\lor\Gamma^{*}_{{{|}}\tau}=C\lor\Gamma_{{{|}}\tau}\subseteq\Gamma^{*}$, so
$C$ is ${\hbox{\rm PR}}_{0}$ with respect to $\Gamma^{*}$. Furthermore the
condition $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ and Lemma 4 imply
that every clause in $\Delta$ is derivable from $\Gamma$ by a $\vdash_{1}$
step. Thus we can derive $\Gamma^{*}$ from $\Gamma$ by $\vdash_{1}$ steps,
then introduce $C$ by the ${\hbox{\rm PR}}_{0}$ rule, and recover
$\Gamma\cup\\{C\\}$ by deleting everything else.

######  Lemma 19.

Suppose $C$ is ${\hbox{\rm PR}}_{0}$ with respect to $\Gamma$, witnessed by
$\tau$ with $x\notin{\hbox{{dom}}}(\tau)$. Then $C$ is ${\hbox{\rm PR}}_{0}$
with respect to $\Gamma^{(x)}$.

######  Proof 3.4.

The ${\hbox{\rm PR}}_{0}$ condition implies that the variable $x$ does not
occur in $C$. We are given that $C\lor\penalty
10000\Gamma_{{{|}}\tau}\subseteq\penalty 10000\Gamma$ and want to show that
$C\lor\Gamma^{(x)}_{{{|}}\tau}\subseteq\Gamma^{(x)}$. So let
$D\in\Gamma^{(x)}$ with $\tau\not\vDash D$. First suppose $D$ is in $\Gamma$
and $x$ does not occur in $D$. Then $C\lor D_{{{|}}\tau}\in\Gamma$ by
assumption, so $C\lor D_{{{|}}\tau}\in\Gamma^{(x)}$. Otherwise, $D=E\lor F$
where both $E\,\dot{\lor}\,x$ and $F\,\dot{\lor}\,\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}$ are in $\Gamma$. Then by assumption
both $C\lor E_{{{|}}\tau}\lor x$ and $C\lor F_{{{|}}\tau}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}$ are in $\Gamma$. Hence $C\lor
D_{{{|}}\tau}=C\lor E_{{{|}}\tau}\lor F_{{{|}}\tau}\in\Gamma^{(x)}$.

We can now prove Theorem 16, that ${{\hbox{\rm DRAT}}^{-}}$ simulates
${{\hbox{\rm DPR}}^{-}}$.

######  Proof 3.5 (Proof of Theorem 16).

We are given a ${{\hbox{\rm DPR}}^{-}}$ refutation of some set $\Delta$, using
only the variables in $\Delta$. By Lemma 18 we may assume without loss of
generality that the refutation uses only $\vdash_{1}$, deletion and
${\hbox{\rm PR}}_{0}$ steps. Consider a ${\hbox{\rm PR}}_{0}$ inference in
this refutation, which derives $\Gamma\cup\\{C\\}$ from a set of clauses
$\Gamma$, witnessed by a partial assignment $\tau$. We want to derive
$\Gamma\cup\\{C\\}$ from $\Gamma$ in DRAT using only variables in $\Delta$.

Suppose $\tau$ is a total assignment to all variables in $\Gamma$. The set
$\Gamma$ is necessarily unsatisfiable, as otherwise it could not occur as a
line in a refutation. Therefore $\Gamma_{{{|}}\tau}$ is simply $\bot$, so the
${\hbox{\rm PR}}_{0}$ condition tells us that $C\in\Gamma$ and we do not need
to do anything.

Otherwise, there is some variable $x$ which occurs in $\Gamma$ but is outside
the domain of $\tau$, and thus in particular does not occur in $C$. We first
use $\vdash_{1}$ and deletion steps to replace $\Gamma$ with $\Gamma^{(x)}$.
By Lemma 19, $C$ is ${\hbox{\rm PR}}_{0}$, and thus PR, with respect to
$\Gamma^{(x)}$. By Lemma 16 there is a short DRAT derivation of
$\Gamma^{(x)}\cup\\{C\\}$ from $\Gamma^{(x)}$, using one new variable which
does not occur in $\Gamma^{(x)}$ or $C$. We choose $x$ for this variable.
Finally, observing that here
$\Gamma^{(x)}\cup\\{C\\}={(\Gamma\cup\\{C\\})}^{(x)}$, we recover
$\Gamma\cup\\{C\\}$ using Lemma 17.

###  3.2. Towards a simulation of ${{\hbox{\rm PR}}^{-}}$ by ${{\hbox{\rm
SPR}}^{-}}$

Our next result shows how to replace a PR inference with SPR inferences,
without additional variables. It is not a polynomial simulation of
${{\hbox{\rm PR}}^{-}}$ by ${{\hbox{\rm SPR}}^{-}}$ however, as it depends
exponentially on the “discrepancy” as defined next. Recall that $C$ is PR with
respect to $\Gamma$ if $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$,
where $\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$ and $\tau$
is a partial assignment satisfying $C$. We will keep this notation throughout
this section. $C$ is SPR with respect to $\Gamma$ if additionally
${\hbox{{dom}}}(\tau)={\hbox{{dom}}}(\alpha)$.

The _discrepancy_ of a PR inference is
$|{\hbox{{dom}}}(\tau)\setminus{\hbox{{dom}}}(\alpha)|$. That is, it is the
number of variables which are assigned by $\tau$ but not by $\alpha$.

######  Theorem 20.

Suppose that $\Gamma$ has a PR refutation $\Pi$ of size $S$ in which every PR
inference has discrepancy bounded by $\delta$. Then $\Gamma$ has a SPR
refutation of size $O(2^{\delta}S)$ which does not use any variables not
present in $\Pi$.

When the discrepancy is logarithmically bounded, Theorem 20 gives polynomial
size SPR refutations automatically. We need a couple of lemmas before proving
the theorem.

######  Lemma 21.

Suppose $\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ and $\beta$ is a
partial assignment extending $\alpha$, such that
${\hbox{{dom}}}(\beta)\subseteq{\hbox{{dom}}}(\tau)$. Then
$\Gamma_{{{|}}\beta}\vdash_{1}\Gamma_{{{|}}\tau}$

######  Proof 3.6.

Suppose $E\in\Gamma_{{{|}}\tau}$. Then $E$ contains no variables from $\beta$,
so $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E$}}_{{{|}}\beta}=\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E$}}$, and by assumption there is a refutation
$\Gamma_{{{|}}\alpha},\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E$}}\vdash_{1}\bot$. Thus $\Gamma_{{{|}}\beta},\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$E$}}\vdash_{1}\bot$ by Fact 2.

######  Proof 3.7 (Proof of Theorem 20.).

Our main task is to show that a PR inference with discrepancy bounded by
$\delta$ can be simulated by multiple SPR inferences, while bounding the
increase in proof size in terms of $\delta$. Suppose $C$ is derivable from
$\Gamma$ by a PR inference. That is,
$\Gamma_{{{|}}\alpha}\vdash_{1}\Gamma_{{{|}}\tau}$ where $\alpha=\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$C$}}$ and $\tau\vDash C$, and by Lemma 9 we
may assume that ${\hbox{{dom}}}(\tau)\supseteq{\hbox{{dom}}}(\alpha)$. List
the variables in ${\hbox{{dom}}}(\tau)\setminus{\hbox{{dom}}}(\alpha)$ as
$p_{1},\ldots,p_{s}$, where $s\leq\delta$.

Enumerate as $D_{1},\dots,D_{2^{s}}$ all clauses containing exactly the
variables $p_{1},\ldots,p_{s}$ with some pattern of negations. Let
$\sigma_{i}=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C\lor D_{i}$}}$, so
that $\sigma_{i}\supseteq\alpha$ and
${\hbox{{dom}}}(\sigma_{i})={\hbox{{dom}}}(\tau)$. By Lemma 21,
$\Gamma_{{{|}}\sigma_{i}}\vdash_{1}\Gamma_{{{|}}\tau}$. Since $\tau\vDash
C\lor D_{j}$ for every $j$, in fact

$\Gamma_{{{|}}\sigma_{i}}\vdash_{1}{(\Gamma\cup\\{C\lor\penalty
10000D_{1},\dots,C\lor\penalty 10000D_{i-1}\\})}_{{{|}}\tau}.$

Thus we may introduce all clauses $C\lor D_{1},\dots,C\lor D_{2^{s}}$ one
after another by SPR inferences. We can then use $2^{s}-1$ resolution steps to
derive $C$.

The result is a set $\Gamma^{\prime}\supseteq\Gamma$ which contains $C$ plus
many extra clauses subsumed by $C$, which must be carried through the rest of
the refutation, as we do not have the deletion rule. But by Lemma 8(a) this is
not a problem, as the presence of these additional subsumed clauses does not
affect the validity of later PR inferences.

##  4\. Upper bounds for some hard tautologies

This section proves that ${{\hbox{\rm SPR}}^{-}}$ — without new variables —
can give polynomial size refutations for many of the usual “hard”
propositional principles. Heule, Kiesl and Biere [HKB19, HKB17] showed that
the tautologies based on the pigeonhole principle (PHP) have polynomial size
${{\hbox{\rm SPR}}^{-}}$ proofs, and Heule and Biere discuss polynomial size
${{\hbox{\rm PR}}^{-}}$ proofs of the Tseitin tautologies and the 2–1
pigeonhole principle in [HB18]. The ${{\hbox{\rm SPR}}^{-}}$ proof of the PHP
tautologies can be viewed as a version of the original extended resolution
proof of PHP given by Cook and Reckhow [CR79]; see also [Kul99b] for an
adaptation of the original proof to use BC inferences.

Here we describe polynomial size ${{\hbox{\rm SPR}}^{-}}$ proofs for several
well-known principles, namely the pigeonhole principle, the bit pigeonhole
principle, the parity principle, the clique-coloring principles, and the
Tseitin tautologies. We also show that orification, xorification, and typical
cases of lifting can be handled in ${{\hbox{\rm SPR}}^{-}}$.

The existence of such small proofs is surprising, since they use only clauses
in the original literals, and it is well-known that such clauses are limited
in what they can express. However, ${{\hbox{\rm SPR}}^{-}}$ proofs can exploit
the underlying symmetries of the principles to introduce new clauses, in
effect arguing that properties can be assumed to hold “without loss of
generality” (see [RS18]).

It is open whether extended resolution, or the Frege proof system, can be
simulated by ${{\hbox{\rm PR}}^{-}}$ or ${{\hbox{\rm DPR}}^{-}}$, or more
generally by ${{\hbox{\rm DSR}}^{-}}$. The examples below show that any
separation of these systems must involve a new technique.

Our proofs use the same basic idea as the sketch in Example 6. One
complication is that we are now working with SPR rather than SR inferences.
This requires us to make the individual inferences more complicated – for
example the assignments $\alpha$ in Example 6 set one pigeon, while those in
Section 4.1 below set two pigeons. Another is that we want to avoid using any
deletion steps. This means that, when showing that an SPR inference is valid,
we have to consider every clause introduced so far. For this reason we will do
all necessary SPR inferences at the start, in a careful order, before we do
any resolution steps. This is the purpose of Lemma 22.

A _$\Gamma$ -symmetry_ is an invertible substitution $\pi$ such that
$\Gamma_{{{|}}\pi}=\Gamma$.

We will use the observation that, if $\pi$ is a $\Gamma$-symmetry and
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$ is a partial
assignment, then by Lemma 1 we have

$\Gamma_{{{|}}\alpha}={(\Gamma_{{{|}}\pi})}_{{{|}}\alpha}=\Gamma_{{{|}}\alpha\circ\pi}.$

Hence, if $\alpha\circ\pi\vDash C$, we can infer $C$ from $\Gamma$ by an SR
inference with $\tau=\alpha\circ\pi$. If furthermore all literals in the
domain and image of $\pi$ are in ${\hbox{{dom}}}(\alpha)$, then
$\alpha\circ\pi$ behaves as a partial assignment and
${\hbox{{dom}}}(\alpha\circ\pi)={\hbox{{dom}}}(\alpha)$, so this becomes an
SPR inference.

We introduce one new piece of notation, writing  $\alpha$ for the clause
expressing that the partial assignment $\alpha$ does not hold (so
$C=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$\alpha$}}$ if and only if
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$). Two partial
assignments are called _disjoint_ if their domains are disjoint. The next
lemma describes sufficient conditions for introducing, successively, the
clauses  $\alpha_{i}$ for $i=0,1,2,\ldots$ using only SPR inferences.

######  Lemma 22.

Suppose $(\alpha_{0},\tau_{0}),\ldots,(\alpha_{m},\tau_{m})$ is a sequence of
pairs of partial assignments such that for each $i$,

  1. (1)

$\Gamma_{{{|}}\alpha_{i}}=\Gamma_{{{|}}\tau_{i}}$

  2. (2)

$\alpha_{i}$ and $\tau_{i}$ are contradictory and have the same domain

  3. (3)

for all $j<i$, the assignments $\alpha_{j}$ and $\tau_{i}$ are either disjoint
or contradictory.

Then we can derive $\Gamma\cup\\{\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$\alpha_{i}$}}:i=0,\dots,m\\}$ from $\Gamma$ by a sequence of
SPR inferences.

######  Proof 4.1.

We write $C_{i}$ for  $\alpha_{i}$ . By item 2, $\tau_{i}\vDash C_{i}$. Thus
it is enough to show that for each $i$,

${\big{(}\Gamma\cup\\{{C_{0}},\ldots,{C_{i-1}}\\}\big{)}}_{{{|}}\alpha_{i}}\supseteq{\big{(}\Gamma\cup\\{{C_{0}},\ldots,{C_{i-1}}\\}\big{)}}_{{{|}}\tau_{i}}.$

We have $\Gamma_{{{|}}\alpha_{i}}=\Gamma_{{{|}}\tau_{i}}$. For $j<i$, either
$\alpha_{j}$ and $\tau_{i}$ are disjoint and consequently
${(C_{j})}_{{{|}}\alpha_{i}}={(C_{j})}_{{{|}}\tau_{i}}=C_{j}$, or they are
contradictory and so $\tau_{i}\vDash C_{j}$ and $C_{j}$ vanishes from the
right hand side.

In the lemma, if we added to (2) the condition that $\alpha_{i}$ and
$\tau_{i}$ disagree on only a single variable, then by Theorem 1.4 we could
derive the clauses  $\alpha_{i}$ by RAT inferences rather than needing SPR
inferences. However in the applications below they typically differ on more
than one variable, so our proofs are in ${{\hbox{\rm SPR}}^{-}}$, not in
${{\hbox{\rm RAT}}^{-}}$.

###  4.1. Pigeonhole principle

Let $n\geq 1$ and $[n]$ denote $\\{0,\ldots,n{-}1\\}$. The pigeonhole
principle $\mathrm{PHP}_{n}$ consists of the clauses

$\displaystyle\bigvee_{j\in[n]}p_{i,j}$ for each fixed $i\in[n+1]$ (pigeon
axioms) $\displaystyle\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{i,j}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{i^{\prime},j}$}}$ for all $i<i^{\prime}\in[n+1]$ and
$j\in[n]$ $\displaystyle\hbox{(hole axioms)}.$

[[HKB19]] $\mathrm{PHP}_{n}$ has polynomial size ${{\hbox{\rm SPR}}^{-}}$
refutations.

######  Proof 4.2.

Our strategy is to first derive all unit clauses  $p_{j,0}$ for $j>0$, which
effectively takes pigeon $0$ and hole $0$ out of the picture and reduces
$\mathrm{PHP}_{n}$ to a renamed instance of $\mathrm{PHP}_{n-1}$. We repeat
this construction to reduce to a renamed instance of $\mathrm{PHP}_{n-2}$,
etc. At each step, we will need to use several clauses introduced by SPR
inferences. We use Lemma 22 to introduce all necessary clauses at one go at
the start of the construction.

Let $\alpha_{i,j,k}$ be the assignment setting $p_{i,k}=1$, $p_{j,i}=1$ and
all other variables $p_{\ell,k},p_{\ell,i}$ for holes $k$ and $i$ to $0$. Let
$\pi_{k,i}$ be the $\mathrm{PHP}_{n}$-symmetry which switches holes $k$ and
$i$, that is, maps $p_{\ell,i}\mapsto p_{\ell,k}$ and $p_{\ell,k}\mapsto
p_{\ell,i}$ for every pigeon $\ell$. Let $\tau_{i,j,k}$ be
$\alpha_{i,j,k}\circ\pi_{k,i}$, so in particular $\tau_{i,j,k}$ sets
$p_{i,i}=1$ and $p_{j,k}=1$. By the properties of symmetries, we have
${(\mathrm{PHP}_{n})}_{{{|}}\alpha_{i,j,k}}={(\mathrm{PHP}_{n})}_{{{|}}\tau_{i,j,k}}$.

For $i=0,\dots,n-2$ define

$A_{i}:=\\{(\alpha_{i,j,k},\tau_{i,j,k}):i<j<n+1,\ i<k<n\\}.$

Any $\tau_{i,j,k}$ appearing in $A_{i}$ contradicts every
$\alpha_{i,j^{\prime},k^{\prime}}$ appearing in $A_{i}$, since they disagree
about which pigeon maps to hole $i$. On the other hand, if $i^{\prime}<i$ and
$\alpha_{i^{\prime},j^{\prime},k^{\prime}}$ appears in $A_{i^{\prime}}$ and is
not disjoint from $\tau_{i,j,k}$, then they must share some hole. So either
$i=k^{\prime}$ or $k=k^{\prime}$, and in either case they disagree about hole
$k^{\prime}$.

Hence we can apply Lemma 22 to derive all clauses  $\alpha_{i,j,k}$ such that
$i<j<n+1$ and $i<k<n$. Note  $\alpha_{i,j,k}$ is the clause $\vbox{\hrule
height=0.5pt\kern
1.07639pt\hbox{$p_{i,k}$}}\lor\bigvee_{\ell\not=i}p_{\ell,k}\lor\vbox{\hrule
height=0.5pt\kern
1.07639pt\hbox{$p_{j,i}$}}\lor\bigvee_{\ell\not=j}p_{\ell,i}$, which we
resolve with hole axioms to get $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{i,k}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{j,i}$}}$.

Now we use induction on $i=0,\dots,n-1$ to derive all unit clauses  $p_{j,i}$
for all $j$ with $i<j<n+1$. Fix $j>i$. For each hole $k>i$ we have
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{i,k}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{j,i}$}}$ (or if $i=n-1$ there is no such
$k$). We have $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{i,i}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{j,i}$}}$ since it is a hole axiom, and for each $k<i$, we
have  $p_{i,k}$ from the inductive hypothesis. Resolving all these with the
axiom $\bigvee_{k}p_{i,k}$ gives  $p_{j,i}$ .

Finally the unit clauses  $p_{n,i}$ for $i<n$ together contradict the axiom
$\bigvee_{i}p_{n,i}$.

###  4.2. Bit pigeonhole principle

Let $n=2^{k}$. The _bit pigeonhole principle_ contradiction,
${\mathrm{BPHP}}_{n}$, asserts that each of $n+1$ pigeons can be assigned a
distinct $k$-bit binary string. For each pigeon $x$, with $0\leq x<n+1$, it
has variables $p^{x}_{1},\dots,p^{x}_{k}$ for the bits of the string assigned
to $x$. We think of strings $y\in{\\{0,1\\}}^{k}$ as holes. When convenient we
will identify holes with numbers $y<n$. We write $(x{\rightarrow}y)$ for the
conjunction $\bigwedge_{i}(p^{x}_{i}=y_{i})$ asserting that pigeon $x$ goes to
hole $y$, where $p^{x}_{i}=1$ is the literal $p^{x}_{i}$ and $p^{x}_{i}=0$ is
the literal  $p^{x}_{i}$ , and where $y_{i}$ is the $i$-th bit of $y$. We
write $(x{\nrightarrow}y)$ for its negation: $\bigvee_{i}(p^{x}_{i}\neq
y_{i})$. The axioms of ${\mathrm{BPHP}}_{n}$ are then

$(x{\nrightarrow}y)\lor(x^{\prime}{\nrightarrow}y)\quad\hbox{for all holes $y$
and all distinct pigeons~{}$x,x^{\prime}$.}$

Notice that the set $\\{(x{\nrightarrow}y):y<n\\}$ consists of the $2^{k}$
clauses containing the variables $p^{x}_{1},\dots,p^{x}_{k}$ with all patterns
of negations. We can derive $\bot$ from this set in $2^{k}{-}1$ resolution
steps.

######  Theorem 23.

The ${\mathrm{BPHP}}_{n}$ clauses have polynomial size ${{\hbox{\rm
SPR}}^{-}}$ refutations.

The theorem is proved below. It is essentially the same as the proof of PHP in
[HKB19] (or Theorem 4.1 above). For each $m<n-1$ and each pair $x,y>m$, we
define a clause

$C_{m,x,y}:=(m{\nrightarrow}y)\lor(x{\nrightarrow}m).$

Note we allow $x=y$. Let $\Gamma$ be the set of all such clauses $C_{m,x,y}$.
We will show these clauses can be introduced by SPR inferences, but first we
show they suffice to derive ${\mathrm{BPHP}}_{n}$.

######  Lemma 24.

${\mathrm{BPHP}}_{n}\cup\Gamma$ has a polynomial size resolution refutation.

######  Proof 4.3.

Using induction on $m=0,1,2,\ldots,n{-}1$ we derive all clauses
$(x{\nrightarrow}m)$ such that $x>m$. So suppose $m<n$ and $x>m$. For each
$y>m$, we have the clause $(m{\nrightarrow}y)\lor(x{\nrightarrow}m),$ as this
is $C_{m,x,y}$. We also have the clause
$(m{\nrightarrow}m)\lor(x{\nrightarrow}m),$ as this is an axiom of
${\mathrm{BPHP}}_{n}$. Finally, for each $m^{\prime}<m$, we have
$(m{\nrightarrow}m^{\prime})$ by the inductive hypothesis (or, in the base
case $m=0$, there are no such clauses). Resolving all these together gives
$(x{\nrightarrow}m)$.

At the end we have in particular derived all the clauses $(n{\nrightarrow}m)$
such that $m<n$. Resolving all these clauses together yields $\bot$.

Thus it is enough to show that we can introduce all clauses in $\Gamma$ using
SPR inferences. We use Lemma 22. For $m<n-1$ and each pair $x,y>m$, define
partial assignments

$\displaystyle\alpha_{m,x,y}$
$\displaystyle:=(m{\rightarrow}y)\wedge(x{\rightarrow}m)$
$\displaystyle\tau_{m,x,y}$
$\displaystyle:=(m{\rightarrow}m)\wedge(x{\rightarrow}y)$

so that $C_{m,x,y}=\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$\alpha_{m,x,y}$}}$ and $\tau_{m,x,y}=\alpha_{m,x,y}\circ\pi$
where $\pi$ swaps all variables for pigeons $m$ and $x$. Hence
${({\mathrm{BPHP}}_{n})}_{{{|}}\alpha_{m,x,y}}={({\mathrm{BPHP}}_{n})}_{{{|}}\tau_{m,x,y}}$
as required.

For the other conditions for Lemma 22, first observe that assignments
$\alpha_{m,x,y}$ and $\tau_{m,x^{\prime},y^{\prime}}$ are always inconsistent,
since they map $m$ to different places. Now suppose that $m<m^{\prime}$ and
$\alpha_{m,x,y}$ and $\tau_{m^{\prime},x^{\prime},y^{\prime}}$ are not
disjoint. Then they must have some pigeon in common, so either $m^{\prime}=x$
or $x^{\prime}=x$. In both cases $\tau_{m^{\prime},x^{\prime},y^{\prime}}$
contradicts $(x{\rightarrow}m)$, in the first case because it maps $x$ to
$m^{\prime}$, and in the second because it maps $x$ to $y^{\prime}$ with
$y^{\prime}>m^{\prime}$.

###  4.3. Parity principle

The _parity principle_ states that there is no (undirected) graph on an odd
number of vertices in which each vertex has degree exactly one (see [Ajt90,
BIK+96]). For $n$ odd, let ${\mathrm{PAR}}_{n}$ be a set of clauses expressing
(a violation of) the parity principle on $n$ vertices, with variables
$x_{i,j}$ for the $\binom{n}{2}$ many values $0\leq i<j<n$, where we identify
the variable $x_{i,j}$ with $x_{j,i}$. We write $[n]$ for
$\\{0,\ldots,n{-}1\\}$. ${\mathrm{PAR}}_{n}$ consists of the clauses

$\displaystyle\bigvee_{j\not=i}x_{i,j}$ for each fixed $i\in[n]$ (“pigeon”
axioms) $\displaystyle\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i,j}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i,j^{\prime}}$}}$ for all distinct $i,j,j^{\prime}\in[n]$
$\displaystyle\hbox{(``hole'' axioms)}.$

######  Theorem 25.

The ${\mathrm{PAR}}_{n}$ clauses have polynomial size ${{\hbox{\rm SPR}}^{-}}$
refutations.

######  Proof 4.4.

Let $n=2m+1$. For $i<m$ and distinct $j,k$ with $2i+1<j,k<n$ define
$\alpha_{i,j,k}$ to be the partial assignment which matches $2i$ to $j$ and
$2i+1$ to $k$, and sets all other adjacent variables to $0$. That is,
$x_{2i,j}=1$ and $x_{2i,j^{\prime}}=0$ for all $j^{\prime}\neq j$, and
$x_{2i+1,k}=1$ and $x_{2i+1,k^{\prime}}=0$ for all $k^{\prime}\neq k$.
Similarly define $\tau_{i,j,k}$ to be the partial assignment which matches
$2i$ to $2i+1$ and $j$ to $k$, and sets all other adjacent variables to $0$,
so that $\tau_{i,j,k}=\alpha_{i,j,k}\circ\pi$ where $\pi$ swaps vertices
$2i+1$ and $j$. It is easy to see that the conditions of Lemma 22 are
satisfied. Therefore, we can introduce all clauses  $\alpha_{i,j,k}$ by SPR
inferences.

We now inductively derive the unit clauses $x_{2i,2i+1}$ for
$i=0,1,\dots,m-1$. Once we have these, refuting ${\mathrm{PAR}}_{n}$ becomes
trivial. So suppose we have $x_{2i^{\prime},2i^{\prime}+1}$ for all
$i^{\prime}<i$ and want to derive $x_{2i,2i+1}$. Consider any $r<2i$. First
suppose $r$ is even, so $r=2m$ for some $m<i$. We resolve the “hole” axiom
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x_{2m,2i}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x_{2m,2m+1}$}}$ with $x_{2m,2m+1}$ to get
$x_{2m,2i}$ , which is the same clause as  $x_{2i,r}$ . A similar argument
works for $r$ odd, and we can also obtain  $x_{2i+1,r}$ in a similar way.

Resolving the clauses  $x_{2i,r}$ and  $x_{2i+1,r}$ for $r<2i$ with the
“pigeon” axioms for vertices $2i$ and $2i+\penalty 100001$ gives clauses

$x_{2i,2i+1}\lor\bigvee_{r>2i+1}x_{2i,r}\quad\hbox{and}\quad
x_{2i,2i+1}\lor\bigvee_{r>2i+1}x_{2i+1,r}.$

Now by resolving clauses  $\alpha_{i,j,k}$ with suitable “hole” axioms we can
get $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{2i,j}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{2i+1,k}$}}$ for all distinct $j,k>2i+1$. Resolving these
with the clauses above gives $x_{2i,2i+1}$, as required.

###  4.4. Clique-coloring principle

The _clique-coloring principle_ ${\mathrm{CC}}_{n,m}$ states, informally, that
a graph with $n$ vertices cannot have both a clique of size $m$ and a coloring
of size $m-1$ (see [Kra97, Pud97]). For $m\leq n$ integers,
${\mathrm{CC}}_{n,m}$ uses variables $p_{a,i}$, $q_{i,c}$ and $x_{i,j}$ where
$a\in[m]$ and $c\in[m{-}1]$ and $i,j\in[n]$ with $i\not=j$. Again, $x_{i,j}$
is identified with $x_{j,i}$. The intuition is that $x_{i,j}$ indicates that
vertices $i$ and $j$ are joined by an edge, $p_{a,i}$ asserts that $i$ is the
$a$-th vertex of a clique, and $q_{i,c}$ indicates that vertex $i$ is assigned
color $c$. We list the clauses of ${\mathrm{CC}}_{n,m}$ as

  1. (1)

$\bigvee\nolimits_{i}p_{a,i}$ for each $a\in[m]$

  2. (2)

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,i}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{a^{\prime},i}$}}$ for distinct
$a,a^{\prime}\in[m]$ and each $i\in[n]$

  3. (3)

$\bigvee\nolimits_{c}q_{i,c}$ for each $i\in[n]$

  4. (4)

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$q_{i,c}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q_{i,c^{\prime}}$}}$ for each $i\in[n]$ and
distinct $c,c^{\prime}\in[m{-}1]$

  5. (5)

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,i}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{a^{\prime},j}$}}\lor x_{i,j}$ for each
distinct $a,a^{\prime}\in[m]$ and distinct $i,j\in[n]$

  6. (6)

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$q_{i,c}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q_{j,c}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i,j}$}}$ for each $c\in[m{-}1]$ and distinct $i,j\in[n]$.

######  Theorem 26.

The ${\mathrm{CC}}_{n,m}$ clauses have polynomial size ${{\hbox{\rm
SPR}}^{-}}$ refutations.

######  Proof 4.5.

The intuition for the ${{\hbox{\rm SPR}}^{-}}$ proof is that we introduce
clauses stating that the first $r$ clique members are assigned vertices that
are colored by the first $r$ colors; iteratively for $r=1,2,\ldots$.

Write $(a{\rightarrow}i{\rightarrow}c)$ for the assignment which sets

$\displaystyle p_{a,i}$ $\displaystyle=1\text{\quad and
\quad$p_{a^{\prime},i}=0$ for all $a^{\prime}\neq a$}$ $\displaystyle q_{i,c}$
$\displaystyle=1\text{\quad and \quad$q_{i,c^{\prime}}=0$ for all
$c^{\prime}\neq c$.}$

For all $r<m-2$, all indices $a>r$, all colors $c>r$ and all distinct vertices
$i,j\in[n]$, define

$\displaystyle\alpha^{r}_{a,i,j,c}$
$\displaystyle:=(a{\rightarrow}j{\rightarrow}r)\land(r{\rightarrow}i{\rightarrow}c)$
$\displaystyle\tau^{r}_{a,i,j,c}$
$\displaystyle:=(a{\rightarrow}j{\rightarrow}c)\land(r{\rightarrow}i{\rightarrow}r).$

Let $\Gamma$ consist of axioms (i), (ii) and (v), containing $p$ and $x$
variables but no $q$ variables, and let $\Delta$ consist of the remaining
axioms (iii), (iv) and (vi), containing $q$ and $x$ variables but no $p$
variables. Let us write $\alpha$ for $\alpha^{r}_{a,i,j,c}$ and $\tau$ for
$\tau^{r}_{a,i,j,c}$. Then $\Gamma_{{{|}}\alpha}=\Gamma_{{{|}}\tau}$ since
$\alpha$ and $\tau$ are the same on $p$ variables. Let $\alpha^{\prime}$ and
$\tau^{\prime}$ be respectively $\alpha$ and $\tau$ restricted to $q$
variables. Then $\Delta_{{{|}}\alpha^{\prime}}=\Delta_{{{|}}\tau^{\prime}}$
since $\tau^{\prime}=\alpha^{\prime}\circ\pi$ where $\pi$ is the
$\Delta$-symmetry which swaps vertices $i$ and $j$. Hence also
$\Delta_{{{|}}\alpha}=\Delta_{{{|}}\tau}$.

We will show that the conditions of Lemma 22 are satisfied, so we can
introduce all clauses  $\alpha^{r}_{a,i,j,c}$ by SPR inferences. The first
condition was just discussed. For the second condition, first notice that
$\alpha^{r}_{a,i,j,c}$ and $\tau^{r}_{a,i,j,c}$ set the same variables.

Now suppose $r,a,c,i,j$ are such that $r<a<m$, that $r<c<m{-}1$, and that
$i,j\in[n]$ are distinct. Suppose
$r^{\prime},a^{\prime},c^{\prime},i^{\prime},j^{\prime}$ satisfy the same
conditions, with $r^{\prime}\leq r$. We want to show that if
$\tau:=\tau^{r}_{a,i,j,c}$ and
$\alpha:=\alpha^{r^{\prime}}_{a^{\prime},i^{\prime},j^{\prime},c^{\prime}}$
are not disjoint, then they are contradictory. Notice that showing this will
necessarily use the literals  $p_{a^{\prime},i}$ and  $q_{i,c^{\prime}}$ in
the definition of our assignments, and that it will be enough to show that
$\alpha$ and $\tau$ disagree about either which index or which color is
assigned to a vertex $i$. First suppose $r^{\prime}=r$. Assuming $\alpha$ and
$\tau$ are not disjoint, we must be in one of the following four cases.

  1. (1)

$i^{\prime}=i$. Then $\alpha$ maps vertex $i$ to color $c^{\prime}>r$ while
$\tau$ maps $i$ to color $r$.

  2. (2)

$i^{\prime}=j$. Then $\alpha$ maps index $r<a$ to vertex $j$ while $\tau$ maps
index $a$ to $j$.

  3. (3)

$j^{\prime}=i$. Then $\alpha$ maps index $a^{\prime}>r$ to vertex $i$ while
$\tau$ maps index $r$ to $i$.

  4. (4)

$j^{\prime}=j$. Then $\alpha$ maps vertex $j$ to color $r<c$ while $\tau$ maps
$j$ to color $c$.

Now suppose $r^{\prime}<r$. Assuming $\alpha$ and $\tau$ are not disjoint, we
have the same cases.

  1. (1)

$i^{\prime}=i$. Then $\alpha$ maps index $r^{\prime}<r$ to vertex $i$ while
$\tau$ maps index $r$ to $i$.

  2. (2)

$i^{\prime}=j$. Then $\alpha$ maps index $r^{\prime}<a$ to vertex $j$ while
$\tau$ maps index $a$ to $j$.

  3. (3)

$j^{\prime}=i$. Then $\alpha$ maps vertex $i$ to color $r^{\prime}<r$ while
$\tau$ maps $i$ to color $r$.

  4. (4)

$j^{\prime}=j$. Then $\alpha$ maps vertex $j$ to color $r^{\prime}<c$ while
$\tau$ maps $j$ to color $c$.

Thus the conditions are met and we can introduce the clauses
$\alpha^{r}_{a,i,j,c}$ , that is,

$\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{a,j}$}}\vee\bigvee_{a^{\prime}\neq
a}p_{a^{\prime},j}\vee\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{j,r}$}}\vee\bigvee_{r^{\prime}\neq
r}q_{j,r^{\prime}}\vee\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{r,i}$}}\vee\bigvee_{r^{\prime}\neq
r}p_{r^{\prime},i}\vee\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{i,c}$}}\vee\bigvee_{c^{\prime}\neq c}q_{i,c^{\prime}},$

for all $r<a<m$, all $r<c<m{-}1$ and all distinct $i,j\in[n]$. Now let
$C^{r}_{a,i,j,c}$ be the clause

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q_{j,r}$}}\ \lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{r,i}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{i,c}$}}.$

We derive this by resolving  $\alpha^{r}_{a,i,j,c}$ with instances of axiom
(ii) to remove the literals $p_{a^{\prime},j}$ and $p_{r^{\prime},i}$ and then
with instances of axiom (iv) to remove the literals $q_{j,r^{\prime}}$ and
$q_{i,c^{\prime}}$. We now want to derive, for each $r$, each $a$ with $r<a<m$
and each $j\in[n]$, the clause

$\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{a,j}$}}\lor\bigvee_{c>r}q_{j,c}$ (3)

which can be read as “if $a>r$ goes to $j$, then $j$ goes to some $c>r$”.
Intuitively, this removes indices and colors $0,\dots,r$ from
${\mathrm{CC}}_{n,m}$, thus reducing it to a CNF isomorphic to
${\mathrm{CC}}_{n,m-r-1}$.

Suppose inductively that we have already derived (3) for all $r^{\prime}<r$.
In particular we have derived $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{a,j}$}}\lor\bigvee_{c>r-1}q_{j,c}$, or for $r=0$ we use the
axiom $\bigvee_{c}q_{j,c}$. We resolve this with the clauses $C^{r}_{a,i,j,c}$
for all $c>r$ to get

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q_{j,r}$}}\ \lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{r,i}$}}\lor{q_{i,r}}.$ (4)

By resolving together suitable instances of axioms (v) and (vi) we obtain

$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{r,i}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{j,r}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{i,r}$}}$

and resolving this with (4) removes the variable $q_{i,r}$ to give
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$q_{j,r}$}}\ \lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{r,i}$}}$. We derive this for every $i$,
and then resolve with the axiom $\bigvee_{i}p_{r,i}$ to get $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$q_{j,r}$}}$, and finally again with our inductively given
clause $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$p_{a,j}$}}\lor\bigvee_{c>r-1}q_{j,c}$ to get $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p_{a,j}$}}\lor\bigvee_{c>r}q_{j,c}$ as
required.

###  4.5. Tseitin tautologies

The _Tseitin tautologies_ ${\mathrm{TS}}_{G,\gamma}$ are well-studied hard
examples for many proof systems (see [Tse68, Urq87]). Let $G$ be an undirected
graph with $n$ vertices, with each vertex $i$ labelled with a charge
$\gamma(i)\in\\{0,1\\}$ such that the total charge on $G$ is odd. For each
edge $e$ of $G$ there is a variable $x_{e}$. Then ${\mathrm{TS}}_{G,\gamma}$
consists of clauses expressing that, for each vertex $i$, the parity of the
values $x_{e}$ over the edges $e$ touching $i$ is equal to the charge
$\gamma(i)$. For a vertex $i$ of degree $d$, this requires $2^{d-1}$ clauses,
using one clause to rule out each assignment to the edges touching $i$ with
the wrong parity. If $G$ has constant degree then this has size polynomial in
$n$, but in general the size may be exponential in $n$. It is well-known to be
unsatisfiable.

The next lemma is a basic property of Tseitin contradictions. Note that it
does not depend on $\gamma$. By cycle we mean a simple cycle, with no repeated
vertices.

######  Lemma 27.

Let $K$ be any cycle in $G$. Then the substitution $\pi_{K}$ which flips the
sign of every literal on $K$ is a ${\mathrm{TS}}_{G,\gamma}$-symmetry.

######  Lemma 28.

If every node in $G$ has degree at least $3$, then $G$ contains a cycle of
length at most $2\log n$.

######  Proof 4.6.

Pick any vertex $i$ and let $H$ be the subgraph consisting of all vertices
reachable from $i$ in at most $\log n$ steps. Then $H$ cannot be a tree, as
otherwise by the assumption on degree it would contain more than $n$ vertices.
Hence it must contain some vertex reachable from $i$ in two different ways.

######  Theorem 29.

The ${\mathrm{TS}}_{G,\gamma}$ clauses have polynomial size ${{\hbox{\rm
SPR}}^{-}}$ refutations.

######  Proof 4.7.

We will construct a sequence of triples
$(G_{0},\gamma_{0},\ell_{0}),\dots,(G_{m},\gamma_{m},\ell_{m})$ where
$(G_{0},\gamma_{0})$ is $(G,\gamma)$, each $G_{i+1}$ is a subgraph of $G_{i}$
formed by deleting one edge and removing any isolated vertices, $\gamma_{i}$
is an odd assignment of charges to $G_{i}$, and $\ell_{i}$ is a literal
corresponding to an edge in $G_{i}\setminus G_{i+1}$. Let

$\Gamma_{i}={\mathrm{TS}}_{G_{0},\gamma_{0}}\cup\\{\ell_{0}\\}\cup\dots\cup{\mathrm{TS}}_{G_{i},\gamma_{i}}\cup\\{\ell_{i}\\}.$

As we go we will construct an ${{\hbox{\rm SPR}}^{-}}$ derivation containing
sets of clauses $\Gamma^{\prime}_{i}$ extending and subsumed by $\Gamma_{i}$,
and we will eventually reach a stage $m$ where $\Gamma_{m}$ is trivially
refutable. The values of $\ell_{i}$, $G_{i+1}$ and $\gamma_{i+1}$ are defined
from $G_{i}$ and $\gamma_{i}$ according to the next three cases.

_Case 1:_ $G_{i}$ contains a vertex $j$ of degree 1. Let $\\{j,k\\}$ be the
edge touching $j$. If $k$ has degree 2 or more, we define
$(G_{i+1},\gamma_{i+1})$ by letting $G_{i+1}$ be $G_{i}$ with edge $\\{j,k\\}$
and vertex $j$ removed, and letting $\gamma_{i+1}$ be $\gamma_{i}$ restricted
to $G_{i+1}$ and with $\gamma_{i+1}(k)=\gamma_{i}(k)+\gamma_{i}(j)$. If $k$
has degree $1$ and the same charge as $j$, then we let $G_{i+1}$ be $G_{i}$
with both $j$ and $k$ removed (with unchanged charges). In both cases, every
clause in ${\mathrm{TS}}_{G_{i+1},\gamma_{i+1}}$ is derivable from
${\mathrm{TS}}_{G_{i},\gamma_{i}}$ by a $\vdash_{1}$ step, as the Tseitin
condition on $j$ in ${\mathrm{TS}}_{G_{i},\gamma_{i}}$ is a unit clause; we
set $\ell_{i}$ to be the literal contained in this clause. If $k$ has degree
$1$ and opposite charge from $j$, then we can already derive a contradiction
from ${\mathrm{TS}}_{G_{i},\gamma_{i}}$ by one $\vdash_{1}$ step.

_Case 2:_ $G_{i}$ contains no vertices of degree 1 or 2. Apply Lemma 28 to
find a cycle $K$ in $G_{i}$ of length at most $2\log n$ and let $e$ be the
first edge in $K$. Our goal is to derive the unit clause $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}_{e}$ and remove $e$ from $G_{i}$.

Let $\alpha$ be any assignment to the variables on $K$ which sets $x_{e}$ to
1, and let $\tau$ be the opposite assignment. Using Lemma 27 applied
simultaneously to all graphs $G_{0},\dots,G_{i}$ we have
${(\Gamma_{i})}_{{{|}}\alpha}={(\Gamma_{i})}_{{{|}}\tau}$, as the unit clauses
$\ell_{i}$ are unaffected by these restrictions. Hence by Lemma 22,
${{\hbox{\rm SPR}}^{-}}$ inferences can be used to introduce all clauses
$\alpha$ , of which there are at most $2^{2\log n-1}$. We resolve them all
together to get the unit clause $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{e}$. This subsumes all other clauses introduced so far
in this step; we set $\ell_{i}$ to be  $x_{e}$ , and by Lemma 8(a), we may
ignore these subsumed clauses in future inferences. (Therefore we avoid
needing the deletion rule.) We define $(G_{i+1},\gamma_{i+1})$ by deleting
edge $e$ from $G_{i}$ and leaving $\gamma_{i}$ unchanged. All clauses in
${\mathrm{TS}}_{G_{i+1},\gamma_{i+1}}$ can now be derived from
${\mathrm{TS}}_{G_{i},\gamma_{i}}$ and $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{e}$ by single $\vdash_{1}$ steps.

_Case 3:_ $G_{i}$ contains no vertices of degree 1, but may contain vertices
of degree 2. We will adapt the argument of case 2. Redefine a _path_ to be a
sequence of edges connected by degree-2 vertices. By temporarily replacing
paths in $G_{i}$ with edges, we can apply Lemma 28 to find a cycle $K$ in
$G_{i}$ consisting of edge-disjoint paths $p_{1},\dots,p_{m}$ where $m\leq
2\log n$. Let $x_{j}$ be the variable associated with the first edge in
$p_{j}$. For each $j$, there are precisely two assignments to the variables in
$p_{j}$ which do not immediately falsify some axiom of
${\mathrm{TS}}_{G_{i},\gamma_{i}}$. Let $\alpha$ be a partial assignment which
picks one of these two assignments for each $p_{j}$, and such that
$\alpha(x_{1})=1$. As in case 2, ${{\hbox{\rm SPR}}^{-}}$ inferences can be
used to introduce  $\alpha$ for each $\alpha$ of this form.

Let us look at the part of  $\alpha$ consisting of literals from path $p_{j}$.
This has the form $z^{j}_{1}\lor\dots\lor z^{j}_{r}$, where $z^{j}_{1}$ is
$x_{j}$ with positive or negative sign and for each $k$, by the choice of
$\alpha$, there are Tseitin axioms expressing that $z^{j}_{k}$ and
$z^{j}_{k+1}$ have the same value. Hence if we set $z^{j}_{1}=0$ we can set
all literals in this clause to $0$ by unit propagation. Applying the same
argument to all parts of $\alpha$ shows that we can derive
$z^{1}_{1}\lor\dots\lor z^{m}_{1}$ from  $\alpha$ and
${\mathrm{TS}}_{G_{i},\gamma_{i}}$ with a single $\vdash_{1}$ step. We
introduce all $2^{m-1}$ such clauses, one for each $\alpha$, all with
$z^{1}_{1}=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x_{1}$}}$. We
resolve them together to get the unit clause  $x_{1}$ , then proceed as in
case 2.

For the size bound, each case above requires us to derive at most
$n\\!\cdot\\!|{\mathrm{TS}}_{G,\gamma}|$ clauses, and the refutation can take
at most $n$ steps.

###  4.6. Or-ification and xor-ification

Orification and xorification have been widely used to make hard instances of
propositional tautologies, see [BSIW04, BS09, Urq11]. This and the next
section discuss how ${{\hbox{\rm SPR}}^{-}}$ inferences can be used to “undo”
the effects of orification, xorification, and lifting without using any new
variables. As a consequence, these techniques are not likely to be helpful in
establishing lower bounds for the size of ${{\hbox{\rm PR}}^{-}}$ refutations.

Typically, one “orifies” many variables at once; however, for the purposes of
this paper, we describe orification of a single variable. Let $\Gamma$ be a
set of clauses, and $x$ a variable. For the $m$-fold _orification_ of $x$, we
introduce new variables $x_{1},\ldots,x_{m}$, with the intent of replacing $x$
with $x_{1}\lor x_{2}\lor\cdots\lor x_{m}$. Specifically, each clause $x\lor
C$ in $\Gamma$ is replaced with $x_{1}\lor\cdots\lor x_{m}\lor C$, and each
clause $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor C$ is replaced
with the $m$-many clauses $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{j}$}}\lor C$. Let $\Gamma^{\lor}$ denote the results of
this orification of $x$. We claim that ${{\hbox{\rm SPR}}^{-}}$ inferences may
be used to derive $\Gamma$ (with $x$ renamed to $x_{1}$) from $\Gamma^{\lor}$,
undoing the orification, as follows. We first use ${{\hbox{\rm SPR}}^{-}}$
inferences to derive each clause $x_{1}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{j}$}}$ for $j>1$. This is done using Lemma 22, with
$\alpha_{j}$ setting $x_{1}$ to $0$ and $x_{j}$ to $1$, and $\tau_{j}$ setting
$x_{1}$ to $1$ and $x_{j}$ to $0$, so that $\tau_{j}$ is $\alpha_{j}$ with
$x_{1}$ and $x_{j}$ swapped. Thus any clause $x_{1}\lor\cdots\lor x_{m}\lor C$
in $\Gamma^{\lor}$ can be resolved with these to yield $x_{1}\lor C$, and for
clauses $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x_{1}$}}\lor C$ in
$\Gamma^{\lor}$ we do not need to change anything.

Xorification of $x$ is a similar construction, but now we introduce $m$ new
variables with the intent of letting $x$ be expressed by $x_{1}\oplus
x_{2}\oplus\cdots\oplus x_{m}$. Each clause $x\lor C$ in $\Gamma$
(respectively, $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\lor C$ in
$\Gamma$) is replaced by $2^{m-1}$ many clauses $x_{1}^{\sigma}\lor
x_{2}^{\sigma}\lor\cdots\lor x_{m}^{\sigma}\lor C$ where $\sigma$ is a partial
assignment setting an odd number (respectively, an even number) of the
variables $x_{j}$ to ${\mathrm{1}}$. To undo the xorification it is enough to
derive the unit clauses  $x_{j}$ for $j>1$. So for each $j>1$, we first use
Lemma 22 to introduce the clause $x_{1}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{j}$, using the same partial assignments as in the
previous paragraph, and the clause $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{1}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{j}$}}$, using assignments $\alpha_{j}$ setting $x_{1}$ and
$x_{j}$ both to $1$, and $\tau_{j}$ setting $x_{1}$ and $x_{j}$ both to $0$,
so that $\tau_{j}$ is $\alpha_{j}$ with the signs of both $x_{1}$ and $x_{j}$
flipped. Resolving these gives $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}_{j}$. This subsumes $x_{1}\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x$}}_{j}$ and $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$x_{1}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{j}$}}$, so by Lemma 8(a), we may ignore these two clauses
in later ${{\hbox{\rm SPR}}^{-}}$ steps, and can thus use the same argument to
derive the clauses $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}_{i}$
for $i\neq j$, since $\alpha_{i}$ and $\tau_{i}$ do not affect the clause
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}_{j}$.

###  4.7. Lifting

Lifting is a technique for leveraging lower bounds on decision trees to obtain
lower bounds in stronger computational models, see [RM99, BHP10, HN12].

The most common form of lifting is the “indexing gadget” where a single
variable $x$ is replaced by $\ell+2^{\ell}$ new variables
$y_{1},\ldots,y_{\ell}$ and $z_{0},\ldots,z_{2^{\ell}-1}$. The intent is that
the variables $y_{1},\ldots,y_{\ell}$ specify an integer $i\in[2^{\ell}]$, and
$z_{i}$ gives the value of $x$. As in Section 4.2, we write
$(\vec{y}{\rightarrow}i)$ for the conjunction $\bigwedge_{j}(y_{j}=i_{j})$
where $i_{j}$ is the $j$-th bit of $i$, and write $(\vec{y}{\nrightarrow}i)$
for its negation $\bigvee_{j}(y_{j}\neq\penalty 10000i_{j})$. Thus, $x$ is
equivalent to the CNF formula
$\bigwedge_{i\in[2^{\ell}]}\left((\vec{y}{\nrightarrow}i)\lor z_{i}\right)$,
and  $x$ is equivalent to the CNF formula
$\bigwedge_{i\in[2^{\ell}]}\left((\vec{y}{\nrightarrow}i)\lor\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$z_{i}$}}\right)$.

Let $\Gamma$ is a set of clauses with an ${{\hbox{\rm SPR}}^{-}}$ refutation.
The indexing gadget applied to $\Gamma$ on the variable $x$ does the following
to modify $\Gamma$ to produce set of lifted clauses $\Gamma^{\prime}$: Each
clause $x\,\dot{\lor}\,C$ containing $x$ is replaced by the $2^{\ell}$ clauses
$(\vec{y}{\nrightarrow}i)\lor z_{i}\lor C$ for $i\in[2^{\ell}]$, and each
clause $\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$x$}}\,\dot{\lor}\,C$
containing  $x$ is replaced by the $2^{\ell}$ clauses
$(\vec{y}{\nrightarrow}i)\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$z_{i}$}}\lor C$.

For all $i\not=0$ and all $a,b\in\\{0,1\\}$, let $\alpha_{i,a,b}$ and
$\tau_{i,a,b}$ be the partial assignments

$\displaystyle\alpha_{i,a,b}$
$\displaystyle:=\,(\vec{y}{\rightarrow}i)\wedge\,z_{0}=a\,\wedge\,z_{i}=b$
$\displaystyle\tau_{i,a,b}$
$\displaystyle:=\,(\vec{y}{\rightarrow}0)\wedge\,z_{0}=b\,\wedge\,z_{i}=a.$

Since $i\not=0$ always holds, it is immediate that conditions (2) and (3) of
Lemma 22 hold. For condition (1), observe that the set of clauses
$\\{(\vec{y}{\nrightarrow}j)\lor z_{j}\lor C:j\in[2^{\ell}]\\}$, restricted by
$(\vec{y}{\rightarrow}i)$, becomes the single clause $z_{i}\lor C$, and
restricted by $(\vec{y}{\rightarrow}0)$ becomes $z_{0}\lor C$. In this way
$\Gamma^{\prime}_{{{|}}\alpha_{i,a,b}}=\Gamma^{\prime}_{{{|}}\tau_{i,a,b}}$
and condition 1. also holds. Therefore by Lemma 22, ${{\hbox{\rm SPR}}^{-}}$
inferences can be used to derive all clauses  $\alpha_{i,a,b}$ , namely all
the clauses $(\vec{y}{\nrightarrow}i)\lor z_{0}\\!\neq\\!a\lor
z_{i}\\!\neq\\!b$. For each fixed $i\neq 0$ this is four clauses, which can be
resolved together to give the clause $(\vec{y}{\nrightarrow}i)$. Then from
these $2^{\ell}-1$ clauses we can obtain by resolution each unit clause
$y_{j}$ for $j=1,\ldots,\ell$. Finally, using unit propagation with these, we
derive the clauses $z_{0}\,\dot{\lor}\,C$ and $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$z_{0}$}}\,\dot{\lor}\,C$ for all original clauses
$x\,\dot{\lor}\,C$ and $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x$}}\,\dot{\lor}\,C$ in $\Gamma$. We have thus derived from
$\Gamma^{\prime}$, using ${{\hbox{\rm SPR}}^{-}}$ and resolution inferences, a
copy $\Gamma^{\prime\prime}$ of all the clauses in $\Gamma$, except with $x$
replaced with $z_{0}$. The other clauses in in $\Gamma^{\prime}$ or that were
inferred during the process of deriving $\Gamma^{\prime\prime}$ are subsumed
by either the unit clauses $y_{j}$ or the clauses in $\Gamma^{\prime\prime}$.
Thus applying part (b) and then part (a) of Lemma 8, they do not interfere
with future ${{\hbox{\rm SPR}}^{-}}$ inferences refuting
$\Gamma^{\prime\prime}$.

##  5\. Lower bounds

This section gives an exponential separation between ${{\hbox{\rm DRAT}}^{-}}$
and ${{\hbox{\rm RAT}}^{-}}$, by showing that the bit pigeonhole principle
${\mathrm{BPHP}}_{n}$ requires exponential size refutations in ${{\hbox{\rm
RAT}}^{-}}$. This lower bound still holds if we allow some deletions, as long
as no initial clause of ${\mathrm{BPHP}}_{n}$ is deleted. On the other hand,
with unrestricted deletions, it follows from Theorems 3.1, 16 and 23 in this
paper that it has polynomial size refutations in ${{\hbox{\rm DRAT}}^{-}}$ and
even in ${{\hbox{\rm DBC}}^{-}}$, as well as in ${{\hbox{\rm SPR}}^{-}}$.

Kullmann [Kul99b] has already proved related separations for generalized
extended resolution (GER), which lies somewhere between DBC and BC in
strength. That work shows separations between various subsystems of GER, and
in particular gives an exponential lower bound on proofs of $\mathrm{PHP}_{n}$
in the system GER with no new variables, by analyzing which clauses are
blocked with respect to $\mathrm{PHP}_{n}$.

We define the _pigeon-width_ of a clause or assignment to equal the number of
distinct pigeons that it mentions. Our size lower bound for
${\mathrm{BPHP}}_{n}$ uses a conventional strategy: we first show a width
lower bound (on pigeon-width), and then use a random restriction to show that
a proof of subexponential size can be made into one of small pigeon-width. We
do not aim for optimal constants.

We have to be careful about one technical point in the second step, which is
that ${{\hbox{\rm RAT}}^{-}}$ refutation size does not in general behave well
under restrictions, as discussed in Section 2.2. So, rather than using
restrictions as such to reduce width, we will define a partial random matching
$\rho$ of pigeons to holes and show that if ${\mathrm{BPHP}}_{n}$ has a
${{\hbox{\rm RAT}}^{-}}$ refutation of small size, then
${\mathrm{BPHP}}_{n}\cup\rho$ has one of small pigeon-width.

A useful tool in analyzing resolution derivations from a set of clauses
$\Gamma$ is the _Prover-Adversary game_ on $\Gamma$ (see e.g. [Pud00, AD08]).
In the game, the Adversary claims to know a satisfying assignment for
$\Gamma$, and the Prover tries to force her into a contradiction by querying
the values of variables; the Prover can also forget variable assignments to
save memory and simplify his strategy. A _position_ in the game is a partial
assignment $\alpha$ recording the contents of the Prover’s memory. To fully
specify the game we also need to specify the starting position.

As the next lemma shows, a strategy for the Prover in this game is essentially
the same thing as a resolution derivation. But it is more intuitive to
describe a strategy than a derivation, and the game also gives a natural way
to show width lower bounds.

######  Lemma 30.

Consider a restriction of the Prover-Adversary game on a set of clauses
$\Gamma$ starting from position  $C$ in which the Prover’s memory can hold
information about at most $m$ pigeons simultaneously. If the Prover has a
winning strategy in this game, then $C$ is derivable from $\Gamma$ in pigeon-
width $m$. If the Adversary has a winning strategy, then $C$ is not derivable
from $\Gamma$ in pigeon-width $m-1$.

######  Proof 5.1.

We can think of a winning strategy for the Prover as a tree in which the nodes
are labelled with a partial assignment (the position $\alpha$) and with the
Prover’s action in that situation, that is: query a variable, forget a
variable, or declare victory because $\alpha$ falsifies a clause from
$\Gamma$. We can make this into a resolution refutation by replacing each
label $\alpha$ with the clause negating it and interpreting the three actions
as respectively resolution, weakening, and deriving a clause from an axiom by
weakening.

For the other direction, it is enough to construct a winning strategy for the
Prover from a derivation of pigeon-width $m-1$. This is the reverse of the
process described above, except that we need to be careful with the resolution
rule. Suppose an instance of the rule is: from $p\vee D$ and $\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p$}}\vee E$ derive $D\vee E$, where each
clause mentions at most $m-1$ pigeons. In the Prover-strategy, this becomes:
from position $\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$D$}}\cup\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$E$}}$,
query $p$. If it is false, forget some variables from  $E$ to reach position
$\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$p$}}\cup\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$D$}}$. If it is true, forget some variables
from  $D$ to reach position $p\cup\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$E$}}$. Thus the Prover may be in a position mentioning $m$
pigeons immediately after $p$ is queried.

######  Lemma 31.

Let $\beta$ be a partial assignment corresponding to a partial matching of $m$
pigeons to holes. Then ${\mathrm{BPHP}}_{n}\cup\beta$ requires pigeon-width
$n{-}m$ to refute in resolution.

######  Proof 5.2.

${\mathrm{BPHP}}_{n}\cup\beta$ is essentially an unusual encoding of the
pigeonhole principle with $n+1-m$ pigeons and $n-m$ holes. Thus, if the Prover
is limited to remembering variables from at most $n-m$ pigeons, there is an
easy strategy for the Adversary in the game starting from the empty position.
Namely, she can always maintain a matching between the pigeons mentioned in
the Prover’s memory and the available holes. The result follows by Lemma 30.

######  Theorem 32.

Let $\rho$ be a partial matching of size at most $n/4$. Let $\Pi$ be a
${{\hbox{\rm DRAT}}^{-}}$ refutation of ${\mathrm{BPHP}}_{n}\cup\rho$ in which
no clause of ${\mathrm{BPHP}}_{n}$ is ever deleted. Then some clause in $\Pi$
has pigeon-width more than $n/3$.

######  Proof 5.3.

Suppose for a contradiction there is a such a refutation $\Pi$ in pigeon-width
$n/3$. We consider each RAT inference in $\Pi$ in turn, and show it can be
eliminated and replaced with standard resolution reasoning, without increasing
the pigeon-width.

Inductively suppose $\Gamma$ is a set of clauses derivable from
${\mathrm{BPHP}}_{n}\cup\rho$ in pigeon-width $n/3$, using only resolution and
weakening. Suppose a clause $C$ in $\Pi$ of the form
$p\,\dot{\lor}\,C^{\prime}$ is RAT with respect to $\Gamma$ and $p$. Let
$\alpha=\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}$, so $\alpha(p)=0$
and $\alpha$ mentions at most $n/3$ pigeons. We consider three cases.

_Case 1:_ the assignment $\alpha$ is inconsistent with $\rho$. This means that
$\rho$ satisfies a literal which appears in $C$, so $C$ can be derived from
$\rho$ by a single weakening step.

_Case 2:_ the assignment $\alpha\cup\rho$ can be extended to a partial
matching $\beta$ of the pigeons it mentions. We will show that this cannot
happen. Let $x$ be the pigeon associated with the literal $p$. Let
$y=\beta(x)$ and let $y^{\prime}$ be the hole $\beta$ would map $x$ to if the
bit $p$ were flipped to ${\mathrm{1}}$. If $y^{\prime}=\beta(x^{\prime})$ for
some pigeon $x^{\prime}$ in the domain of $\beta$, let $\beta^{\prime}=\beta$.
Otherwise let $\beta^{\prime}=\beta\cup\\{(x^{\prime},y^{\prime})\\}$ for some
pigeon $x^{\prime}$ outside the domain of $\beta$.

Let $H$ be the hole axiom
$(x{\nrightarrow}y^{\prime})\lor(x^{\prime}{\nrightarrow}y^{\prime})$ in
$\Gamma$. The clause $(x{\nrightarrow}y^{\prime})$ contains the literal  $p$ ,
since $(x{\rightarrow}y^{\prime})$ contains $p$. So $H=\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$p$}}\,\dot{\lor}\,H^{\prime}$ for some
clause $H^{\prime}$. By the RAT condition, either $C^{\prime}\cup H^{\prime}$
is a tautology or $\Gamma\vdash_{1}C\lor H^{\prime}$. Either way,
$\Gamma\cup\vbox{\hrule height=0.5pt\kern 1.07639pt\hbox{$C$}}\cup\vbox{\hrule
height=0.5pt\kern 1.07639pt\hbox{$H^{\prime}$}}\vdash_{1}\bot$. Since
$\beta^{\prime}\supseteq\alpha$, $\beta^{\prime}$ falsifies $C$. It also
falsifies $H^{\prime}$, since it satisfies
$(x{\rightarrow}y^{\prime})\wedge(x^{\prime}{\rightarrow}y^{\prime})$ except
at $p$. It follows that $\Gamma\cup\beta^{\prime}\vdash_{1}\bot$. By
assumption, $\Gamma$ is derivable from ${\mathrm{BPHP}}_{n}\cup\rho$ in
pigeon-width $n/3$, and $\beta^{\prime}$ extends $\rho$. Since unit
propagation does not increase pigeon-width, this implies that
${\mathrm{BPHP}}_{n}\cup\beta^{\prime}$ is refutable in resolution in pigeon-
width $n/3$, by first deriving $\Gamma$ and then using unit propagation. This
contradicts Lemma 31 as $\beta^{\prime}$ is a matching of at most $n/3+n/4+1$
pigeons.

_Case 3:_ the assignment $\alpha\cup\rho$ cannot be extended to a partial
matching of the pigeons it mentions. Consider the Prover-Adversary game on
${\mathrm{BPHP}}_{n}\cup\rho$ with starting position $\alpha$. The Prover can
ask all remaining bits of the pigeons mentioned in $\alpha$, and since there
is no suitable partial matching this forces the Adversary to reveal a
collision and lose the game. This strategy has pigeon-width $n/3$; it follows
that $C$ is derivable from ${\mathrm{BPHP}}_{n}\cup\rho$ in resolution in this
pigeon-width, as required.

######  Theorem 33.

Let $\Pi$ be a ${{\hbox{\rm DRAT}}^{-}}$ refutation of ${\mathrm{BPHP}}_{n}$
in which no clause of ${\mathrm{BPHP}}_{n}$ is ever deleted. Then $\Pi$ has
size at least $2^{n/60}$.

######  Proof 5.4.

Construct a random restriction $\rho$ by selecting each pigeon independently
with probability $1/5$ and then randomly matching the selected pigeons with
distinct holes (there is an ${(1/5)}^{n+1}$ chance that there is no matching,
because we selected all the pigeons — in this case we set all variables at
random).

Let $m=n/4$. Let $C$ be a clause mentioning at least $m$ distinct pigeons
$x_{1},\dots,x_{m}$ and choose literals $p_{1},\dots,p_{m}$ in $C$ such that
$p_{i}$ belongs to pigeon $x_{i}$. The probability that $p_{i}$ is satisfied
by $\rho$ is $1/10$. However, these events are not quite independent for
different $i$, as the holes used by other pigeons are blocked for pigeon
$x_{i}$. To deal with this, we may assume that pigeons $x_{1},\dots,x_{m}$, in
that order, were the first pigeons considered in the construction of $\rho$.
When we come to $x_{i}$, if we set it, then there are $n/2$ holes which would
satisfy $p_{i}$, at least $n/2-m\geq n/4$ of which are free; so of the free
holes, the fraction which satisfy $p_{i}$ is at least $1/3$. So the
probability that $\rho$ satisfies $p_{i}$, conditioned on it not satisfying
any of $p_{1},\dots,p_{i-1}$, is at least $1/15$. Therefore the probability
that $C$ is not satisfied by $\rho$ is at most
${(1-1/15)}^{m}<e^{-m/15}=e^{-n/60}$.

Now suppose $\Pi$ contains no more than $2^{n/60}$ clauses of pigeon width at
least $n/4$. By the union bound, for a random $\rho$, the probability that at
least one of these clauses is not satisfied by $\rho$ is at most
$2^{n/60}e^{-n/60}={(2/e)}^{n/60}$. Therefore most restrictions $\rho$ satisfy
all clauses in $\Pi$ of pigeon-width at least $n/4$, and by the Chernoff bound
we may choose such a $\rho$ which also sets no more than $n/4$ pigeons.

We now observe inductively that for each clause $C$ in $\Pi$, some subclause
of $C$ is derivable from ${\mathrm{BPHP}}_{n}\cup\rho$ in resolution in
pigeon-width $n/3$, ultimately contradicting Lemma 31. If $C$ has pigeon-width
more than $n/3$, this follows because $C$ is subsumed by $\rho$. Otherwise, if
$C$ is derived by a RAT inference, we repeat the proof of Theorem 32; in case
2 we additionally use the observation that if $\Gamma\vdash_{1}C\lor
H^{\prime}$ and $\Gamma^{\prime}$ subsumes $\Gamma$, then
$\Gamma^{\prime}\vdash_{1}C\lor H^{\prime}$.

######  Corollary 34.

${{\hbox{\rm RAT}}^{-}}$ does not simulate ${{\hbox{\rm DRAT}}^{-}}$.
${{\hbox{\rm RAT}}^{-}}$ does not simulate ${{\hbox{\rm SPR}}^{-}}$.

######  Proof 5.5.

By Theorem 23, ${\mathrm{BPHP}}_{n}$ has short proofs in ${{\hbox{\rm
SPR}}^{-}}$. Thus, by Theorem 16, this also holds for ${{\hbox{\rm
DRAT}}^{-}}$ (and for ${{\hbox{\rm DBC}}^{-}}$ by Theorem 3.1). On the other
hand, Theorem 33 just showed ${\mathrm{BPHP}}_{n}$ requires exponential size
${{\hbox{\rm RAT}}^{-}}$ proofs.

##  6\. Open problems

There are a number of open questions about the systems with no new variables.
Of particular importance is the question of the relative strengths of
${{\hbox{\rm DPR}}^{-}}$, ${{\hbox{\rm DSR}}^{-}}$ and related systems. The
results of [HB18, HKB17, HKB19] and the present paper show that ${{\hbox{\rm
DPR}}^{-}}$, and even the possibly weaker system ${{\hbox{\rm SPR}}^{-}}$, are
strong. ${{\hbox{\rm DPR}}^{-}}$ is a promising system for effective proof
search algorithms, but it is open whether practical proof search algorithms
can effectively exploit its strength. It is also open whether ${{\hbox{\rm
DPR}}^{-}}$ or ${{\hbox{\rm DSR}}^{-}}$ simulates ER.

Another important question is to understand the strength of deletion for these
systems. Of course, deletion is well-known to help the performance of SAT
solvers in practice, if for no other reason, because unit propagation is
faster when fewer clauses are present. In addition, for systems such as RAT,
it is known that deletion can allow new inferences. The results in Sections 4
and 5 improve upon this by showing that ${{\hbox{\rm RAT}}^{-}}$ does not
simulate ${{\hbox{\rm DRAT}}^{-}}$. This strengthens the case, at least in
theory, for the importance of deletion.

In Section 4 we described small ${{\hbox{\rm SPR}}^{-}}$ proofs of many of the
known “hard” tautologies that have been shown to require exponential size
proofs in constant depth Frege. It is open whether ${{\hbox{\rm SPR}}^{-}}$
simulates Frege; and by these results, any separation of ${{\hbox{\rm
SPR}}^{-}}$ and Frege systems will likely require developing new techniques.
Even more tantalizing, we can ask whether ${{\hbox{\rm SR}}^{-}}$ simulates
Frege.

There are several hard tautologies for which we do not whether there are as
polynomial size ${{\hbox{\rm SPR}}^{-}}$ proofs. Jakob Nordström [personal
communication, 2019] suggested (random) 3-XOR SAT and the even coloring
principle as examples. 3-XOR SAT has short cutting planes proofs via Gaussian
elimination; it is open whether ${{\hbox{\rm SPR}}^{-}}$ or ${{\hbox{\rm
DSPR}}^{-}}$ or even ${{\hbox{\rm DSR}}^{-}}$ has polynomial size refutations
for all unsatisfiable 3-XOR SAT principles. The even coloring principle is a
special case of the Tseitin principle [Mar06]: the graph has an odd number of
edges, each vertex has even degree, and the initial clauses assert that, for
each vertex, exactly one-half the incident edges are labeled 1. It is not hard
to see that the even coloring principle can be weakened to the Tseitin
principle by removing some clauses with the deletion rule. Hence there are
polynomial size ${{\hbox{\rm DSPR}}^{-}}$ refutations (with deletion) of the
even coloring principle. It is open whether ${{\hbox{\rm SPR}}^{-}}$ (without
deletion) has polynomial size refutations for the even coloring principle.

Paul Beame [personal communication, 2018] suggested that the graph PHP
principles (see [BSW01]) may separate systems such as ${{\hbox{\rm SPR}}^{-}}$
or even ${{\hbox{\rm SR}}^{-}}$ from Frege systems. However, there are reasons
to suspect that in fact the graph PHP principles also have short ${{\hbox{\rm
SPR}}^{-}}$ proofs. Namely, SPR inferences can infer a lot of clauses from the
graph PHP clauses. If an instance of graph PHP has every pigeon with outdegree
$\geq 2$, then there must be an alternating cycle of pigeons $i_{1},\ldots
i_{\ell+1}$ and holes $j_{1},\ldots j_{\ell}$ such that $i_{\ell}=i_{1}$, the
edges $(i_{s},j_{s})$ and $(i_{s+1},j_{s})$ are all in the graph, and
$\ell=O(\log n)$. Then an SPR inference can be used to learn the clause
$\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i_{1},j_{1}}$}}\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i_{2},j_{2}}$}}\lor\cdots\lor\vbox{\hrule height=0.5pt\kern
1.07639pt\hbox{$x_{i_{\ell},j_{\ell}}$}}$, by using the fact that a satisfying
assignment that falsifies this clause can be replaced by the assignment that
maps instead each pigeon $i_{s+1}$ to hole $j_{s}$.

This construction clearly means that SPR inferences can infer many clauses
from the graph PHP clauses. However, we do not know how to use these to form a
short ${{\hbox{\rm SPR}}^{-}}$ proof of the graph PHP principles. It remains
open whether a polynomial size ${{\hbox{\rm SPR}}^{-}}$ proof exists.

#### Acknowledgements

We thank the reviewers of the conference and journal versions of this paper
for suggestions and comments that improved the paper. We also thank Jakob
Nordström, Paul Beame, Marijn Heule, Thomas Kochmann and Oliver Kullmann for
useful comments, questions and suggestions.

## References

  * [AD08] A. Atserias and V. Dalmau.  A combinatorial characterization of resolution width.  Journal of Computer and System Sciences, 74(3):323–334, 2008.
  * [Ajt90] M. Ajtai.  Parity and the pigeonhole principle.  In Feasible Mathematics: A Mathematical Sciences Institute Workshop held in Ithaca, New York, June 1989, pages 1–24. Birkhäuser, 1990.
  * [BHP10] Paul Beame, Trinh Huynh, and Toniann Pitassi.  Hardness amplification in proof complexity.  In Proc. 42nd Annual ACM Symposium on Theory of Computing (STOC’10), pages 87–96, 2010.
  * [BIK+96] Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák.  Lower bounds on Hilbert’s Nullstellensatz and propositional proofs.  Proceedings of the London Mathematical Society, 73(3):1–26, 1996\.