Supercritical Tradeoff Between Size and Depth for Resolution over Parities

There are numerous results establishing exponential lower bounds for tree-like $\mathrm{Res}(\oplus )$ refutations of standard combinatorial formulas, using a variety of techniques [24, 25, 20, 22, 23, 26, 12].

Independently, Chattopadhyay, Mande, Sanyal, and Sherif [15] and Beame and Kroth [5] introduced a lifting approach for establishing lower bounds in tree-like $\mathrm{Res}(\oplus )$.

Given a CNF formula $\phi (y_1,y_2,\mathrm{\dots },y_n)$ and a Boolean function $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ (called a gadget), we define the lifted formula $\phi \circ g$ as the CNF encoding of the formula $\phi (g(x_{1,1},x_{1,2},\mathrm{\dots },x_{1,\mathrm{\ell }}),\mathrm{\dots },g(x_{n,1},x_{n,2},\mathrm{\dots },x_{n,\mathrm{\ell }}))$ where each variable $y_i$ in $\phi$ is replaced by $g(x_{i,1},\mathrm{\dots },x_{i,\mathrm{\ell }})$ for fresh variables $x_{i,1},x_{i,2},\mathrm{\dots },x_{i,\mathrm{\ell }}$.

Chattopadhyay, Mande, Sanyal, and Sherif [15] introduced the notion of $k$-stifling gadgets as follows. A Boolean function $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ is called a $k$-stifling gadget if, for every $a\in \{0,1\}$ and every choice of $\mathrm{\ell }-k$ input variables, there exists a setting of those $\mathrm{\ell }-k$ variables such that the output of $g$ is always equal to $a$, regardless of the values of the remaining $k$ variables. They further showed that if every resolution refutation of a formula $\phi$ has depth at least $h$, and $g$ is a $k$-stifling gadget, then any tree-like $\mathrm{Res}(\oplus )$ refutation of the lifted formula $\phi \circ g$ must have size at least $2^{kh}$.

Efremenko, Garlik, and Itsykson [17] made the first significant progress beyond the tree-like setting by establishing exponential lower bounds for bottom-regular $\mathrm{Res}(\oplus )$ refutations of the Binary Pigeonhole Principle formula ${\mathrm{BPHP}}_n^{n+1}$. Their work introduced the notions of closure and a random-walk technique, both of which have proven instrumental in subsequent research. Building on these ideas, and combining them with lifting techniques, Bhattacharya, Chattopadhyay, and Dvořák [10] showed that certain formulas require exponential-size refutations in bottom-regular $\mathrm{Res}(\oplus )$, while still admitting polynomial-size refutations in Resolution.

Alekseev and Itsykson [2] showed that one can construct formulas hard for bottom-regular $\mathrm{Res}(\oplus )$ based on any formula that requires large resolution depth. Specifically, they proved that if $\phi$ is an unsatisfiable CNF formula over $n$ variables with resolution depth at least $\mathrm{\Omega }(n)$, then any regular $\mathrm{Res}(\oplus )$ refutation of the lifted and transformed formula $\mathrm{mix}(\phi )\circ g$ must have size at least $2^{\mathrm{\Omega }(n)}$, where $g$ is a constant-size gadget and $\mathrm{mix}$ is a semantic-preserving transformation of $\phi$.

Moreover, Alekseev and Itsykson [2] made progress beyond bottom-regular $\mathrm{Res}(\oplus )$ by establishing a tradeoff between the size and depth of general $\mathrm{Res}(\oplus )$ refutations. Specifically, they constructed a family of formulas – lifted Tseitin formulas – over $n$ variables and of size $\mathrm{poly}(n)$ such that any $\mathrm{Res}(\oplus )$ refutation must have either size at least $2^{\mathrm{\Omega }(n/\log n)}$ or depth at least $\mathrm{\Omega }(n\log \log n)$. Subsequently, Efremenko and Itsykson [18] improved the depth lower bound to $\mathrm{\Omega }(n\log n)$. In particular, this result implies exponential lower bounds for regular $\mathrm{Res}(\oplus )$ for all reasonable notions of regularity. However, a limitation of this result is that it applies to a specific formula. In this paper, we address this issue by developing a general lifting result.

Independently and in parallel with our work, two recent papers appeared that further strengthen depth lower bounds, albeit at the expense of weakening the size bound in the tradeoff described above. Specifically, Bhattacharya and Chattopadhyay [9] proved that for every $\epsilon >0$, every $\mathrm{Res}(\oplus )$ refutation of lifted Tseitin formulas must either have size $2^{\mathrm{\Omega }(n^{\epsilon })}$ or depth $\mathrm{\Omega }(n^{2-\epsilon })$, where $n$ denotes the number of variables. Byramji and Impagliazzo [13] established that every Depth-$D$ $\mathrm{Res}(\oplus )$ refutation of the weak binary pigeonhole principle ${\mathrm{BPHP}}_n^m$ requires size $2^{\mathrm{\Omega }(n^3/D^2)}$. It is worth noting that the depth of any $\mathrm{Res}(\oplus )$ refutation of this formula is at least $\mathrm{\Omega }(n)$, so their bound is meaningful for $D$ ranging from $\mathrm{\Omega }(n)$ up to $o(n^{3/2})$.

It is important to note that, for the lifted Tseitin formulas and the binary pigeonhole principle used in the size-or-depth lower bound of [2, 18, 9] and [13], it remains unclear whether they actually admit short $\mathrm{Res}(\oplus )$ refutations. In other words, it is still unclear whether the observed phenomenon constitutes a genuine tradeoff or merely reflects the current limitations of our techniques for proving size lower bounds. In this paper, we address the following question: Does there exist a formula that admits a short $\mathrm{Res}(\oplus )$ refutation, yet any such refutation must have either superlinear (in the number of variables) depth or exponential (in the size of the formula) size?

A negative answer to this question – combined with the result from [2] – would yield exponential lower bounds on the size of $\mathrm{Res}(\oplus )$ refutations.

On the other hand, a positive answer would establish a supercritical tradeoff between size and depth in $\mathrm{Res}(\oplus )$. Here, supercritical means that for refutations of small size, the required depth significantly exceeds the worst-case upper bound achievable in the unrestricted setting. A positive answer would also lend support to a possible explanation for why proving $\mathrm{Res}(\oplus )$ lower bounds for seemingly simple formulas – such as the pigeonhole principle – remains so challenging. It may be that these formultas do admit short refutations, but all such refutations necessarily have large depth, making them difficult to construct.

A supercritical tradeoff between two proof complexity measures $\mu$ and $\nu$ for a formula $\phi$ occurs when $\phi$ has proofs with small $\mu$ and others with small $\nu$, but any proof with $\mu$ below a certain threshold forces $\nu$ to significantly exceed the worst-case upper bound known for all formulas.

In the last few years, many supercritical tradeoffs in proof complexity have been established [29, 4, 7, 6, 31, 30, 8, 19, 11, 16, 21, 14]. We briefly overview the most relevant results concerning Resolution and $\mathrm{Res}(\oplus )$. Razborov [29] established a supercritical tradeoff between width and size for tree-like Resolution. Fleming, Pitassi, and Robere [19] proved supercritical tradeoffs between size/width and depth for Resolution. More recently, Buss and Thapen [11] introduced a simple and highly flexible construction yielding a supercritical tradeoff between size/width and depth in Resolution. Finally, de Rezende et al. [16] and Göös et al. [21] showed that many of these tradeoffs can be made truly supercritical, meaning that the lower bounds are expressed in terms of the formula’s size, rather than merely the number of variables.

Chattopadhyay and Dvořák [14] established a supercritical tradeoff between width and size for tree-like $\mathrm{Res}(\oplus )$. Their proof builds on a corresponding lifting theorem, which directly lifts Razborov’s result for tree-like Resolution [29] to the $\mathrm{Res}(\oplus )$ setting.

Note that all the tradeoffs mentioned above have been established for proof systems for which superpolynomial size lower bounds are already known.

Our main result is the following theorem.

The size of the formula $\psi \circ {\oplus }_s\circ g$ is exponential in $s$, so in applications of Theorem 1 we choose $s$ to be as small as possible. On the other hand, to obtain non-trivial depth lower bounds, we need $w$ to be as large as possible. Two closely related width–depth tradeoff results for resolution are available in the literature, both addressing the regime in which the width is close to the total number of variables $n$: one due to Fleming, Pitassi, and Robere [19], and another due to Buss and Thapen [11]. The former applies for widths $w=n^{1-ϵ}$, while the latter applies for widths $w=\mathrm{\Omega }(n/\log n)$, which is significantly more suitable for our purposes. Applying the lifting from Theorem 1 to the width–depth tradeoff established by Buss and Thapen [11], we obtain a supercritical tradeoff between the size and depth of $\mathrm{Res}(\oplus )$ refutations.

To our knowledge, this is the first instance of a supercritical tradeoff demonstrated in a proof system lacking known superpolynomial lower bounds on proof size.

Another important specific case of Theorem 1 is a size-depth tradeoff for $\mathrm{Res}(\oplus )$ obtained by lifting from resolution width.

Consider several interesting specific cases of Theorem 4.

• $\mathrm{■}$

  Size-depth tradeoff for formula of size polynomial in number of variables. Let $w(n)=\mathrm{\Omega }(n)$. Then the formula ${\mathrm{\Psi }}_{n,\lceil \log n\rceil }$ contains $m:=\mathrm{\Theta }(n\log n)$ variables, ${\mathrm{\Psi }}_{n,\lceil \log n\rceil }$ is an $O(\log m)$-CNF formula of size $\mathrm{poly}(m)$ and any $\mathrm{Res}(\oplus )$ refutations of ${\mathrm{\Psi }}_{n,\lceil \log n\rceil }$ has either depth at least $\mathrm{\Omega }(m\log m)$ or size at least $2^{\mathrm{\Omega }(m/\log m)}$.

  This result extends the result from [18] for a large number of formulas.

• $\mathrm{■}$

  Maximal depth. Let $w(n)=\mathrm{\Omega }(n)$. Consider an arbitrary $1>\delta >0$. The formula ${\mathrm{\Psi }}_{n,\lceil n^{1-\delta }\rceil }$ contains $m:=\mathrm{\Theta }(n^{2-\delta })$ variables, ${\mathrm{\Psi }}_{n,\lceil n^{1-\delta }\rceil }$ is a CNF formula of size $poly(n)2^{n^{1-\delta }}$ and any $\mathrm{Res}(\oplus )$ refutations of ${\mathrm{\Psi }}_{n,\lceil n^{1-\delta }\rceil }$ has either depth at least $\mathrm{\Omega }(m^{3/2-\delta /2})$ or size at least $2^{\mathrm{\Omega }(n)}$.

  So if we do not restrict ourselves to formulas of polynomial size in the number of variables, then we can get a superpolynomial size lower bound for depth less than $m^{3/2-\delta }$.

• $\mathrm{■}$

  Minimal width. Let $w(n)=\mathrm{\Omega }\left(n^{1/2+\delta }\right)$, where $1/2>\delta >0$. The formula ${\mathrm{\Psi }}_{n,\lceil n^{1/2}\rceil }$ contains $m:=\mathrm{\Theta }(n^{3/2})$ variables, ${\mathrm{\Psi }}_{n,\lceil n^{1/2}\rceil }$ is a CNF formula of size $poly(n)2^{n^{1/2}}$ and any $\mathrm{Res}(\oplus )$ refutations of ${\mathrm{\Psi }}_{n,\lceil n^{1/2}\rceil }$ has either depth at least $\mathrm{\Omega }\left(n^{3/2+\delta }\right)=\mathrm{\Omega }\left(m^{1+2\delta /3}\right)$ or size at least $2^{\mathrm{\Omega }\left(n^{1/2+\delta }\right)}$.

  So we can get a non-trivial size-depth tradeoff starting from a formula with the resolution width $\mathrm{\Omega }\left(n^{1/2+\delta }\right)$.

Proof of Theorem 1 builds on the size-depth tradeoff established by Alekseev and Itsykson [2], with subsequent improvements by Efremenko and Itsykson [18].

As a first step, we develop a more flexible size-depth tradeoff that applies to a broad class of formulas. Below, we outline the main ideas behind the tradeoff established by Alekseev and Itsykson [2].

Consider a $\mathrm{Res}(\oplus )$ refutation $\mathrm{\Pi }$. We identify certain linear clauses within $\mathrm{\Pi }$ as good clauses. By definition, a good clause cannot be an axiom of the original formula. These clauses satisfy a crucial property we refer to as the dichotomy property. Specifically, for every good clause $C$ of moderately small width, one of the following holds:

• $\mathrm{■}$

  The size of the refutation $\mathrm{\Pi }$ is exponential;

• $\mathrm{■}$

  There exists another good linear clause in $\mathrm{\Pi }$ that appears at a significantly greater depth than $C$ and whose width exceeds that of $C$ by only a small amount.

Assuming that the empty clause is good and the size of $\mathrm{\Pi }$ is small, the dichotomy property implies that one can iteratively find increasingly deeper good clauses within $\mathrm{\Pi }$, ultimately yielding a lower bound on the depth.

The dichotomy property is established through a combination of a random walk argument and a bottleneck argument. We begin by defining a set $\mathrm{\Sigma }$ of good full assignments that falsify a given linear clause $C_0$ (for simplicity, one may think of $\mathrm{\Sigma }$ as the set of all assignments falsifying $C_0$). We then select a random assignment $\sigma \in \mathrm{\Sigma }$ and perform a $t$-step random walk along the refutation graph. At each step, we move from a linear clause to one of its premises that is also falsified by $\sigma$, counting only applications of resolution rules (applications of weakening are ignored).

The random walk theorem asserts that, with probability at least $p$, such a walk ends at a good linear clause. Now, if all good linear clauses reachable from $C_0$ within $t$ steps have width greater than $|C_0|+s$, then there must be at least $p\cdot 2^s$ such clauses. This is because a random assignment falsifying $C_0$ can falsify a clause of width at least $|C_0|+s$ with probability at most $2^{-s}$.

Alekseev and Itsykson [2] proved a random walk theorem for formulas of the form $\phi \circ g$, where $g$ is a 2-stifling gadget and $\phi$ is an unsatisfiable CNF formula that admits a sufficiently strong strategy for Delayer in a specific Prover–Delayer game. This game is defined with respect to the formula $\phi$ and a set $𝒜$ of its partial assignments, which must satisfy two conditions: (1) no assignment in $𝒜$ falsifies any clause of $\phi$, and (2) $𝒜$ is closed under restriction, i.e., any restriction of an assignment in $𝒜$ also belongs to $𝒜$.

The game proceeds as follows. It begins with some initial assignment ${\rho }_0\in 𝒜$. In each round, Prover selects a variable $x$ and queries its value. Delayer then has two options:

1. 1.

   Pay one black coin to choose a value $a\in \{0,1\}$ and extend the current assignment by setting $x:=a$; or

2. 2.

   Reply with $\ast$, allowing Prover to choose the value $a$.

Regardless of the outcome, Delayer earns one white coin for every move. The game terminates as soon as the current assignment no longer belongs to $𝒜$.

The required property of Delayer’s strategy is as follows: for every starting assignment ${\rho }_0\in 𝒜$ in the $(\phi ,𝒜)$-game, there exists a strategy for Delayer that guarantees earning at least $t-|{\rho }_0|$ white coins while spending at most $n$ black coins, where $t$ is significantly larger than $n$. Alekseev and Itsykson [2] provide an example of such a strategy for Tseitin formulas, in which $t$ is, roughly speaking, the number of edges and $n$ is the number of vertices in the underlying graph.

Our first observation is that Delayer strategies for such games can be derived from strategies in the Atserias–Dalmau games [3], which characterize resolution width, via a lifting transformation using a parity gate. This simple but powerful idea allows us to establish Theorem 4, thereby completing the first step of our approach.

However, formulas with large resolution width are inherently hard for resolution and can therefore only be used to show that small-depth $\mathrm{Res}(\oplus )$ refutations require large size. To establish a supercritical tradeoff, we also need to demonstrate the existence of short refutations with large depth. Our second step is to refine the lifting theorem so that it can be applied starting from formulas whose every resolution refutation must have either width at least $w$ or depth at least $h$. This refinement precisely enables us to apply lifting to the known supercritical tradeoffs between resolution width and depth.

In Section 4, we introduce an analogue of the Atserias–Dalmau games tailored to formulas that require resolution width at least $w$ for any resolution proof of depth at most $h$. The properties of winning positions in these games closely resemble those in the original Atserias–Dalmau games, provided we focus on positions within distance $h$ from the empty position. We then apply the parity gadget to these games. Notably, in the proof of the size-versus-depth tradeoff for suitable parameters, it suffices to consider Delayer’s strategy only on positions that remain close to the empty position. This insight enables us to establish the size-depth tradeoff starting from formulas that have no refutations of width at most $h$ and depth at most $w$ simultaneously, thereby proving Theorem 1.

Let $\phi$ be an unsatisfiable CNF formula. A resolution refutation of $\phi$ is a sequence of clauses $C_1,C_2,\mathrm{\dots },C_s$ such that $C_s$ is the empty clause (i.e., identically false) and for every $i\in [s]$ the clause $C_i$ is either a clause of $\phi$ or is obtained from previous clauses by the resolution rule that allows us to derive a clause $C\vee D$ from clauses $C\vee x$ and $D\vee \neg x$.

The size of a resolution refutation is the number of clauses in it. The depth of a resolution refutation is the length of the longest path between the empty clause and the clause of the original formula. The width of a resolution refutation is the maximal size of a clause from the refutation. The resolution width of an unsatisfiable CNF formula $\phi$ is the minimal possible width over all resolution refutations of $\phi$.

Here and after, all scalars are from the field ${𝔽}_2$. Let $X$ be a set of variables taking values in ${𝔽}_2$. A linear form in variables from $X$ is a homogeneous linear polynomial over ${𝔽}_2$ in variables from $X$ or, in other words, a polynomial ${\sum }_i^n{x}_i{a}_i$, where $x_i\in X$ is a variable and $a_i\in {𝔽}_2$ for all $i\in [n]$. A linear equation is an equality $f=a$, where $f$ is a linear form and $a\in {𝔽}_2$.

A linear clause is a disjunction of linear equations: ${\bigvee }_{i=1}^t(f_i=a_i)$. Note that over ${𝔽}_2$ a linear clause ${\bigvee }_{i=1}^t(f_i=a_i)$ may be represented as the negation of a linear system: $\neg {\bigwedge }_{i=1}^t(f_i=a_i+1)$.

Now we define the proof system resolution over parities ($\mathrm{Res}(\oplus )$) [25].

Let $\phi$ be an unsatisfiable CNF formula. A $\mathrm{Res}(\oplus )$ refutation of $\phi$ is a sequence of linear clauses $C_1$, $C_2$, …, $C_s$ such that $C_s$ is the empty clause (i.e., identically false) and for every $i\in [s]$ the clause $C_i$ is either a clause of $\phi$ or is obtained from previous clauses by one of the following inference rules:

• $\mathrm{■}$

  Resolution rule allows us to derive a linear clause $C\vee D$ from linear clauses $C\vee (f=a)$ and $D\vee (f=a+1)$.

• $\mathrm{■}$

  Weakening rule allows us to derive from a linear clause $C$ any linear clause $D$ in the variables of $\phi$ that semantically follows from $C$ (i.e., any assignment satisfying $C$ also satisfies $D$).

The size of a $\mathrm{Res}(\oplus )$ refutation is the number of linear clauses in it. The depth of a $\mathrm{Res}(\oplus )$ refutation is the maximal number of resolution rules applied on a path between a clause of the initial formula and the empty clause.

For any function $f(n)$, we denote by Depth-$f(n)$ $\mathrm{Res}(\oplus )$ the subsystem of $\mathrm{Res}(\oplus )$ consisting of refutations with depth at most $f(n)$, where $n$ is the number of variables in the formula being refuted.

For a linear clause $C$ we denote by $L(C)$ the set of linear forms that appear in $C$; i.e. $L\left({\bigvee }_{i=1}^t(f_i=a_i)\right)=\{f_1,f_2,\mathrm{\dots },f_t\}$. The same notation we use for linear systems: if $\mathrm{\Psi }$ is a ${𝔽}_2$-linear system, $L(\mathrm{\Psi })$ denotes the set of all linear forms from $\mathrm{\Psi }$.

For every CNF formula $\mathrm{\Phi }$ over the variables $Y=\{y_1,y_2,\mathrm{\dots },y_m\}$ and every Boolean function $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ we define a CNF formula $\mathrm{\Phi }\circ g$ with variables $X=\{x_{i,j}\mid i\in [m],j\in [\mathrm{\ell }]\}$ representing in CNF $\mathrm{\Phi }(g(x_{1,1},x_{1,2},\mathrm{\dots },x_{1,\mathrm{\ell }}),g(x_{2,1},x_{2,2},\mathrm{\dots },x_{2,\mathrm{\ell }}),\mathrm{\dots },g(x_{m,1},x_{m,2},\mathrm{\dots },x_{m,\mathrm{\ell }}))$ (i.e. we substitute to every variable of $\mathrm{\Phi }$ the function $g$ applied to $\mathrm{\ell }$ fresh variables). Let $\mathrm{\Phi }=\underset{i\in I}{\bigwedge }{C}_i$, where $C_i$ is a clause for all $i\in I$. For every $i\in [m]$ we denote by $y_i\circ g$ the canonical CNF formula representing $g(x_{i,1},x_{i,2},\mathrm{\dots },x_{i,\mathrm{\ell }})$ which has $\mathrm{\ell }$ variables in every clause and by $(\neg y_i)\circ g$ the canonical CNF formula representing $\neg g(x_{i,1},x_{i,2},\mathrm{\dots },x_{i,\mathrm{\ell }})$ which has $\mathrm{\ell }$ variables in every clause. Let $C_i=l_{i,1}\vee l_{i,2}\vee \mathrm{\cdots }\vee l_{i,n_i}$, where $l_i$ is a literal. Then we denote by $C_i\circ g$ a CNF formula that represents $l_{i,1}\circ g\vee l_{i,2}\circ g\vee \mathrm{\cdots }\vee l_{i,n_i}\circ g$ as follows: $C_i\circ g$ is the conjunction of all clauses of the form $D_1\vee D_2\vee \mathrm{\cdots }\vee D_{n_i}$, where $D_j$ is a clause of $l_{i,j}\circ g$ for all $j\in [m_i]$. And $\mathrm{\Phi }\circ g:=\underset{i\in I}{\bigwedge }{C}_i\circ g$.

We refer to $\mathrm{\Phi }\circ g$ as a formula $\mathrm{\Phi }$ lifted with a gadget $g$, to the set $Y=\{y_1,y_2,\mathrm{\dots },y_m\}$ as a set of unlifted variables, and to the set $X=\{x_{i,j}\mid i\in [m],j\in [\mathrm{\ell }]\}$ as the set of lifted variables.

For a set of vectors $U$ in a vector space, we denote by $⟨U⟩$ the linear span of $U$.

We consider the set of propositional variables $X=\{x_{i,j}\mid i\in [m],j\in [\mathrm{\ell }]\}$. The variables from $X$ are divided into $m$ blocks by the value of the first index. The variables $x_{i,1},x_{i,2},\mathrm{\dots },x_{i,\mathrm{\ell }}$ form the $i$-th block, for $i\in [m]$. We may view the set $X$ as the set of lifted variables with respect to a gadget of size $\mathrm{\ell }$.

Let $F=\{f_1,f_2,\mathrm{\dots },f_n\}$ be a set of ${𝔽}_2$-linear forms with variables from $X$. Consider a coefficient matrix $M$ of $F$: its columns correspond to $X$, and for all $i\in [n]$, $i$-th row is the coefficient vector of $f_i$. For every $i\in [m]$, let $M_i$ consist of matrix columns corresponding to the variables from the $i$-th block. Let $I\subseteq [m]$. We say that ${\{M_i\}}_{i\in I}$ is safe if there are distinct indices $i_1,i_2,\mathrm{\dots },i_t\in I$ and elements $v_{i_1}\in M_{i_1},v_{i_2}\in M_{i_2},\mathrm{\dots },v_{i_t}\in M_{i_t}$ such that $v_{i_1},v_{i_2},\mathrm{\dots },v_{i_t}$ is a basis of $⟨{\cup }_{i\in I}{M}_i⟩$.

A closure [17] of a set of linear forms $F$ is any inclusion-wise minimal set $S\subseteq [m]$ such that ${\{M_i\}}_{i\in [m]\setminus S}$ is safe. Informally, the closure indicates the set of the most essential unlifted variables for the set of linear forms $F$.

We denote the closure of $F$ by $\mathrm{Cl}(F)$.

We also require the notion of amortized closure, introduced by Efremenko and Itsykson [18]. Unlike the plain closure, which can grow dramatically with the addition of a single linear form, the amortized closure is a superset of the plain closure designed to grow more gradually and smoothly.

We say that a subset $A\subseteq [m]$ is coverable w.r.t. $\{M_i\mid i\in [m]\}$ if for every $i\in A$ there is $v_i\in M_i$ such the set $\{v_i\mid i\in A\}$ is linearly independent. For subsets $A,B\subseteq [m]$, we say that $A$ is less than $B$ ($A⪯B$) if the largest element in the symmetric difference $A\mathrm{△}B$ belongs to $B$.

An amortized closure of $F$ [18], denoted by $\widetilde{\mathrm{Cl}}(F)$, is the $⪯$-maximal subset of $[m]$ that is coverable w.r.t. $\{M_i\mid i\in [m]\}$. It is easy to see that $\widetilde{\mathrm{Cl}}(F)$ does not depend on the permutation of rows in the coefficient matrix of $F$.

In the lifting settings, we will identify subsets of $[m]$ with corresponding subsets of the lifted variables $Y$. It is especially convenient to use such correspondence for closure and amortized closure. So, we will assume that the support and the (amortized) closure of the set of linear forms over lifted variables is the set of unlifted variables.

A partial assignment $\rho$ to the set of variables $X$ is called block-respectful if, for every $i$, $\rho$ either assigns values to all variables with support $i$ or does not assign values to any of them.

Suppose that $\rho$ is a block-respectful partial assignment. Then we define by $\widehat{\rho }$ the partial assignment on the set of variables $Y$ such that $\widehat{\rho }(y_i)=g(\rho (x_{i,1},x_{i,2},\mathrm{\dots },x_{i,\mathrm{\ell }}))$ (here we assume that if the right-hand side is undefined, then the left-hand side is also undefined).

Let . A gadget (i.e. Boolean function) $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ is called $k$-stifling [15] if for every $A\subset [\mathrm{\ell }]$ of size $k$ for every $c\in \{0,1\}$ there exists $a\in {\{0,1\}}^{\mathrm{\ell }}$ such that for every $b\in {\{0,1\}}^{\mathrm{\ell }}$ if $a$ and $b$ agree on set of indices $[\mathrm{\ell }]\setminus A$, then $g(b)=c$.

It is easy to see that the majority function $Ma{j}_{2k+1}:{\{0,1\}}^{2k+1}\to \{0,1\}$ is a $k$-stifling for every $k$.

Here, we state the supercritical tradeoff between width and depth in resolution, as established by Buss and Thapen [11].

Let $𝒜$ be a proper set of partial assignments for a CNF formula $\phi (y_1,y_2,\mathrm{\dots },y_n)$.

We denote by ${\oplus }_k$ the parity gadget ${\{0,1\}}^k\to \{0,1\}$ that maps $(a_1,a_2,\mathrm{\dots },a_k)$ to $a_1+a_2+\mathrm{\cdots }+a_{k}mod2$.

For every partial assignment $\rho$ to the variables of the formula $\phi \circ {\oplus }_k$ we define the partial assignment $\tilde{\rho }$ to the variables of $\phi$ as follows:

• $\mathrm{■}$

  $\tilde{\rho }$ is defined on $y_i$, if and only if $\rho$ is defined on all $x_{i,1},x_{i,2},\mathrm{\dots },x_{i,k}$;

• $\mathrm{■}$

  $\tilde{\rho }(y_i)={⨁}_{j=1}^k\rho (x_{i,j})$.

Based on the formula $\phi \circ {\oplus }_k$ we define a set ${𝒜}^{{\oplus }_k}$ that consists of partial assignments $\rho$ to variables of $\phi \circ {\oplus }_k$ such that $\tilde{\rho }\in 𝒜$.