Amortized Closure and Its Applications in Lifting for Resolution over Parities

Efremenko, Klim; Itsykson, Dmitry

doi:10.4230/LIPIcs.CCC.2025.8

Amortized Closure and Its Applications in Lifting for Resolution over Parities

Klim Efremenko

Ben-Gurion University of the Negev, Beer-Sheva, Israel Dmitry Itsykson

Ben-Gurion University of the Negev, Beer-Sheva, Israel
On leave from Steklov Institute of Mathematics at St. Petersburg, Russia

Abstract

The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [14], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth $\mathrm{Res}(\oplus)$ refutations [14, 3]. In this work, we present amortized closure, an enhancement that retains the properties of original closure [14] but offers tighter control on its growth. Specifically, adding a new linear form increases the amortized closure by at most one. We explore two applications that highlight the power of this new concept.

Utilizing our newly defined amortized closure, we extend and provide a succinct and elegant proof of the recent lifting theorem by Chattopadhyay and Dvorak [10]. Namely we show that for an unsatisfiable CNF formula $\varphi$ and a 1-stifling gadget $g\colon\{0,1\}^{\ell}\to\{0,1\}$ , if the lifted formula $\varphi\circ g$ has a tree-like $\mathrm{Res}(\oplus)$ refutation of size $2^{d}$ and width $w$ , then $\varphi$ has a resolution refutation of depth $d$ and width $w$ . The original theorem by Chattopadhyay and Dvorak [10] applies only to the more restrictive class of strongly stifling gadgets.

As a more significant application of amortized closure, we show improved lower bounds for bounded-depth $\mathrm{Res}(\oplus)$ , extending the depth beyond that of Alekseev and Itsykson [3]. Our result establishes an exponential lower bound for depth- $\Omega(n\log n)$ $\mathrm{Res}(\oplus)$ refutations of lifted Tseitin formulas, a notable improvement over the existing depth- $\Omega(n\log\log n)$ $\mathrm{Res}(\oplus)$ lower bound.

Keywords and phrases:

lifting, resolution over parities, closure of linear forms, lower bounds, width, depth, size vs depth tradeoff

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Proof complexity

Acknowledgements:

The authors thank Yaroslav Alekseev and Alexander Knop for fruitful discussions.

Funding:

Supported by European Research Council Grant No. 949707.

DOI:

10.4230/LIPIcs.CCC.2025.8

Event:

40th Computational Complexity Conference (CCC 2025)

Editors:

Srikanth Srinivasan

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Propositional proof complexity investigates proof systems for the language of unsatisfiable CNF formulas, denoted as $\mathrm{UNSAT}$ . The fundamental question of whether the complexity classes $\mathrm{NP}$ and $\mathrm{coNP}$ are distinct is equivalent to asking whether there exists a proof system that can provide polynomial-size proofs for all formulas in $\mathrm{UNSAT}$ [12]. A central focus in proof complexity is establishing superpolynomial lower bounds on proof sizes for specific proof systems; a direction often referred to as Cook’s program, which aims to separate $\mathrm{NP}$ and $\mathrm{coNP}$ .

While many exponential-size lower bounds are known for weak proof systems, we lack superpolynomial lower bounds for Frege systems, which include standard propositional proof systems from logic textbooks. A Frege derivation is a sequence of Boolean formulas; each of them is either an axiom or is obtained from the previous by a set of sound and implicationally complete inference rules. Proving Frege lower bounds is often compared to proving Boolean formula/circuit lower bounds for explicit Boolean functions, and both seem intractable. However, progress has been made in restricted settings. An exponential lower bound for constant-depth circuits computing parity was proven in the 1980s [16, 1]. Ajtai later used a similar approach to prove a superpolynomial lower bound for bounded-depth Frege systems [2]. Razborov and Smolenski proved lower bounds for constant-depth circuits with $\lnot$ , $\lor$ , $\land$ , and $\mathrm{MOD}_{p}$ gates in 1987 [23, 21]. The analogous problem of proving a lower bound for constant-depth Frege systems using $\lnot$ , $\lor$ , $\land$ and $\mathrm{MOD}_{p}$ gates (denoted $\mathrm{AC}^{0}[p]\text{-}\mathrm{Frege}$ ) is open for all $p>1$ .

This paper is devoted to the study of the propositional proof system resolution over parities ( $\mathrm{Res}(\oplus)$ ) [19], which is a subsystem of $\mathrm{AC}^{0}[2]\text{-}\mathrm{Frege}$ . This system extends resolution by incorporating linear algebra over $\mathbb{F}_{2}$ . The proof lines in this proof system are linear clauses, disjunctions of $\mathbb{F}_{2}$ -linear equations; or, equivalently, linear clauses can be treated as negations of $\mathbb{F}_{2}$ -linear systems. A refutation of an unsatisfiable CNF formula $\varphi$ is a sequence of linear clauses such that the last linear clause in this sequence is an empty clause (i.e., constant false), and every other linear clause is obtained from the previous clauses by the resolution rule or by the weakening rule. The resolution rule allows resolve by a linear form, i.e. allows to derive $(A\lor B)$ from $A\lor f=0$ and $B\lor f=1$ . The weakening rule allows the deriving of any linear clause that semantically follows from the given. Establishing superpolynomial lower bounds on the size of $\mathrm{Res}(\oplus)$ refutations remains a significant open challenge, representing a crucial step toward proving lower bounds for the more general proof system $\mathrm{AC}^{0}[2]\text{-}\mathrm{Frege}$ .

1.1 Lifting

Lifting is a highly effective technique for establishing lower bounds by transferring them from weaker to stronger computational models. Recent developments in lifting for fragments of $\mathrm{Res}(\oplus)$ offer promising avenues toward proving a superpolynomial lower bound for general $\mathrm{Res}(\oplus)$ . The most relevant lifting results pertaining to $\mathrm{Res}(\oplus)$ are briefly described below.

Chattopadhyay, Mande, Sanyal, and Sherif [11] developed a universal lifting technique for parity decision trees via $1$ -stifling gadgets, which are characterized by the following property: a gadget $g\colon\{0,1\}^{\ell}\to\{0,1\}$ is $1$ -stifling if, for any index $i\in[\ell]$ and any target bit $b$ , there exists an assignment $y$ such that any $x$ agreeing with $y$ on all but $i$ th position yields $g(x)=b$ . Their result demonstrates that if a function (or relation) $f$ requires query complexity $d$ , then for any $1$ -stifling gadget $g$ , the lifted function (or relation) $f\circ g$ requires parity decision trees of size at least $2^{d}$ . In the proof complexity settings, this result implies that if a formula $\varphi$ requires resolution depth $d$ , then for any $1$ -stifling gadget $g$ , the lifted formula $\varphi\circ g$ requires tree-like $\mathrm{Res}(\oplus)$ size at least $2^{d}$ [11]. Independently, Beame and Koroth [5] obtained similar results. Recently, Podolskii and Shekhovostov [20] and Byramji and Impagliazzo [9] extended the results of [11] to randomized parity decision trees.

Two notions of regular $\mathrm{Res}(\oplus)$ – top-regular and bottom-regular – are defined analogously to regular resolution, inheriting its key restrictions [14]. Both variants are strictly more powerful than tree-like $\mathrm{Res}(\oplus)$ . Efremenko, Garlik, and Itsykson [14] established exponential lower bounds on the size of bottom-regular $\mathrm{Res}(\oplus)$ refutations. Later, Bhattacharya, Chattopadhyay, and Dvorak [7] applied lifting techniques to show that bottom-regular $\mathrm{Res}(\oplus)$ does not simulate classical resolution. Subsequently, Alekseev and Itsykson [3] introduced a more general lifting method that transforms formulas with large resolution depth into ones requiring exponential-size bottom-regular $\mathrm{Res}(\oplus)$ refutations.

Alekseev and Itsykson [3] applied their lifting technique to establish the first size lower bounds that apply to general $\mathrm{Res}(\oplus)$ , presenting a strong size–depth tradeoff: any $\mathrm{Res}(\oplus)$ refutation of the lifted Tseitin formula must either have exponential size or depth at least $\Omega(n\log\log n)$ , where $n$ is the number of variables. This result subsumes lower bounds for both bottom-regular and top-regular $\mathrm{Res}(\oplus)$ .

The lifting techniques of Bhattacharya, Chattopadhyay, and Dvorak [7] and Alekseev and Itsykson [3] rely heavily on the concept of closure of a set of linear forms in lifted variables, initially defined by Efremenko, Garlik, and Itsykson [14]. The closure captures the most essential unlifted variables for these linear forms. Based on this, Alekseev and Itsykson [3] developed a game-based lifting technique, which they demonstrated by the following simple and elegant example:

Theorem 1 ([3]).

If a CNF formula $\varphi$ requires resolution width $w$ , then for every $1$ -stifling gadget $g$ , the formula $\varphi\circ g$ requires $\mathrm{Res}(\oplus)$ width $w$ .

The proof of Theorem 1 proceeds by an explicit transformation of strategies, converting winning strategies from Atserias and Dalmau’s [4] resolution-width games into winning strategies for games characterizing the $\mathrm{Res}(\oplus)$ width [18].

Chattopadhyay and Dvorak [10] recently established the following lifting theorem.

Theorem 2 ([10]).

If every resolution refutation of a CNF formula $\varphi$ of width at most $w$ requires depth at least $d$ , then for every strongly stifling gadget $g$ , any tree-like $\mathrm{Res}(\oplus)$ refutation of the formula $\varphi\circ g$ of width at most $w$ has size at least $2^{d}$ .

Chattopadhyay and Dvorak [10] uncovered a striking application of this theorem: a supercritical tradeoff for tree-like $\mathrm{Res}(\oplus)$ refutations. This shows that a slight narrowing of width can force a double exponential blow-up in refutation size. Specifically, for a sufficiently small width, the tree-like $\mathrm{Res}(\oplus)$ refutation size can exceed its worst-case upper bound observed in the unrestricted case. This tradeoff is obtained by a straightforward application of Theorem 2 alongside Razborov’s corresponding tree-like resolution result [22].

Strongly stifling gadgets constitute a more restricted class compared to $1$ -stifling gadgets, meaning that Theorem 2 extends Theorem 1 and the results of [11] but only for this smaller class of gadgets. Establishing Theorem 2 requires a technically demanding proof, primarily due to the explicit transformation that directly converts a tree-like $\mathrm{Res}(\oplus)$ refutation of the lifted formula into a tree-like resolution refutation of the base formula. The proof of Theorem 2 largely mirrors the approach outlined in [11]. However, in the case of bounded width, Chattopadhyay and Dvorak diverge by utilizing forgetting parity decision trees instead of standard parity decision trees. These forgetting trees incorporate forgetting nodes that correspond to weakening rules. The most challenging aspect involves handling these forgetting nodes, for which the authors restrict themselves to strongly stifling gadgets to facilitate the analysis.

1.2 Our contributions

In this work, we contribute to the lifting technique. Namely, we develop the notion of amortized closure of a set of linear forms. This new concept retains all the desirable properties of plain closure but additionally guarantees that the amortized closure increases by at most one when a single linear form is added to the set. The construction of this amortized closure and the proof of its properties (Theorem 7) constitute the main technical contribution of our work. We give two nice applications to demonstrate this new concept’s power. We believe amortized closure is of independent interest and will find further applications in lifting theorems in proof complexity and Boolean complexity.

As a first application, we prove the following theorem, which extends Theorem 2 to the entire class of 1-stifling gadgets, thereby also generalizing Theorem 1 and the mentioned result from [11].

Theorem 3 (Theorem 37).

Let $\varphi$ be an unsatisfiable CNF formula and $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a 1-stiffling gadget. Assume that $\varphi\circ g$ has a tree-like $\mathrm{Res}(\oplus)$ refutation of width $w$ and size $2^{d}$ . Then $\varphi$ has a resolution refutation of width $w$ and depth $d$ .

We present a concise and elegant proof of Theorem 3, adapting Alekseev and Itsykson’s game approach [3] from Theorem 1 to amortized closure.

As a second and more significant application, we improve depth in the lower bound for bounded-depth $\mathrm{Res}(\oplus)$ refutations established by Alekseev and Itsykson [3]. Specifically, the following theorem implies an exponential lower bound for depth- $cn\log n$ $\mathrm{Res}(\oplus)$ refutations of lifted Tseitin formulas, where $n$ is the number of variables and $c$ is a constant.

Theorem 4 (Informal restatement of Corollary 43).

Let $\phi_{n}$ be an unsatisfiable Tseitin formula based on a $\Theta(\log n)$ -regular expander with $n$ vertices lifted by the 5-input majority gadget. Then, $\phi_{n}$ is a CNF formula with $m=\Theta(n\log n)$ variables and size $\mathrm{poly}(m)$ such that any $\mathrm{Res}(\oplus)$ refutation of $\phi_{n}$ has either size at least $2^{\Omega(m/\log m)}$ or depth at least $\Omega(m\log m)$ .

Although the first application is less significant, we present it first in the introduction as it offers a clear and natural motivation for introducing the concept of amortized closure. Namely, we begin by detailing the game-based approach of Alekseev and Itsykson [3], and then we explain why its direct application fails to establish Theorem 3, emphasizing the necessity of our amortized closure. Then, we present our main contribution, the amortized closure construction, and detail its essential properties. We conclude with the second application: we demonstrate how amortized closure helps to obtain an exponential lower bound for bounded-depth $\mathrm{Res}(\oplus)$ refutations for larger depths.

1.2.1 Bounded-width lifting

Here we present the proof idea of Theorem 3. We are going to apply the game approach that was used by Alekseev and Itsykson in the proof of Theorem 1. We start with definitions of some basic notions: lifting and closure.

Let $\varphi(y_{1},y_{2},\dots,y_{m})$ be an unsatisfiable CNF. We call the set of variables $Y=\{y_{1},y_{2},\dots,y_{m}\}$ unlifted. Let $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be an 1-stifling gadget. The lifted formula $\varphi\circ g$ depends of variables $X=\{x_{i,j}\mid i\in[m],j\in[\ell]\}$ , called lifted variables. The formula $\varphi\circ g$ represents in CNF the result of the substitution $\varphi(g(x_{1,1},\dots,x_{1,\ell}),\dots,g(x_{m,1},\dots,x_{m,\ell}))$ .

Safe sets and closure

Consider the set of $\mathbb{F}_{2}$ -linear forms $F=\{f_{1},f_{2},\dots,f_{k}\}$ in lifted variables and consider their coefficient matrix $M_{F}$ . The columns of $M_{F}$ can be splitted on $m$ blocks, where the $i$ th block corresponds to variables $x_{i,1},x_{i,2},\dots,x_{i,\ell}$ with first index $i$ . The set of linear forms $F$ is safe [14] if, among the columns of $M_{F}$ , one can find a basis that includes at most one column for each block. A crucial observation is that if a set of linear forms $F$ is safe, then any satisfiable linear system formed using the linear forms in $F$ for any assignment $\sigma$ of the unlifted variables admits a solution that respects the assignment $\sigma$ on the unlifted variables [7, 3]. Indeed, values of variables whose columns are not in the basis can be chosen arbitrarily. Since the gadget is 1-stifling, we can fix its value regardless of the value of the remaining basis variables.

However, $F$ is not necessary to be safe. A closure of $F$ is an inclusion-minimal set of blocks such that if we set zeros to all variables from these blocks, the set $F$ becomes safe. For the coefficient matrix, this operation corresponds to the removal of columns corresponding to these blocks. We will identify the closure with the corresponding set of unlifted variables. Bhattacharya, Chattopadhyay, and Dvorak noted that the closure contains all essential unlifted variables in the following sense: given a solution $\alpha$ of a linear system $\Phi$ in lifted variables, for any unlifted variable $y$ that lies outside a closure of the set of linear forms in $\Phi$ , there exists another solution $\beta$ of $\Phi$ such that the assignments induced by $\alpha$ and $\beta$ on the unlifted variables differ precisely in the value assigned to $y$ .

The following properties of closure were proved by Efremeko, Garlik, and Itsykson [14].

$\blacksquare$

(Uniqueness) Closure of the set of linear forms $F$ is unique, and it is denoted by $\mathop{\mathrm{Cl}}(F)$ ;
$\blacksquare$

(Monotonicity) If $F\subseteq F^{\prime}$ , then $\mathop{\mathrm{Cl}}(F)\subseteq\mathop{\mathrm{Cl}}(F^{\prime})$ ;
$\blacksquare$

(Span invariance) If $\langle F_{1}\rangle=\langle F_{2}\rangle$ , then $\mathop{\mathrm{Cl}}(F_{1})=\mathop{\mathrm{Cl}}(F_{2})$ ;
$\blacksquare$

(Size bound) $|\mathop{\mathrm{Cl}}(F)|\leq\dim\langle F\rangle=\mathrm{rk}\left(M_{F}\right)$ .

Using the notion of closure, Alekseev and Itsykson [3] define the correspondence between linear systems over lifted variables and partial assignments for unlifted variables as follows:

$\blacksquare$

A system of linear equations $\Psi$ over lifted variables corresponds a partial assignment $\rho$ to unlifted variables if $\rho$ is defined on $\mathop{\mathrm{Cl}}(L(\Psi))$ and $\Psi$ has a solution $\tau$ such that $\tau$ induces on the unlifted variables an assignment that is consistent with $\rho$ , where $L(\Psi)$ denotes the system of linear forms that occur in $\Psi$ . We also say that $\tau$ defines the correspondence between $\Psi$ and $\rho$ .

This correspondence is not one-to-one; it is possible that one linear system corresponds to several partial assignments and vice versa.

An important property of this correspondence is that if $\Psi$ corresponds $\rho$ and $\rho$ does not falsify any clause of $\varphi$ , then $\Psi$ does not contradict any clause of $\varphi\circ g$ .

This correspondence is in the heart of the proof of Theorem 1 since it allows the transformation of a strategy in the game characterizing resolution width of $\varphi$ to a strategy in the game characterizing $\mathrm{Res}(\oplus)$ width of $\varphi\circ g$ .

Let us try to apply this approach directly to the following proposition.

Proposition 5.

If any resolution refutation of $\varphi$ of width $w$ has depth at least $d$ , then for any 1-stifling gadget $g\colon\{0,1\}^{\ell}\to\{0,1\}$ , any $\mathrm{Res}(\oplus)$ refutation of the formula $\varphi\circ g$ of width $w$ has depth at least $d$ .

Proposition 5 is weaker than Theorem 3 since it says about depth instead of tree-like size. However, in this example, we highlight the problem, explain why the approach described above can not be applied directly, and identify the missing property of closure.

We proceed with the definition of games characterizing depth in bounded-width resolution and bounded-width $\mathrm{Res}(\oplus)$ .

A $(\varphi,w)$ -game for resolution

Consider the following game based on an unsatisfiable CNF formula $\varphi$ and a natural parameter $w$ . The game has two players: Prover and Adversary. Players save a partial assignment $\rho$ that is initially empty. For every move, Prover can either remove some value from $\rho$ or, if $|\rho|<w$ , Prover can choose a variable $x$ and ask Adversary for its value. Adversary chooses $a\in\{0,1\}$ and extends the current assignment $\rho$ by $x:=a$ . For every move, Adversary earns a coin. The game ends when $\rho$ falsifies a clause of $\varphi$ . It is known that Adversary has a strategy in the $(\varphi,w+1)$ -game that guarantees him to earn at least $d$ coins if and only if any resolution refutation of $\varphi$ within width $w$ has depth at least $d$ [6].

A $(\varphi,w)$ -game for $\mathrm{Res}(\oplus)$

Consider an extension of the previous game. This game is also based on a CNF formula $\varphi$ and a natural parameter $w$ . Now, the players, Prover and Adversary, save a linear system $\Psi$ in variables of $\varphi$ that is initially empty (i.e. constant true). On every move, Prover can either replace $\Psi$ on its semantical implication or, if the rank of $\Psi$ is less than $w$ , Prover can choose a linear form $f$ and ask Adversary for its value. Adversary chooses $a\in\{0,1\}$ and adds the equation $f=a$ to $\Psi$ . Adversary earns a coin for every move. The game ends when $\Psi$ contradicts a clause of $\varphi$ . Similarly, one can show Adversary has a strategy in the $(\varphi,w+1)$ game that guarantees him to earn at least $d$ coins if and only if any $\mathrm{Res}(\oplus)$ refutation of $\varphi$ within width $w$ has depth at least $d$ .

Let us try to prove Proposition 5 using these games. Since any resolution refutation of $\varphi$ of width at most $w$ requires depth at least $d$ , there is an Adversary’s strategy in the first $(\varphi,w+1)$ -game that guarantees him to earn at least $d$ coins. Using this strategy, we try to construct an Adversary’s strategy in the second $(\varphi\circ g,w+1)$ -game that will also guarantee the Adversary to earn at least $d$ coins. It will imply that any $\mathrm{Res}(\oplus)$ refutation of $\varphi\circ g$ within width $w$ requires depth at least $d$ .

We will describe an Adversary’s strategy in the second $(\varphi\circ g,w+1)$ -game using the known Adversary’s strategy in the first $(\varphi,w+1)$ -game. Describing Adversary’s strategy in the second game, we play in parallel in the first game, making moves instead of Prover and using the Adversary’s strategy in the first game. We maintain the following invariant: the current system $\Psi$ in the second game corresponds to the current partial assignment $\rho$ in the first game. While this invariant holds, if $\rho$ does not falsify any clause of $\varphi$ , then $\Psi$ does not contradict any clause of $\varphi\circ g$ .

If Prover in the second game changes $\Psi$ to its semantical corollary $\Psi^{\prime}$ , then playing for the Prover in the first game, we restrict $\rho$ to $\mathop{\mathrm{Cl}}(L(\Psi^{\prime}))$ in the first game. Notice that since $\Psi^{\prime}$ semantically follows from $\Psi$ , $L(\Psi^{\prime})\in\langle L(\Psi)\rangle$ , hence $\mathop{\mathrm{Cl}}(L(\Psi^{\prime}))\subseteq\mathop{\mathrm{Cl}}(L(\Psi))$ .

If Prover in the second game asks the value of a linear form $f$ , we consider two cases.

$\blacksquare$

First case: $\mathop{\mathrm{Cl}}(L(\Psi)\cup\{f\})=\mathop{\mathrm{Cl}}(L(\Psi))$ . Let $\sigma$ be the solution of $\Psi$ that defines the correspondence between $\Psi$ and $\rho$ . Adversary chooses the value $a=f|_{\sigma}$ and does nothing in the first game. It is easy to see that $\sigma$ also defines the correspondence between $\Psi\land(f=a)$ and $\rho$ ; hence, the invariant still holds.
$\blacksquare$

Second case: $\mathop{\mathrm{Cl}}(L(\Psi)\cup\{f\})\neq\mathop{\mathrm{Cl}}(L(\Psi))$ . In this case, we, playing by Prover in the first game, prolong $\rho$ to variables from $\mathop{\mathrm{Cl}}(L(\Psi)\cup\{f\})\neq\mathop{\mathrm{Cl}}(L(\Psi))$ (recall that we identify elements of closure with unlifted variables) by asking them one by one. Since we extend $\rho$ to variables out of $\mathop{\mathrm{Cl}}(L(\Psi))$ , for the new value of $\rho$ , there is a solution $\tau$ of $\Psi$ such that $\tau$ induces an assignment on unlifted variables consistent with $\rho$ . Adversary chooses the value $a=f|_{\tau}$ . Now $\tau$ defines the correspondence between $\Psi\land(f=a)$ and $\rho$ ; hence, the invariant still holds.

Unfortunately, this strategy does not allow us to estimate the number of coins that the Adversary earns in the second game. The problem is that the closure can increase significantly in one step. At this moment, we have spent many coins in the first game while earning only one coin in the second one. Theoretically, it is possible, for example, that on each odd step, Prover in the second game decreases $|\mathop{\mathrm{Cl}}(L(\Psi))|$ on $k$ and on each even step increases $|\mathop{\mathrm{Cl}}(L(\Psi))|$ by $k$ . Then, the Adversary in the second game will earn 1 coin for each pair of two consequent steps while spending $k$ coins in the first game.

To solve this issue, we define the amortized closure $\widetilde{\mathop{\mathrm{Cl}}}(F)$ that has all properties of $\mathop{\mathrm{Cl}}(F)$ and also can be increased by at most one by adding a linear form. Using amortized closure in the strategy above instead of plain closure, we can guarantee that every time we spend a coin in the first game, we earn a coin in the second game. Hence, the strategy will guarantee to earn at least $d$ coins, and we will prove Proposition 5.

The proof of Theorem 3 is very similar to the presented proof idea of Proposition 5. To characterize the size of tree-like $\mathrm{Res}(\oplus)$ refutations, we use width-bounded Prover-Delayer games instead of Prover-Adversary games for $\mathrm{Res}(\oplus)$ .

1.2.2 Amortized closure

Before defining amortized closure, consider an example where the closure increases more than by one by adding just one linear form.

Example 6.

Let $m=3$ and $\ell=2$ . Consider linear forms: $f_{1}=x_{3,2},f_{2}=x_{1,2},f_{3}=x_{2,2}+x_{3,1},f_{4}=x_{2,1}$ . The coefficient matrix of $F=\{f_{1},f_{2},f_{3},f_{4}\}$ is the following:

M_{F}=\begin{pmatrix}00&00&01\\ 01&00&00\\ 00&01&10\\ 00&10&00\end{pmatrix}

$\blacksquare$

We claim that $\mathop{\mathrm{Cl}}(f_{1},f_{2},f_{3})=\emptyset$ . Indeed, the submatrix of $M_{F}$ formed by the first three rows contains a basis from the columns $x_{1,2},x_{2,2}$ , and $x_{3,2}$ . Hence, $\{f_{1},f_{2},f_{3}\}$ is safe and, thus, $\mathop{\mathrm{Cl}}(f_{1},f_{2},f_{3})=\emptyset$ .
$\blacksquare$

Let us show that $\mathop{\mathrm{Cl}}(f_{1},f_{2},f_{3},f_{4})=\{2,3\}$ . Indeed, if we remove both the second and third blocks, the resulting matrix will have the basis consisting of only column $x_{1,2}$ . The rank of $M_{F}$ is $4$ , which is greater than the number of blocks. If we remove only the second or only the third block, the rank of the obtained matrix will be $3$ , which is also greater than the number of remaining blocks. Hence, $\mathop{\mathrm{Cl}}(f_{1},f_{2},f_{3},f_{4})=\{2,3\}$ .

Let $S$ be a finite linearly ordered set. We can extend this order to the set of all subsets of $S$ as follows: for subsets $A,B\subseteq S$ , we say that $A$ is less than $B$ if the largest element in the symmetric difference $A\triangle B$ belongs to $B$ . In our case, we take $S=[m]$ , equipped with the natural order. This induces a total order $\preceq$ on the subsets of $[m]$ . While the specific linear order on $[m]$ is not essential, using the natural order has a convenient consequence: the resulting order $\preceq$ corresponds to comparing the binary representations of subsets: for each subset $A\subseteq[m]$ , associate the integer $\sum_{i\in A}2^{i}$ . Then $A\preceq B$ if and only if this sum for $A$ is less than or equal to that for $B$ .

Let $F$ be a set of linear forms with coefficient matrix $M_{F}$ . We say that a subset of blocks $A\subseteq[m]$ is coverable with respect to $M_{F}$ if one can choose $|A|$ linearly independent columns from the matrix $M_{F}$ such that every block from $A$ contains one chosen column. An amortized closure of $F$ is the $\preceq$ -maximal subset of $[m]$ that is coverable with respect to $M_{F}$ . We denote the amortized closure of $F$ by $\widetilde{\mathop{\mathrm{Cl}}}(F)$ .

Let us clarify why we use the term amortized. The sequence $\mathop{\mathrm{Cl}}(\{f_{1}\}),\mathop{\mathrm{Cl}}(\{f_{1},f_{2}\}),\dots,% \mathop{\mathrm{Cl}}(f_{1},f_{2},\dots,f_{n})$ is monotonic, but the difference between consecutive terms can be large. In contrast, as we will see later, the amortized closure sequence $\widetilde{\mathop{\mathrm{Cl}}}(\{f_{1}\}),\widetilde{\mathop{\mathrm{Cl}}}(% \{f_{1},f_{2}\}),\dots,\widetilde{\mathop{\mathrm{Cl}}}(f_{1},f_{2},\dots,f_{n})$ is also monotonic, yet each step differs from the previous by at most one element. Moreover, each term in this sequence contains the corresponding term of the original closure sequence. The amortized closure anticipates future growth by including certain elements early, thus avoiding sudden increases in size.

In Example 6, $\widetilde{\mathop{\mathrm{Cl}}}(f_{1})=\{3\},\widetilde{\mathop{\mathrm{Cl}}}% (f_{1},f_{2})=\{1,3\},\widetilde{\mathop{\mathrm{Cl}}}(f_{1},f_{2},f_{3})=\{1,% 2,3\}$ and $\widetilde{\mathop{\mathrm{Cl}}}(f_{1},f_{2},f_{3},f_{4})=\{1,2,3\}$ .

The uniqueness of amortized closure trivially follows from the definition. We establish other properties in the following theorem:

Theorem 7.

Amortized closure has the following properties.

1.

(Size bound) $|\widetilde{\mathop{\mathrm{Cl}}}(F)|\leq\dim\langle F\rangle$ (Lemma 19);
2.

(Span invariance) If $\langle F\rangle=\langle H\rangle$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F)=\widetilde{\mathop{\mathrm{Cl}}}(H)$ (Lemma 20 );
3.

(Lipschitz continuity) $\widetilde{\mathop{\mathrm{Cl}}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(F% \cup\{f\})$ and $|\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})|\leq|\widetilde{\mathop{\mathrm{% Cl}}}(F)|+1$ (Theorem 21);
4.

(Monotonicity) If $F\subseteq\langle H\rangle$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(H)$ (Corollary 22);
5.
(Relation between closures)
1. (a)
  
  $\mathop{\mathrm{Cl}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(F)$ (Lemma 26);
2. (b)
  
  If $\mathop{\mathrm{Cl}}(F\cup\{f\})\neq\mathop{\mathrm{Cl}}(F)$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})=\widetilde{\mathop{\mathrm{Cl}}}(F)$ (Lemma 28).

Since the amortized closure contains the plain closure, the amortized closure also contains all essential unlifted variables, i.e. linear systems do not restrict values of unlifted variables out of the amortized closure. The most technically involved part is the proof of Lipschitz continuity of amortized closure.

1.2.3 Lower bound for depth- $cn\log n$ $\mathrm{Res}(\oplus)$

Alekseev and Itsykson [3] have recently proved that every $\mathrm{Res}(\oplus)$ refutation of lifted Tseitin formulas either has size at least $2^{\Omega(n/\log n)}$ or depth at least $\Omega(n\log\log n)$ , where $n$ is the number of variables. Our Theorem 4 is the improvement of this result, and its proof is basically built on the proof by Alekseev and Itsykson [3]. To explain our contribution, we start by presenting the idea of the former result. This tradeoff was proved for the lifted formulas $\varphi\circ g$ , where $g:\{0,1\}^{\ell}\to\{0,1\}$ is a $2$ -stifling gadget (for example, $g$ can be the $\ell$ -input majority for $\ell\geq 5$ ; see Section 3.2 for definition) and $\varphi$ satisfies rather strong conditions. Namely, there exists a set of partial assignments $\mathcal{A}$ to variables of $\varphi$ and integer numbers $t$ and $p$ such that the following conditions hold.

1.

Any assignment from $\mathcal{A}$ does not falsify a clause of $\varphi$ .
2.

For any assignment $\sigma\in\mathcal{A}$ , for any $\rho\subseteq\sigma$ , $\rho\in\mathcal{A}$ .
3.
Any $\mathrm{Res}(\oplus)$ refutation $\Pi$ of $\varphi\circ g$ satisfies the following random-walk property.
- $\blacksquare$
  
  We say that a linear clause $C$ in the lifted variables is $\mathcal{A}$ -good if the system $\lnot C$ corresponds to some assignment from $\mathcal{A}$ ; i.e. there exists a solution $\sigma$ of $\lnot C$ that induces on $\mathop{\mathrm{Cl}}(L(C))$ an assignment from $\mathcal{A}$ , where $L(C)$ denotes the set of linear forms that appear in $C$ .
- $\blacksquare$
  
  Consider arbitrary $\mathcal{A}$ -good clause $C_{0}$ from $\Pi$ such that $|\mathop{\mathrm{Cl}}(L(C_{0}))|\leq t/2$ . Let $\rho_{0}\in\mathcal{A}$ correspond to $\lnot C_{0}$ . Let $\tau$ be a random solution of $\lnot C_{0}$ among all solutions inducing the partial assignment $\rho_{0}$ on unlifted variables. We make $t/2$ steps in $\Pi$ starting in $C_{0}$ , and on each step, we move from the current linear clause to a premise of the rule falsified by $\tau$ (we count only steps corresponding to resolution rules and do not count weakening rules). Then, with probability at least $2^{-p}$ , this walk finishes in an $\mathcal{A}$ -good clause.

Fortunately, Tseitin formulas meet these conditions for appropriate $\mathcal{A},p$ , and $t$ [3].

Assume that there is a $\mathrm{Res}(\oplus)$ refutation $\Pi$ of $\varphi\circ g$ of size less than $2^{s}$ , where $s$ is some parameter. The following argument was used in [3] to prove that $\Pi$ has a large depth. Let $C_{0}$ be the empty clause from a $\Pi$ ; $C_{0}$ is $\mathcal{A}$ -good for trivial reasons. By the random-walk property on the distance $t/2$ from $C_{1}$ , there is an $\mathcal{A}$ -good clause $C_{1}$ . If $|\mathop{\mathrm{Cl}}(L(C_{1}))|\leq t/2$ , then by the random walk property on the distance $t/2$ from $C_{0}$ , there is an $\mathcal{A}$ -good clause $C_{2}$ , and so on. Let we finish this process at $\mathcal{A}$ -good clause $C_{k}$ such that $|\mathop{\mathrm{Cl}}(L(C_{k}))|>t/2$ . Then we get that the depth of $\Pi$ is at least $kt/2$ . We have to show that $k$ can be sufficiently large, for this we have to use that the size of $\Pi$ is less than $2^{s}$ .

To bound $k$ from below, Alekseev and Itsykson [3] estimate the rank of $\lnot C_{i+1}$ in comparison to the rank $\lnot C_{i}$ . Namely, the size upper bound on $\Pi$ together with the random-walk property imply that one can choose $C_{i+1}$ such that $\mathrm{rk}(\lnot C_{i+1})\leq\mathrm{rk}(\lnot C_{i})(\ell+1)+p+s$ . Since the estimated value of the rank can be increased in at least $(\ell+1)$ times by one step, in this approach $k\leq\log_{(\ell+1)}\frac{t}{2(p+s)}+1$ . The total depth that can be achieved by this approach is at most $O(t\log\frac{t}{p+s})$ .

Our improvement

Instead of estimating rank, we suggest estimating the size of the amortized closure $|\widetilde{\mathop{\mathrm{Cl}}}(\lnot C_{i})|$ . We prove the following lemma.

Lemma 8 (Lemma 38).

Let $\Phi$ and $\Psi$ be two linear systems in the lifted variables $X=\{x_{i,j}\mid i\in[m],j\in[\ell]\}$ . Let $\pi$ be a partial assignment defined on $\{x_{i,j}\mid i\in[\mathop{\mathrm{Cl}}(L(\Phi))],j\in[\ell]\}$ . Let $\Sigma$ consist of all solutions $\sigma$ of $\Phi$ such that $\sigma$ extends $\pi$ . Assume that $\Sigma\neq\emptyset$ . Let $\tau$ be a random element of $\Sigma$ . Then $\Pr[\tau\mbox{ satisfies }\Psi]\leq 2^{|\widetilde{\mathop{\mathrm{Cl}}}(L(% \Phi))|-|\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))|}$ .

Lemma 8, the upper bound $|\Pi|<2^{s}$ and the random-walk property imply that on the distance $t/2$ from $C_{i}$ one can find an $\mathcal{A}$ -good $C_{i+1}$ such that $|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{i+1})|\leq|\widetilde{\mathop{\mathrm{% Cl}}}(L(C_{i})|+p+s$ . So we can achieve $k=\lceil\frac{t}{2(p+s)}\rceil$ and depth at least $\Omega\left(\frac{t^{2}}{p+s}\right)$ . This is sufficient to establish Theorem 4.

Notice that there is a potential way to improve $k$ by improving the upper bound on $p$ in the random-walk property and taking smaller $s$ .

1.3 Discussion about closures

The concept of closure proves helpful when addressing problems with an underlying lifted structure. In such cases, the closure of a set of linear forms effectively captures the most essential unlifted variables. Furthermore, when the lifting involves a 1-stifling gadget, the set of linear forms imposes no constraints on variables outside the closure.

Plain closure is monotone but not necessarily Lipschitz. Amortized closure, containing plain closure, is both monotone and Lipschitz. For the best results, using both is recommended: plain closure more accurately identifies essential unlifted variables, while amortized closure allows for more convenient estimations.

While (as shown by [11]) closure is not required for parity decision trees (i.e., for tree-like $\mathrm{Res}(\oplus)$ ), where essential unlifted variables can be captured iteratively along a path, closure (both plain and amortized) provides a key advantage in dag-like proofs: path-independence. This invariance is why closure is necessary for lower bounds in regular and bounded-depth $\mathrm{Res}(\oplus)$ . Furthermore, our first application shows that even for tree-like $\mathrm{Res}(\oplus)$ in bounded-width settings, amortized closure can give better results, as in our case, it applies to a broader class of gadgets.

A limitation of using closure is that variables within the closure are not necessarily indeed constrained by the linear forms. It seems to be one of the primary obstacles preventing us from applying a bottleneck argument to unrestricted $\mathrm{Res}(\oplus)$ .

1.4 Further research

We identify the following questions as interesting directions for further investigation.

$\blacksquare$

Prove a supercritical tradeoff between the size and depth of dag-like $\mathrm{Res}(\oplus)$ refutations. Specifically, provide an example of a family of formulas with a polynomial-size $\mathrm{Res}(\oplus)$ refutation, yet every such refutation has a depth that exceeds the number of variables. While numerous supercritical tradeoffs between the size and depth exist for resolution [15, 8, 13, 17], all use the width-size relationship, which remains unknown for $\mathrm{Res}(\oplus)$ . Thus, the question requires some additional ideas.
$\blacksquare$

Prove a superpolynomial lower bound for $\mathrm{Res}(\oplus)$ refutations of depth $n^{1+\epsilon}$ for some $\epsilon>0$ . As we noticed above, improving the success probability in the random-walk theorem from [3] is sufficient for further depth improvement.
$\blacksquare$

Prove a lifting theorem that translates lower bounds on resolution width to lower bounds on the size of $\mathrm{Res}(\oplus)$ refutations with depth at most $n$ . The lifted Tseitin formula is the only known example of a lower bound for bounded-depth $\mathrm{Res}(\oplus)$ . Such a lifting theorem will provide a method for generating many such examples.

2 Closure and amortized closure

In this section, we give preliminaries about closure, provide a definition of amortized closure, and prove its main properties.

Throughout the paper, we use the notation $\langle S\rangle$ to denote the span of the set of vectors $S$ from some vector space.

2.1 Safe and dangerous sets of linear forms

We consider the set of propositional variables $X=\{x_{i,j}\mid i\in[m],j\in[\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},\dots,x_{i,\ell}$ form the $i$ th block, for $i\in[m]$ .

Consider sets of linear forms using variables from $X$ over the field $\mathbb{F}_{2}$ . The support of a linear form $f=x_{i_{1},j_{1}}+x_{i_{2},j_{2}}+\dots+x_{i_{k},j_{k}}$ is the set $\{i_{1},i_{2},\dots,i_{k}\}$ of blocks of variables that appear in $f$ with non-zero coefficients. We denote the support by $\mathrm{supp}(f)$ . The support of a set of linear forms $F$ is the union of the supports of all linear forms in this set. We denote it by $\mathrm{supp}(F)$ . We say that a linearly independent set of linear forms $F$ is dangerous if $|F|>|\mathrm{supp}(F)|$ . We say that a set of linear forms $F$ is safe if $\langle F\rangle$ does not contain a dangerous set. If $F$ is linearly dependent but $\langle F\rangle$ contains a dangerous set, instead of saying that $F$ is dangerous, we say it is not safe.

Every linear form corresponds to a vector of its coefficients indexed by the variables from the set $X$ . Given a list of linear forms $f_{1},f_{2},\dots,f_{k}$ , one may consider their coefficient matrix of size $k\times|X|$ in which the $i$ -th row coincides with the coefficient vector of $f_{i}$ .

Theorem 9 ([14]).

Let $f_{1},f_{2},\dots,f_{k}$ be linearly independent linear forms and let $M$ be their coefficient matrix. Then, the following conditions are equivalent.

(1)

The set of linear forms $f_{1},f_{2},\dots,f_{k}$ is safe.
(2)

One can choose $k$ blocks and one variable from each of these blocks such that the columns of $M$ corresponding to the $k$ chosen variables are linearly independent. (Since $\mathrm{rk}(M)=k$ the chosen set of columns forms the basis.)

2.2 Closure

Let $S\subseteq[m]$ be a set of blocks; for a linear form $f$ we denote by $f[\setminus S]$ a linear form obtained from $f$ by substituting $0$ for all variables with support in $S$ . For a set of linear forms $F$ we will use the notation $F[\setminus S]=\{f[\setminus S]\mid f\in F\}$ .

A closure of a set of linear forms $F$ is any inclusion-wise minimal set $S\subseteq[m]$ such that $F[\setminus S]$ is safe.

Lemma 10 (Uniqueness [14]).

For any $F$ , its closure is unique.

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

Lemma 11 (Monotonicity [14]).

If $F_{1}\subseteq F_{2}$ , then $\mathop{\mathrm{Cl}}(F_{1})\subseteq\mathop{\mathrm{Cl}}(F_{2})$ .

Lemma 12 (Span invariance [14]).

$\mathop{\mathrm{Cl}}(F)=\mathop{\mathrm{Cl}}(\langle F\rangle)$ .

Lemma 13 (Size bound [14]).

$|\mathop{\mathrm{Cl}}(F)|+\dim\langle F[\setminus\mathop{\mathrm{Cl}}(F)]% \rangle\leq\dim\langle F\rangle$ , and hence $|\mathop{\mathrm{Cl}}(F)|\leq\dim\langle F\rangle$ .

A set of linear forms $F$ is minimally dangerous if it is dangerous, and $\langle F\rangle$ does not contain a dangerous set with strictly smaller support than the support of $F$ . Recall that a dangerous set is necessarily linearly independent.

Consider the following algorithm:

Algorithm 14.

Input: a set of linear forms $F$ .

1.

$S\leftarrow\emptyset$ ;
2.
While $\langle F[\setminus S]\rangle$ contains dangerous sets:
1. (a)
  
  Find a minimally dangerous set in $\langle F[\setminus S]\rangle$ . Let $T$ be its support.
2. (b)
  
  $S\leftarrow S\cup T$ .
3.

Return $S$ .

Lemma 15 ([14]).

Algorithm 14 computes $\mathop{\mathrm{Cl}}(F)$ regardless on choosing $T$ on Step 2a.

Corollary 16.

If $F$ contains a minimally dangerous set with support $T\subseteq[m]$ , then $\mathop{\mathrm{Cl}}(F)=T\cup\mathop{\mathrm{Cl}}(F[\setminus T])$ .

2.3 Coverable sets

Let $V_{1},V_{2},\dots,V_{m}$ be sets of vectors from some linear space over a field $\mathbb{F}$ .

We say that a subset $A\subseteq[m]$ is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ if for every $i\in A$ there is $v_{i}\in V_{i}$ such the set $\{v_{i}\mid i\in A\}$ is linearly independent.

The following extension of the well-known Hall’s matching theorem was proved by Welsh in 1971.

Theorem 17 ([24]).

A set $A\subseteq[m]$ is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ if and only if for every $B\subseteq A$ the dimension of $\langle\cup_{i\in B}V_{i}\rangle$ is at least $|B|$ .

We consider the following order $\preceq$ on the subsets of $[m]$ : for any $A,B\subseteq[m]$ , $A\preceq B$ , if and only if $\sum_{i\in A}2^{i}\leq\sum_{i\in B}2^{i}$ . We also define the strict order $A\prec B$ , if and only if $A\preceq B$ and $A\neq B$ . In other words, we can say that $A$ is less than $B$ if the largest element in the symmetric difference $A\triangle B$ belongs to $B$ .

The order $\preceq$ plays a central role in the following theorem, which is proved in Subsection 2.5.

Theorem 18.

Let $L$ and $L^{\prime}$ be vector spaces over a field $\mathbb{F}$ let $e\in L^{\prime}$ be such that $e\notin L$ and $L^{\prime}=\langle L\cup\{e\}\rangle$ . Let $\pi$ denote the projection from $L^{\prime}$ to $L$ . Let $V^{\prime}_{1},V^{\prime}_{2},\dots,V^{\prime}_{m}$ be sets of vectors from $L^{\prime}$ . Let for every $i\in[m]$ , $V_{i}=\{\pi(v)\mid v\in V_{i}^{\prime}\}$ .

Let $T\subseteq[m]$ be $\preceq$ -maximal coverable set with respect to $V^{\prime}_{1},V^{\prime}_{2},\dots,V^{\prime}_{m}$ . Let $S\subseteq[m]$ be $\preceq$ -maximal coverable set with respect to $V_{1},V_{2},\dots,V_{m}$ . Then $S\subseteq T$ and $|T\setminus S|\leq 1$ .

2.4 Amortized closure and its properties

Let $X=\{x_{i,j}\mid i\in[m],j\in[\ell]\}$ be the set of propositional variables and $F=\{f_{1},f_{2},\dots,f_{n}\}$ be a set of $\mathbb{F}_{2}$ -linear forms with variables from $X$ . Consider a coefficient matrix 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 $V_{i}$ consist of matrix columns corresponding to variables with support $\{i\}$ .

An amortized closure of $F$ , denoted by $\widetilde{\mathop{\mathrm{Cl}}}(F)$ , is the $\preceq$ -maximal subset of $[m]$ that is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ . It is easy to see that $\widetilde{\mathop{\mathrm{Cl}}}(F)$ does not depend on the permutation of rows in the coefficient matrix of $F$ .

In the rest of the subsection, we prove the properties of amortized closure (i.e., Theorem 7).

Lemma 19 (Size bound).

$|\widetilde{\mathop{\mathrm{Cl}}}(F)|\leq\dim\langle F\rangle$ .

Proof.

$|\widetilde{\mathop{\mathrm{Cl}}}(F)|$ is at most the rank of a coefficient matrix of $F$ that equals $\dim\langle F\rangle$ . $\hfill\blacktriangleleft$

Lemma 20 (Span invariance).

If $\langle F_{1}\rangle=\langle F_{2}\rangle$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})=\widetilde{\mathop{\mathrm{Cl}}}(F_{2})$ .

Proof.

It is well-known that for every finite set of vectors $U$ from some linear space over $\mathbb{F}_{2}$ and for every basis of $\langle U\rangle$ one can obtain this basis from $U$ by a sequence of the following to operations: 1) adding one vector to another; 2) removing zero.

Since $\langle F_{1}\rangle=\langle F_{2}\rangle$ , we can choose the common basis in them. Thus, it is sufficient to verify that $\widetilde{\mathop{\mathrm{Cl}}}(\{f_{1},f_{2},\dots,f_{n}\})=\widetilde{% \mathop{\mathrm{Cl}}}(\{f_{1}+f_{2},f_{1},\dots,f_{n}\})$ and $\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{0\})=\widetilde{\mathop{\mathrm{Cl}}}(F)$ . Both these properties straightforwardly follow from the definition of amortized closure. $\hfill\blacktriangleleft$

Theorem 21 (Lipschitz continuity).

$\widetilde{\mathop{\mathrm{Cl}}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(F% \cup\{f\})$ and $|\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})\setminus\widetilde{\mathop{% \mathrm{Cl}}}(F)|\leq 1$ .

Proof.

This theorem follows from Theorem 18; we proceed with a formal verification.

Let us denote $n=|F|$ and $F^{\prime}=F\cup\{f\}$ . Consider the coefficient matrix $M_{F^{\prime}}$ of the set of linear forms of $F^{\prime}$ . The coefficient matrix $M_{F}$ of the set of linear forms $F$ is obtained from $M_{F^{\prime}}$ by removing the last row.

We choose $\mathbb{F}=\mathbb{F}_{2}$ . Let $L^{\prime}=\mathbb{F}_{2}^{n+1}$ and $L=\mathbb{F}_{2}^{n}$ , identified with the subspace of $L$ , where the last coordinate is zero. Thus if $e=(0,0,\dots,0,1)\in\mathbb{F}_{2}^{n+1}$ , then $L^{\prime}=\langle L\cup\{e\}\rangle$ ; let $\pi$ denote the projection from $L^{\prime}$ to $L$ .

Let $V^{\prime}_{i}$ for $i\in[m]$ consist of columns of the coefficient matrix $M_{F^{\prime}}$ of $F^{\prime}$ corresponding to variables with support $\{i\}$ . Then for all $i\in[m]$ , the set $V_{i}=\{\pi(v)\mid v\in V_{i}^{\prime}\}$ consists of columns of the coefficient matrix $M_{F}$ of the set $F$ , corresponding to variables whose support is exactly $\{i\}$ . We apply Theorem 18 with $S=\widetilde{\mathop{\mathrm{Cl}}}(F)$ and $T=\widetilde{\mathop{\mathrm{Cl}}}(F^{\prime})=\widetilde{\mathop{\mathrm{Cl}}% }(F\cup\{f\})$ , yielding $\widetilde{\mathop{\mathrm{Cl}}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(F% \cup\{f\})$ and $|\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})\setminus\widetilde{\mathop{% \mathrm{Cl}}}(F)|\leq 1$ . $\hfill\blacktriangleleft$

Corollary 22 (Monotonicity).

If $F_{1}\subseteq\langle F\rangle$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})\subseteq\widetilde{\mathop{\mathrm{Cl}% }}(F)$ .

Proof.

By Theorem 21, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})\subseteq\widetilde{\mathop{\mathrm{Cl}% }}(F_{1}\cup F)$ and by Lemma 20, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1}\cup F)=\widetilde{\mathop{\mathrm{Cl}}}% (F)$ . $\hfill\blacktriangleleft$

2.4.1 Relation between closures

Now we prove item 5 of Theorem 7. To compare plain and amortized closures, we establish Lemma 24, the analogue of Corollary 16.

We call a subset $T\subseteq[m]$ important for a set of linear forms $F$ if there exists a safe linearly independent set of linear forms $\{h_{1},h_{2},\dots,h_{k}\}\subseteq\langle F\rangle$ with support $T$ such that $k=|T|$ .

Proposition 23.

If $\langle F\rangle$ contains a minimal dangerous set with support $T$ , then $T$ is important.

Proof.

Let $\{h_{1},h_{2},\dots,h_{k},h_{k+1}\}$ be a minimal dangerous set with support $T$ . The minimality implies that the set $h_{1},h_{2},\dots,h_{k}$ is safe. The support of $\{h_{1},h_{2},\dots,h_{k}\}$ equals $T$ , since if it is less than $T$ , this set would be dangerous. Hence, $T$ is important. $\hfill\blacktriangleleft$

Lemma 24.

Let $T$ be important for $F$ . Then $\widetilde{\mathop{\mathrm{Cl}}}(F)=T\cup\widetilde{\mathop{\mathrm{Cl}}}(F[% \setminus T])$ .

Proof.

Since $T$ is important, there exists a linearly independent and safe set $H=\{h_{1},h_{2},\dots,h_{k}\}\in\langle F\rangle$ with support $T$ , where $k=|T|$ . Let us choose a basis $F_{1}$ in $\langle F\rangle$ that contains $H$ . Since $\langle F_{1}\rangle=\langle F\rangle$ , $\langle F_{1}[\setminus T]\rangle=\langle F[\setminus T]\rangle$ , hence, by Lemma 20, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})=\widetilde{\mathop{\mathrm{Cl}}}(F)$ and $\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])=\widetilde{\mathop{% \mathrm{Cl}}}(F[\setminus T])$ . So it is sufficient to show that $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})=T\cup\widetilde{\mathop{\mathrm{Cl}}}(% F_{1}[\setminus T])$ .

Let $V_{i}$ , for $i\in[m]$ , be the set of columns of the coefficient matrix $M_{F_{1}}$ of $F_{1}$ , corresponding to variables with support $\{i\}$ . Our first goal is to show that $T\cup\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])$ is coverable w.r.t. $V_{1},\dots,V_{m}$ .

Consider the coefficient matrix $M_{H}$ of $H$ . Since $H$ is safe and linearly independent, Theorem 9 implies that for every $i\in T$ , one can choose a column $u_{i}$ of $M_{H}$ corresponding to a variable with support $i$ such that all these columns are linearly independent. $M_{H}$ is a submatrix of the coefficient matrix $M_{F_{1}}$ of $F_{1}$ . Let for $i\in T$ , $v_{i}$ be the column in $M_{F_{1}}$ corresponding to $u_{i}$ . The set $\{v_{i}\mid i\in T\}$ is also linearly independent since for all $i\in T$ , $u_{i}$ is the prefix of $v_{i}$ . Notice that all columns of $M_{F_{1}}$ corresponding to variables with support out of $T$ have zeros in the first $k$ coordinates, hence for all $i\in T$ , $v_{i}$ does not belong to the linear span of all columns of $M_{F_{1}}$ with support out of $T$ . Since the coefficient matrix of $F_{1}[\setminus T]$ is obtained from the coefficient matrix of $F_{1}$ by substitution zero to all variables with support from $T$ , for every $i\in\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])$ there is $v_{i}\in V_{i}$ such that the set $\{v_{i}\mid i\in\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])\}$ is linearly independent. Thus, the set $\{v_{i}\mid i\in T\cup\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])\}$ is linearly independent, thus $T\cup\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])$ is coverable w.r.t. $V_{1},\dots,V_{m}$ .

For all $i\in[m]$ , let $V^{\prime}_{i}=V_{i}$ if $i\notin T$ and $V^{\prime}_{i}=\{0\}$ otherwise. Since $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})$ is coverable w.r.t. $\{V_{i}\mid i\in[m]\}$ , $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})\setminus T$ is coverable w.r.t. $\{V^{\prime}_{i}\mid i\in[m]\}$ . By the definition, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])$ is $\preceq$ -maximal subset of $[m]$ that is coverable w.r.t. $\{V^{\prime}_{i}\mid i\in[m]\}$ . Hence, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})\setminus T\preceq\widetilde{\mathop{% \mathrm{Cl}}}(F_{1}[\setminus T])$ . We know that $\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])\cap T=\emptyset$ . Thus, $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})=T\cup(\widetilde{\mathop{\mathrm{Cl}}}% (F_{1})\setminus T)\preceq T\cup\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[% \setminus T])$ . Since $T\cup\widetilde{\mathop{\mathrm{Cl}}}(F_{1}[\setminus T])$ is coverable w.r.t. $\{V_{i}\mid i\in[m]\}$ , we get $\widetilde{\mathop{\mathrm{Cl}}}(F_{1})=T\cup\widetilde{\mathop{\mathrm{Cl}}}(% F_{1}[\setminus T])$ . $\hfill\blacktriangleleft$

Lemma 25.

If $F\subseteq G$ , then $\widetilde{\mathop{\mathrm{Cl}}}(G)=\mathop{\mathrm{Cl}}(F)\cup\widetilde{% \mathop{\mathrm{Cl}}}(G[\setminus\mathop{\mathrm{Cl}}(F)])$ .

Proof.

Consider the execution of Algorithm 14 on $F$ . Let $T_{1},T_{2},\dots,T_{s}$ be the minimally dangerous sets found by the algorithm. Then $\mathop{\mathrm{Cl}}(F)=T_{1}\cup T_{2}\cup\dots T_{s}$ .

By Proposition 23, $T_{1}$ is important for $F$ , hence it is important for $G$ . Then, by Lemma 24, $\widetilde{\mathop{\mathrm{Cl}}}(G)=T_{1}\cup\widetilde{\mathop{\mathrm{Cl}}}(% G[\setminus T_{1}])$ . By Proposition 23, $T_{2}$ is important for $F[\setminus T_{1}]$ , hence it is important for $G[\setminus T_{1}]$ . Then, by Lemma 24, $\widetilde{\mathop{\mathrm{Cl}}}(G)=T_{1}\cup T_{2}\cup\widetilde{\mathop{% \mathrm{Cl}}}(G[\setminus(T_{1}\cup T_{2})])$ . Continue this reasoning $s$ times we get that $\widetilde{\mathop{\mathrm{Cl}}}(G)=T_{1}\cup T_{2}\cup\dots\cup T_{s}\cup% \widetilde{\mathop{\mathrm{Cl}}}(G[\setminus(T_{1}\cup T_{2}\cup\dots\cup T_{s% })])=\mathop{\mathrm{Cl}}(F)\cup\widetilde{\mathop{\mathrm{Cl}}}(G[\setminus% \mathop{\mathrm{Cl}}(F)])$ . $\hfill\blacktriangleleft$

Lemma 26.

$\mathop{\mathrm{Cl}}(F)\subseteq\widetilde{\mathop{\mathrm{Cl}}}(F)$ .

Proof.

Follows from Lemma 25 applied to $G=F$ . $\hfill\blacktriangleleft$

Our immediate goal is to show that if adding a linear form $f$ increases the plain closure, it does not affect the amortized closure. We begin by proving this in the special case where the closure of the initial set is empty.

Lemma 27.

If $F$ is safe and for a linear form $f$ , $F\cup\{f\}$ is not safe, then $\widetilde{\mathop{\mathrm{Cl}}}(F)=\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})$ .

Proof.

Since $F\cup\{f\}$ is not safe, $\langle F\cup\{f\}\rangle$ contains a minimally dangerous set $H=\{h_{1},h_{2},\dots,h_{k+1}\}$ with support $T$ of size $k$ . Assume that $H$ contains the maximal possible number of elements from $\langle F\rangle$ . It is easy to see that the number of such elements should be $k$ . Indeed, this number should be less than $k+1$ since $F$ is safe; if $H$ contains two elements from $f+\langle F\rangle$ , we can change one of them to their sums, and this increases the number of elements from $\langle F\rangle$ . Let $h_{1},h_{2},\dots,h_{k}\in\langle F\rangle$ and $h_{k+1}\in f+\langle F\rangle$ . Since $F$ is safe, the support of the set $\{h_{1},h_{2},\dots,h_{k}\}$ is also $T$ . Hence, $T$ is important, thus

\widetilde{\mathop{\mathrm{Cl}}}(F\cup f)\mathop{=}\limits^{\mbox{\small(Lem.% \leavevmode\nobreak\ \ref{acl-basis-inv})}}\widetilde{\mathop{\mathrm{Cl}}}(F% \cup\{h_{k+1}\})\mathop{=}\limits^{\mbox{\small(Lem.\leavevmode\nobreak\ \ref{% aCl-important})}}T\cup\widetilde{\mathop{\mathrm{Cl}}}((F\cup\{h_{k+1}\})[% \setminus T])\mathop{=}\limits^{\mbox{\small(Lem.\leavevmode\nobreak\ \ref{acl% -basis-inv})}}\\ T\cup\widetilde{\mathop{\mathrm{Cl}}}(F[\setminus T])\mathop{=}\limits^{\mbox{% \small(Lem.\leavevmode\nobreak\ \ref{aCl-important})}}\widetilde{\mathop{% \mathrm{Cl}}}(F).\quad\

$\hfill\blacktriangleleft$

The following lemma extends Lemma 27 to the general case.

Lemma 28.

If $\mathop{\mathrm{Cl}}(F)\subsetneq\mathop{\mathrm{Cl}}(F\cup\{f\})$ , then $\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})=\widetilde{\mathop{\mathrm{Cl}}}(F)$ .

Proof.

Consider the execution of Algorithm 14 on $F$ . Let $T_{1},T_{2},\dots,T_{s}$ be the minimally dangerous sets found by the algorithm. Then $\mathop{\mathrm{Cl}}(F)=T_{1}\cup T_{2}\cup\dots T_{s}$ . Notice that we can construct the closure of $F\cup\{f\}$ using the algorithm starting from the same sets $T_{1},T_{2},\dots,T_{s}$ . By multiple applications of Lemma 16, we get that $\mathop{\mathrm{Cl}}(F\cup\{f\})=\mathop{\mathrm{Cl}}(F)\cup\mathop{\mathrm{Cl% }}(F\cup\{f\}[\setminus\mathop{\mathrm{Cl}}(F)])$ . By the definition of closure, $F[\setminus\mathop{\mathrm{Cl}}(F)])$ is safe; since $\mathop{\mathrm{Cl}}(F\cup\{f\})\neq\mathop{\mathrm{Cl}}(F)$ , the set of linear forms $(F\cup\{f\})[\setminus\mathop{\mathrm{Cl}}(F)])$ is not safe. By Lemma 27, $\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})[\setminus\mathop{\mathrm{Cl}}(F)]% =\widetilde{\mathop{\mathrm{Cl}}}(F)[\setminus\mathop{\mathrm{Cl}}(F)]$ .

By Lemma 25 we get $\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})=\widetilde{\mathop{\mathrm{Cl}}}(% (F\cup\{f\})[\setminus\mathop{\mathrm{Cl}}(F)])\cup\mathop{\mathrm{Cl}}(F)$ and $\widetilde{\mathop{\mathrm{Cl}}}(F)=\widetilde{\mathop{\mathrm{Cl}}}(F[% \setminus\mathop{\mathrm{Cl}}(F)])\cup\mathop{\mathrm{Cl}}(F)$ .

Finally,

\widetilde{\mathop{\mathrm{Cl}}}(F\cup\{f\})=\widetilde{\mathop{\mathrm{Cl}}}(% (F\cup\{f\})[\setminus\mathop{\mathrm{Cl}}(F)])\cup\mathop{\mathrm{Cl}}(F)=% \widetilde{\mathop{\mathrm{Cl}}}(F[\setminus\mathop{\mathrm{Cl}}(F)])\cup% \mathop{\mathrm{Cl}}(F)=\widetilde{\mathop{\mathrm{Cl}}}(F).\

$\hfill\blacktriangleleft$

2.5 Proof of Theorem 18

Proof of Theorem 18.

For every $i\in T$ we choose $u_{i}^{\prime}\in V^{\prime}_{i}$ such that the set $\{u^{\prime}_{i}\mid i\in T\}$ is linearly independent. For $i\in T$ we denote $u_{i}:=\pi(u^{\prime}_{i})$ . For every $i\in S$ we choose $v_{i}\in V_{i}$ such that the set $\{v_{i}\mid i\in S\}$ is linearly independent. Let for $i\in S$ , $v^{\prime}_{i}$ be an element of $V_{i}^{\prime}$ such that $\pi(v^{\prime}_{i})=v_{i}$ .

Notice that the set $\{v^{\prime}_{i}\mid i\in S\}$ is also linearly independent, hence $S$ is coverable with respect to $V^{\prime}_{1},V^{\prime}_{2},\dots,V^{\prime}_{m}$ . By maximality of $T$ , $S\preceq T$ . If $S=T$ , then the theorem holds; hence, assume that $S\prec T$ (strictly less). Let us denote $t:=\max(T\setminus S)$ .

The theorem holds if $S\cup\{t\}=T$ . So, we assume that $S\cup\{t\}\neq T$ .

Claim 29.

$S\cup\{t\}$ is coverable with respect to $V^{\prime}_{1},V^{\prime}_{2},\dots,V^{\prime}_{m}$ .

Proof.

We will maintain the set of vectors $\{w^{\prime}_{i}\mid i\in S\cup\{t\}\}$ that satisfies the following properties:

1.

If $i\in S$ and $i<t$ , then $w^{\prime}_{i}=v_{i}^{\prime}$ ;
2.

$w^{\prime}_{t}=u^{\prime}_{t}$ ;
3.

If $i\in S$ and $i>t$ , then either $w^{\prime}_{i}=v_{i}^{\prime}$ , or $w^{\prime}_{i}=u_{i}^{\prime}$ ;
4.

The inequality $\dim\langle\{w_{i}\mid i\in S\cup\{t\}\}\rangle\geq|S|$ holds, where for all $i\in S\cup\{t\}$ , $w_{i}=\pi(w^{\prime}_{i})$ .

Initially assume that for all $i\in S$ and $i\neq t$ , $w^{\prime}_{i}:=v_{i}^{\prime}$ and $w^{\prime}_{t}=u^{\prime}_{t}$ . In other words the set $\{w_{i}^{\prime}\mid i\in S\cup\{t\}\}$ initially equals $\{v_{i}^{\prime}\mid i\in S\}\cup\{u^{\prime}_{t}\}$ . It is easy to verify that all properties above are satisfied.

While the set of vectors $\{w_{i}^{\prime}\mid i\in S\cup\{t\}\}$ is not linearly independent, we apply to this set some operation that will guarantee the satisfaction of all properties. We describe this operation below.

Since $\dim\{w_{i}\mid i\in S\cup\{t\}\}\geq|S|$ , we also have that $\dim\{w^{\prime}_{i}\mid i\in S\cup\{t\}\}\geq|S|$ . Since $\{w_{i}^{\prime}\mid i\in S\cup\{t\}\}$ is not linearly independent, $\dim\langle\{w^{\prime}_{i}\mid i\in S\cup\{t\}\}\rangle=|S|$ . Thus, there exists a unique non-empty set $I\subseteq S\cup\{t\}$ and non-zero elements $\{\alpha_{i}\in\mathbb{F}\}_{i\in I}$ such that $\sum_{i\in I}\alpha_{i}w^{\prime}_{i}=0$ ; and, thus, $\sum_{i\in I}\alpha_{i}w_{i}=0$ .

We claim that for all $j\in I$ , $j\geq t$ . Indeed, assume that for some $j\in I$ , $j<t$ , Then $\langle\{w_{i}\mid i\in S\cup\{t\}\setminus\{j\}\rangle$ contains $\langle\{w_{i}\mid i\in S\cup\{t\}\}\rangle$ whose dimension is at least $|S|$ , thus $S\cup\{t\}\setminus\{j\}$ is coverable with respect to $V_{1},\dots,V_{n}$ , but $S\prec S\cup\{t\}\setminus\{j\}$ ; contradiction with the maximality of $S$ .

It is impossible to have $w^{\prime}_{i}=u^{\prime}_{i}$ for all $i\in I$ since all $u^{\prime}_{i}$ are linearly independent. Thus, there exists $k\in I$ such that $w^{\prime}_{k}=v^{\prime}_{k}\neq u^{\prime}_{k}$ . Since $k\in I$ , $\{w_{i}\mid i\in S\cup\{t\}\}\in\langle\{w_{i}\mid i\in S\cup\{t\}\setminus\{k\}\rangle$ , by the dimension argument we get that the set $\{w_{i}\mid i\in S\cup\{t\}\setminus\{k\}\}$ is linearly independent. Let us change values $w^{\prime}_{k}:=u^{\prime}_{k}$ (and, correspondingly, $w_{k}:=u_{k}$ ). Note that $\dim\langle\{w_{i}\mid i\in S\cup\{t\}\}\rangle\geq\dim\langle\{w_{i}\mid i\in S% \cup\{t\}\setminus\{k\}\}\rangle=|S|$ , hence all the properties are satisfied for new values of $w_{i}^{\prime}$ .

We can’t apply this operation infinitely since the value $|\{i\in S\mid i>t,w_{i}^{\prime}\neq u_{i}^{\prime}\}|$ is decreased on every step. Hence, at some moment, we can’t apply the operation, which means that $\{w^{\prime}_{i}\mid i\in S\cup\{t\}\}$ is linearly independent and, thus, $S\cup\{t\}$ is coverable with respect to $V_{1}^{\prime},V_{2}^{\prime},\dots,V_{m}^{\prime}$ . $\hfill\vartriangleleft$

Consider the set $\{u_{i}\mid i\in T\}$ . Since $\{u^{\prime}_{i}\mid i\in T\}\in\langle\{u_{i}\mid i\in T\}\cup\{e\}\rangle$ , $\dim\langle\{u_{i}\mid i\in T\}\rangle\geq|T|-1$ .

If $\dim\langle\{u_{i}\mid i\in T\}\rangle=|T|$ , the set $\{u_{i}\mid i\in T\}$ is linearly independent, we get a contradiction with maximality of $S$ since $S\prec T$ . Thus, $\dim\langle\{u_{i}\mid i\in T\}\rangle=|T|-1$ . Let us fix some $\ell\in T$ such that $u_{\ell}$ is in the span of $u_{i}$ for $i\in T\setminus\{\ell\}$ . In this case $\{u_{i}\mid i\in T\setminus\{\ell\}\}$ is linearly independent, thus $T\setminus\{\ell\}$ is coverable with respect to $V_{1},\dots,V_{m}$ .

Claim 30.

$t\leq\ell$

Proof.

The set $T\setminus\{\ell\}$ is coverable with respect to $V_{1},\dots,V_{m}$ . Since $S$ is the maximal coverable, $T\setminus\{\ell\}\preceq S$ . It implies that $t\leq\ell$ . $\hfill\vartriangleleft$

Claim 31.

$t\neq\ell$

Proof.

Assume that $t=\ell$ . By Claim 29 the set $S\cup\{\ell\}$ is coverable with respect to $V_{1}^{\prime},\dots,V_{n}^{\prime}$ . Then $S\cup\{\ell\}\preceq T$ . Since $S\cup\{\ell\}=S\cup\{t\}\neq T$ , $S\cup\{\ell\}\prec T$ . Let $h=\max(T\setminus(S\cup\{\ell\})$ . It is straightforward that $h<t=\ell$ . By the definition of $h$ we get that $S\prec\{i\in T\mid i\geq h,i\neq\ell\}$ , but the set $\{u_{i}\mid i\in T,i\geq h,i\neq\ell\}$ is linearly independent since it is a subset of $\{u_{i}\mid i\in T\setminus\{\ell\}\}$ . This contradicts the maximality of $S$ . $\hfill\vartriangleleft$

The last two claims imply $t<\ell$ .

Claim 29 implies that $S\cup\{t\}\preceq T$ . If $S\cup\{t\}\neq T$ , then $S\cup\{t\}\prec T$ . Let $t^{\prime}=\max(T\setminus(S\cup\{t\})$ .

Let $J=(\{t^{\prime}+1,\dots,m\}\setminus\{t,\ell\})\cap T$ . The set $J\cup\{t^{\prime},t\}$ is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ since $\{u_{j}\mid j\in T\setminus\{\ell\}\}$ is linearly independent. The set $J\cup\{\ell\}$ is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ since $v_{i}$ for $i\in S$ are linearly independent and $t<\ell$ . The sets $J\cup\{\ell,t\}$ and $J\cup\{\ell,t^{\prime}\}$ are not coverable with respect to $V_{1},V_{2},\dots,V_{m}$ since it would contradict maximality of $S$ . The following lemma (Lemma 32) implies that such a situation is impossible. We get a contradiction with our assumption that the theorem does not hold. $\hfill\blacktriangleleft$

Lemma 32.

Let $J\subseteq[m]$ , $t,t^{\prime}$ and $\ell$ be different elements from $[m]\setminus J$ . Assume that $J\cup\{\ell\}$ is coverable with respect to $V_{1},V_{2},\dots,V_{m}$ but $J\cup\{\ell,t\}$ and $J\cup\{\ell,t^{\prime}\}$ are not coverable. Then $J\cup\{t^{\prime},t\}$ is not coverable.

Proof.

Asume for a sake of contradiction that $J\cup\{t^{\prime},t\}$ is coverable.

For any set $A\subseteq[m]$ we will use the notation $U(A):=\langle\bigcup_{i\in A}V_{i}\rangle$ .

By Theorem 17 since $J\cup\{\ell,t\}$ is not coverable, there exists $A\subseteq J\cup\{\ell,t\}$ such that $\dim U(A)<|A|$ . Since $J\cup\{\ell\}$ and $J\cup\{t^{\prime},t\}$ are coverable, both $\ell$ and $t$ belong $A$ . Let us denote $A^{\prime}:=A\setminus\{\ell,t\}$ .

Since $J\cup\{t^{\prime},t\}$ is coverable, $\dim U(A^{\prime}\cup\{t\})\geq|A^{\prime}|+1$ . Since $J\cup\{\ell\}$ is coverable, $\dim U(A^{\prime}\cup\{\ell\})\geq|A^{\prime}|+1$ . But we know that $\dim U(A^{\prime}\cup\{t,\ell\})\leq|A|^{\prime}+1$ , hence $\dim U(A^{\prime}\cup\{t\})=\dim U(A^{\prime}\cup\{\ell\})=\dim U(A^{\prime}% \cup\{t,\ell\})=|A^{\prime}|+1$ . The last equality implies that $V_{\ell}\subseteq U(A^{\prime}\cup\{t\})$ and $V_{t}\subseteq U(A^{\prime}\cup\{\ell\})$ .

Analogously using that $J\cup\{\ell,t^{\prime}\}$ is not coverable we get that there exists $B^{\prime}\subseteq[m]\setminus\{\ell,t^{\prime}\}$ such that $\dim U(B^{\prime}\cup\{t^{\prime}\})=\dim U(B^{\prime}\cup\{\ell\})=\dim U(B^{% \prime}\cup\{t^{\prime},\ell\})=|B^{\prime}|+1$ . This equality implies that $V_{\ell}\subseteq U(B^{\prime}\cup\{t^{\prime}\})$ and $V_{t^{\prime}}\subseteq U(B^{\prime}\cup\{\ell\})$ .

By our assumption, the set $J\cup\{t^{\prime},t\}$ is coverable. So, we may estimate

|A^{\prime}\cup B^{\prime}|+2\leq\dim U(A^{\prime}\cup B^{\prime}\cup\{t,t^{% \prime}\})\leq\dim U(A^{\prime}\cup B^{\prime}\cup\{t,t^{\prime},\ell\})=\\ \dim U(A^{\prime}\cup B^{\prime}\cup\{t^{\prime},\ell\})=\dim U(A^{\prime}\cup B% ^{\prime}\cup\{\ell\})=\\ \dim U(A^{\prime}\cup\{\ell\})+\dim U(B^{\prime}\cup\{\ell\})-\dim U((A^{% \prime}\cap B^{\prime})\cup\{\ell\})\leq\\ |A^{\prime}|+1+|B^{\prime}|+1-(|A^{\prime}\cap B^{\prime}|+1)=|A^{\prime}\cup B% ^{\prime}|+1,

and get a contradiction. In the first equality, we explore that $V_{t}\subseteq U(A^{\prime}\cup\{\ell\})$ . In the second equality we explore that $V_{t^{\prime}}\subseteq U(B^{\prime}\cup\{\ell\})$ . In the third equality we use that $\dim\langle X\cup Y\rangle=\dim\langle X\rangle+\dim\langle Y\rangle-\dim(% \langle X\rangle\cap\langle Y\rangle)$ . In the last inequality we used the known values of $\dim U(A^{\prime}\cup\{\ell\})$ and $\dim U(B^{\prime}\cup\ell)$ and that $J\cup\{\ell\}$ is coverable. $\hfill\blacktriangleleft$

3 Preliminary knowledge on resolution over parities and lifting

3.1 Resolution and resolution over parities

Here and after, all scalars are from the field $\mathbb{F}_{2}$ . Let $X$ be a set of variables that take values in $\mathbb{F}_{2}$ . A linear form in variables from $X$ is a homogeneous linear polynomial over $\mathbb{F}_{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\mathbb{F}_{2}$ for all $i\in[n]$ . A linear equation is an equality $f=a$ , where $f$ is a linear form and $a\in\mathbb{F}_{2}$ .

A linear clause is a disjunction of linear equations: $\bigvee_{i=1}^{t}(f_{i}=a_{i})$ . Notice that over $\mathbb{F}_{2}$ a linear clause $\bigvee_{i=1}^{t}(f_{i}=a_{i})$ may be represented as the negation of a linear system: $\lnot\bigwedge_{i=1}^{t}(f_{i}=a_{i}+1)$ .

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},\dots,f_{t}\}$ . The same notation we use for linear systems: if $\Psi$ is a $\mathbb{F}_{2}$ -linear system, $L(\Psi)$ denotes the set of all linear forms from $\Psi$ .

Let $\varphi$ be an unsatisfiable CNF formula. A refutation of $\varphi$ in the proof system $\mathrm{Res}(\oplus)$ [19] is a sequence of linear clauses $C_{1},C_{2},\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 $\varphi$ or is obtained from previous clauses by one of the following inference rules:

$\blacksquare$

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

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

The width (sometimes the term rank is used for the same notion) of a $\mathrm{Res}(\oplus)$ refutation is the maximal rank of the negation of a linear clause from the refutation.

A $\mathrm{Res}(\oplus)$ refutation of $\varphi$ is a tree-like if it can be arranged as a tree, where leaves correspond clauses of $\varphi$ and any clause in the interior node is obtained by a rule from the clauses in its children.

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.

A resolution refutation of a formula $\varphi$ is a special case of a $\mathrm{Res}(\oplus)$ refutation, where all linear clauses are plain (i.e., disjunctions of literals). For resolution refutations, we also use the notions of width and depth that correspond to the same notions in $\mathrm{Res}(\oplus)$ refutations.

3.2 Lifting of formulas via gadget

For every CNF formula $\Phi$ with variables $Y=\{y_{1},y_{2},\dots,y_{m}\}$ and every Boolean function $g\colon\{0,1\}^{\ell}\to\{0,1\}$ we define a CNF formula $\Phi\circ g$ with variables $X=\{x_{i,j}\mid i\in[m],j\in[\ell]\}$ representing $\Phi(g(x_{1,1},x_{1,2},\dots,x_{1,\ell}),g(x_{2,1},x_{2,2},\dots,x_{2,\ell}),% \dots,g(x_{m,1},x_{m,2},\dots,x_{m,\ell}))$ (i.e. we substitute to every variable of $\Phi$ the function $g$ applied to $\ell$ fresh variables). Let $\Phi=\bigwedge\limits_{i\in I}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 cannonical CNF formula representing $g(x_{i,1},x_{i,2},\dots,x_{i,\ell})$ which has $\ell$ variables in every clause and by $(\lnot y_{i})\circ g$ the cannonical CNF formula representing $\lnot g(x_{i,1},x_{i,2},\dots,x_{i,\ell})$ which has $\ell$ variables in every clause. Let $C_{i}=l_{i,1}\lor l_{i,2}\lor\dots\lor 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\lor l_{i,2}\circ g\lor\dots\lor l_{i,n_{i}}\circ g$ as follows: $C_{i}\circ g$ consists of all clauses of the form $D_{1}\lor D_{2}\lor\dots\lor D_{n_{i}}$ , where $D_{j}$ is a clause of $l_{i,j}\circ g$ for all $j\in[m_{i}]$ . And $\Phi\circ g:=\bigwedge\limits_{i\in I}C_{i}\circ g$ .

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

Sometimes, we will identify subsets of $[m]$ with corresponding subsets of $Y$ . It is especially convenient to use such correspondence for the notions of support, 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 $\hat{\rho}$ the partial assignment on the set of variables $Y$ such that $\hat{\rho}(y_{i})=g(\rho(x_{i,1},x_{i,2},\dots,x_{i,\ell}))$ (here we assume that if the right-hand side is undefined, then the left-hand side is also undefined).

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

Lemma 33 ([7, 3]).

Let $\Psi$ be a satisfiable linear system in the lifted variables $X$ . Let $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a $1$ -stifling gadget. Suppose

$\blacksquare$

$\sigma$ is a full assignment to lifted variables $X$ satisfying $\Psi$ .
$\blacksquare$

$\pi$ is a full assignment to unlifted variables $Y$ such that $\pi|_{\mathop{\mathrm{Cl}}(L(\Psi))}=\hat{\sigma}|_{\mathop{\mathrm{Cl}}(L(% \Psi))}$ .

Then there exists a full assignment $\tau$ to the lifted variables $X$ such that $\tau$ satisfies $\Psi$ and

\hat{\tau}=\pi.

Lemma 34 ([3]).

Let $\Psi$ be a satisfiable linear system in the lifted variables $X$ . Let $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a $1$ -stifling gadget. Suppose there exists a full assignment $\sigma$ to lifted variables $X$ satisfying $\Psi$ such that $\hat{\sigma}|_{\mathop{\mathrm{Cl}}(L(\Psi))}$ does not falsify any clause of $\varphi$ . Then, $\Psi$ does not contradict any clause of $\varphi\circ g$ .

4 Bounded-width lifting theorem

In this section, we present our first application of amortized closure. Namely, we give an easy proof of the lifting theorem that extends Theorem 2 recently obtained by Chattopadhyay and Dvorak [10]. In Subsection 4.1, we define bounded-width games characterizing resolution depth and tree-like $\mathrm{Res}(\oplus)$ size. In Subsection 4.2, we state and prove our lifting theorem.

4.1 Bounded-width games for resolution and resolution over parities

Consider the following bounded-width Prover-Adversary game [6, 15]. The game is defined for an unsatisfiable CNF formula $\varphi$ and integer parameter $w\geq 1$ . During the game, players save a partial assignment $\rho$ . Initially, $\rho$ is empty. Every her move, Prover has several possibilities: 1) Forget: change $\rho$ to $\rho^{\prime}$ if $\rho^{\prime}\subseteq\rho$ ; 2) Query: if $|\rho|<w$ , Prover can choose a variable $x$ not from domain of $\rho$ and Adversary chooses $a\in\{0,1\}$ and changes $\rho:=\rho\cup\{x:=a\}$ . For every move, Adversary earns a coin. The game ends if $\rho$ falsifies a clause of $\varphi$ .

Lemma 35 (Lemma 6 from [6]).

An unsatisfiable CNF formula $\varphi$ has resolution refutation of width $w$ and depth $d$ if and only if Prover has a strategy in the game for $\varphi$ with the parameter $w+1$ that guarantees that Adversary earns at most $d$ coins for any his behavior.

Now, we introduce a bounded-width $\mathrm{Res}(\oplus)$ -Prover-Delayer game. This game is also defined on an unsatisfiable formula $\varphi$ and a parameter $w$ . The players save a linear system $\Psi$ , which is initially empty. Prover has several possibilities for every her move: 1) Forget: change the system $\Psi$ to any system $\Psi^{\prime}$ such that $\Psi$ semantically implies $\Psi^{\prime}$ . 2)Query: if $\mathrm{rk}(\Psi)<w$ , Prover can choose a linear form $f$ . Delayer can either choose a value $a\in\{0,1\}$ and change $\Psi$ to $\Psi\land(f=a)$ or report $*$ , in the second case Prover chooses $a\in\{0,1\}$ by herself and update $\Psi$ to $\Psi\land(f=a)$ . Delayer earns a coin for each answer $*$ . The game ends if the system $\Psi$ contradicts a clause of $\varphi$ .

Lemma 36.

If Delayer has a strategy in the game defined for an unsatisfiable formula $\varphi$ with parameter $w+1$ that guarantees him to earn at least $d$ coins, then the size of any tree-like $\mathrm{Res}(\oplus)$ refutation of $\varphi$ of width at most $w$ has size at least $2^{d}$ .

Proof.

Consider a tree-like $\mathrm{Res}(\oplus)$ refutation $\Pi$ of $\varphi$ with width at most $w$ . For a node $v$ of the proof tree, we denote by $C_{v}$ a linear clause that labels $v$ . Based on Delayer’s strategy, we define a random path from the root to a leaf of $\Pi$ . We start a path in the root of the proof tree that corresponds to an empty clause. To define a path we will play the bounded-width game on the formula $\varphi$ . The linear system in the game always equals the negation of the current clause. At the root, we have the empty linear system.

If a current node $u$ has only one child $v$ (i.e., it corresponds to the weakening rule), we move to this child $v$ . Since $C_{v}$ semantically implies $C_{u}$ , $\lnot C_{u}$ semantically implies $\lnot C_{v}$ . In the game, we change a linear system $\lnot C_{u}$ to its semantical implication $\lnot C_{v}$ . It is easy to see that $\mathrm{rk}(\lnot C_{v})\leq\mathrm{rk}(\lnot C_{u})$ .

Assume that $C_{u}$ results from the resolution rule applied to $C_{u_{0}}$ and $C_{u_{1}}$ , and $f_{u}$ is the resolved linear form. In this case $C_{u_{0}}=(f_{u}=0)\lor D_{0}$ and $C_{u_{1}}=(f_{u}=1)\lor D_{1}$ and $C_{u}=D_{0}\lor D_{1}$ . Prover asks for the value of the linear form $f_{u}$ . It is a legal step since $\mathrm{rk}(\lnot C_{u})\leq w$ . If Delayer answers $*$ , we choose $a\in\{0,1\}^{*}$ at random. Otherwise, $a\in\{0,1\}$ is the value chosen by Delayer. We move to $u_{1-a}$ . In the game, we first get a linear system $(f_{u}=a)\lor\lnot C_{u}$ and then change it to its semantical implication $\lnot C_{1-a}$ . With probability $1$ we finish the path in a leaf $\ell$ of the proof tree. $C_{\ell}$ is a clause of $\varphi$ , and thus $\lnot C_{\ell}$ contradicts a clause of $\varphi$ . By the property of Delayer’s strategy, Delayer earns at least $d$ coins at that moment. Thus, for every leaf, the probability that the path finishes in this leaf is at most $2^{-d}$ . Hence the number of leaves in the proof tree is at least $2^{d}$ . $\hfill\blacktriangleleft$

4.2 Proof of lifting theorem

Theorem 37.

Let $\varphi$ be an unsatisfiable CNF formula and $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a 1-stiffling gadget. Assume that $\varphi\circ g$ has a tree-like $\mathrm{Res}(\oplus)$ refutation of rank $w$ and size $2^{d}$ . Then $\varphi$ has a resolution refutation of width $w$ and depth $d$ .

Proof.

Proof by contradiction. Assume that $\varphi$ does not have a resolution refutation of width $w$ and depth $d$ . Then, by Lemma 35, there is a strategy of Adversary in the first game for the formula $\varphi$ and the parameter $w+1$ that guarantees him to earn at least $d+1$ coins. Using this strategy, we construct the strategy of Delayer in the second game for the formula $\varphi\circ g$ and the parameter $w+1$ .

Let $\Psi$ denote the current linear system in the second game; $\Psi$ is a linear system in the lifted variables. Let $\rho$ denote the current partial assignment in the first game; it assigns values to unlifted variables. We maintain the following invariant: $\rho$ is defined on $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ and $\Psi$ has a solution $\pi$ such that $\hat{\pi}$ coincides with $\rho$ on $\widetilde{\mathop{\mathrm{Cl}}}(L(\Phi))$ . Initially, $\Psi$ is the empty system, $\rho$ is the empty assignment, and the invariant holds for any $\pi$ . Consider Prover’s different types of moves in the second game.

First, assume that Prover makes a query and chooses a linear form $f$ .

1.

If $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi)\cup\{f\})=\widetilde{\mathop{\mathrm{% Cl}}}(L(\Psi))$ . Delayer chooses $a$ equals the value of $f$ on $\pi$ . The values $\rho$ and $\pi$ remain unchanged.
2.

If $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi)\cup\{f\})\neq\widetilde{\mathop{% \mathrm{Cl}}}(L(\Psi))$ , then by Theorem 21, $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi)\cup\{f\})=\widetilde{\mathop{\mathrm{% Cl}}}(L(\Psi))\cup\{j\}$ for some $j\notin\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ . Delayer reports $*$ . We ask the value of the variable $y_{j}$ in the first game and let $a_{j}$ be the answer. We update $\rho:=\rho\cup\{y_{j}:=a_{j}\}$ . Let Prover choose a value $a\in\{0,1\}$ in the second game. By Lemma 28, $\mathop{\mathrm{Cl}}(L(\Psi)\cup\{f\})=\mathop{\mathrm{Cl}}(L(\Psi))$ . Since $\mathop{\mathrm{Cl}}(L(\Psi)\cup\{f\})=\mathop{\mathrm{Cl}}(L(\Psi))\subseteq% \widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ , Lemma 33 implies that there is a solution $\tau$ of $\Psi\land(f=a)$ such that $\hat{\tau}$ coincide with $\rho$ on $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ . We update $\pi:=\tau$ .

Now assume that Prover forgets, i.e. she changes $\Psi$ to $\Psi^{\prime}$ , where $\Psi$ semantically implies $\Psi^{\prime}$ . Then we restrict $\rho$ on the set of variables $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ . Since $L(\Psi^{\prime})\subseteq\langle L(\Psi)\rangle$ , by Corollary 22 $\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi^{\prime}))\subseteq\widetilde{\mathop{% \mathrm{Cl}}}(L(\Psi))$ .

Assume that the invariant holds and $\rho$ does not falsify any clause of $\varphi$ . By Lemma 26, $\mathop{\mathrm{Cl}}(L(\Psi))\subseteq\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))$ , hence by Lemma 34, $\Psi$ does not contradict a clause of $\varphi\circ g$ .

In the first game, Adversary can earn at least $d+1$ coins. By the construction of the strategy, each time Adversary earns a coin, Delayer also earns a coin. Hence, Delayer, using the described strategy, can earn at least $d+1$ coins. And by Lemma 36, this contradicts the assumption of the theorem. $\hfill\blacktriangleleft$

5 Lower bound for depth- $\Omega(n\log n)$ $\mathrm{Res}(\oplus)$

In this section, we describe how to prove an exponential lower for depth- $\Omega(n\log n)$ $\mathrm{Res}(\oplus)$ . In Subsection 5.1, we present the key lemma utilizing the notion of amortized closure that we will use to improve the result by [3]. In Subsections 5.2 and 5.3, we describe how to modify the proof by [3] to improve it using the key lemma.

5.1 Key lemma

Lemma 38.

Let $\Phi$ and $\Psi$ be two linear systems in variables $X=\{x_{i,j}\mid i\in[m],j\in[\ell]\}$ . Let $\pi$ be a partial assignment defined on $\{x_{i,j}\mid i\in[\mathop{\mathrm{Cl}}(L(\Phi))],j\in[\ell]\}$ . Let $\Sigma$ consist of all solutions $\sigma$ of $\Phi$ such that $\sigma$ extends $\pi$ . Assume that $\Sigma\neq\emptyset$ . Let $\tau$ be a random element of $\Sigma$ . Then $\Pr[\tau\mbox{ satisfies }\Psi]\leq 2^{|\widetilde{\mathop{\mathrm{Cl}}}(L(% \Phi))|-|\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))|}$ .

Proof.

By the definition of the closure, the set of linear form $L(\Phi|_{\pi})$ is safe. Hence, by Theorem 9, there exists a basis in the set of columns of the matrix of $\Phi|_{\pi}$ such that for every block, the basis contains at most one column corresponding to this block. Let $Z\subseteq X$ be the set of variables corresponding to the basis elements. Since $\Sigma\neq\emptyset$ , the system $\Phi|_{\pi}$ is satisfiable. Hence, the system $\Phi|_{\pi}$ can be equivalently rewritten as the system of $|Z|$ equations, each of them linearly expresses the corresponding variable from $Z$ from variables $X\setminus Z\setminus\mathrm{Dom}(\pi)$ . Let us denote this representation by $\Phi_{\pi}^{\prime}$ .

A random solution of $\Phi|_{\pi}$ has the following structure: we take at random values of all variables $X\setminus Z\setminus\mathrm{Dom}(\pi)$ , and, then the values of variables from $Z$ are uniquely determined by the system $\Phi_{\pi}^{\prime}$ . Thus, the following statement holds.

Claim 39.

Let $H$ be a satisfiable linear system in the variables $X\setminus Z\setminus\mathrm{Dom}(\pi)$ . Then $\Pr[\tau\mbox{ satisfies }H]=2^{-\mathrm{rk}(H)}$ .

Let $\Pi$ be the following linear system: $\bigwedge_{j\in[\ell],i\in[\mathop{\mathrm{Cl}}(L(\Phi))]}x_{i,j}=\pi(x_{i,j})$ .

Notice that the linear system $\Phi\land\Pi$ is semantically equivalent to the system $\Phi|_{\pi}\land\Pi$ that is equivalent to the system $\Phi^{\prime}_{\pi}\land\Pi$ .

The system $\Pi\land\Phi_{\pi}^{\prime}$ sets variables from $\mathrm{Dom}(\pi)$ to constants and expresses the variables from $Z$ from the variables $X\setminus Z\setminus\mathrm{Dom}(\pi)$ . Let $\Psi^{\prime}$ denote the linear system $\Psi$ where we substitute for all variables from $\mathrm{Dom}(\pi)\cup Z$ their expressions given by the system $\Pi\land\Phi_{\pi}^{\prime}$ . So $\Psi^{\prime}$ is a linear system in the variables $X\setminus Z\setminus\mathrm{Dom}(\pi)$ .

Let $\Psi^{\prime\prime}$ be the maximal set of linearly independent equations from $\Psi^{\prime}$ .

\Pr[\tau\mbox{ satisfies }\Psi]=\Pr[\tau\mbox{ satisfies }\Psi\land\Pi\land% \Phi^{\prime}_{\pi}]=\Pr[\tau\mbox{ satisfies }\Psi^{\prime}\land\Pi\land\Phi^% {\prime}_{\pi}]\\ =\Pr[\tau\mbox{ satisfies }\Psi^{\prime\prime}\land\Pi\land\Phi^{\prime}_{\pi}% ]=\Pr[\tau\mbox{ satisfies }\Psi^{\prime\prime}]\mathop{=}\limits^{\mbox{% \small(Claim\leavevmode\nobreak\ \ref{probability-in-pure-variables})}}2^{-% \mathrm{rk}(\Psi^{\prime\prime})}

|\widetilde{\mathop{\mathrm{Cl}}}(L(\Psi))|\mathop{\leq}\limits^{\mbox{\small(% Cor.\leavevmode\nobreak\ \ref{cor:acl-is-monotone})}}|\widetilde{\mathop{% \mathrm{Cl}}}(L(\Pi\land\Phi^{\prime}_{\pi}\land\Psi))|\mathop{=}\limits^{% \mbox{\small(Lem.\leavevmode\nobreak\ \ref{acl-basis-inv})}}|\widetilde{% \mathop{\mathrm{Cl}}}(L(\Pi\land\Phi^{\prime}_{\pi}\land\Psi^{\prime\prime}))|% \mathop{\leq}\limits^{\mbox{\small(Cor.\leavevmode\nobreak\ \ref{cor:acl-is-% monotone})}}\\ |\widetilde{\mathop{\mathrm{Cl}}}(L(\Pi\land\Phi\land\Psi^{\prime\prime}))|% \mathop{=}\limits^{\mbox{\small(Lem.\leavevmode\nobreak\ \ref{amortised-via-% plain})}}\\ |\mathop{\mathrm{Cl}}(L(\Phi))|+|\widetilde{\mathop{\mathrm{Cl}}}\left(L(\Pi[% \setminus\mathop{\mathrm{Cl}}(L(\Phi))])\cup L(\Phi[\setminus\mathop{\mathrm{% Cl}}(L(\Phi))])\cup L(\Psi^{\prime\prime}[\setminus\mathop{\mathrm{Cl}}(L(\Phi% ))])\right)|=\\ |\mathop{\mathrm{Cl}}(L(\Phi))|+|\widetilde{\mathop{\mathrm{Cl}}}(L(\Phi[% \setminus\mathop{\mathrm{Cl}}(L(\Phi))])\cup L(\Psi^{\prime\prime}))|\mathop{% \leq}\limits^{\mbox{\small(Th.\leavevmode\nobreak\ \ref{acl-continious})}}\\ |\mathop{\mathrm{Cl}}(L(\Phi))|+|\widetilde{\mathop{\mathrm{Cl}}}(L(\Phi)[% \setminus\mathop{\mathrm{Cl}}(L(\Phi))]))|+\mathrm{rk}(\Psi^{\prime\prime})% \mathop{=}\limits^{\mbox{\small(Lem.\leavevmode\nobreak\ \ref{amortised-via-% plain})}}|\widetilde{\mathop{\mathrm{Cl}}}(L(\Phi))|+\mathrm{rk}(\Psi^{\prime% \prime}).

So we get, $\Pr[\tau\mbox{ satisfies }\Psi]=2^{-\mathrm{rk}(\Psi^{\prime\prime})}\leq 2^{|% \widetilde{\mathop{\mathrm{Cl}}}(L(\Phi))|-|\widetilde{\mathop{\mathrm{Cl}}}(L% (\Psi))|}$ . $\hfill\blacktriangleleft$

5.2 Random-walk theorem

The main technical tool used in [3] in proving the lower bound for bounded-depth $\mathrm{Res}(\oplus)$ is the random-walk theorem.

Let $\varphi$ be a CNF formula and $\mathcal{A}$ be a set consisting of partial assignments for variables of $\varphi$ . We assume that $\mathcal{A}$ has two properties:

$\blacksquare$

$\mathcal{A}$ is closed under restrictions: if for every $\rho\in\mathcal{A}$ for every $\sigma\subseteq\rho$ , $\sigma\in\mathcal{A}$ .
$\blacksquare$

For every $\sigma\in\mathcal{A}$ , $\sigma$ does not falsify any clause of $\varphi$ .

$(\varphi,\mathcal{A})$ -games of Prover and Delayer with starting position $\rho_{0}\in\mathcal{A}$

In this game, two players, Prover and Delayer, maintain a partial assignment $\rho$ for variables of $\varphi$ that initially equals $\rho_{0}$ . On every move, Prover chooses a variable $x$ , and Delayer has two options:

$\blacksquare$

Delayer can earn a white coin and reports $*$ . Then, Prover chooses a Boolean value $a$ of $x$ .
$\blacksquare$

Delayer can earn a white coin and pay a black coin to choose a Boolean value $a$ of $x$ by himself.

The current assignment $\rho$ is updated: $\rho:=\rho\cup\{x:=a\}$ . The game ends when $\rho\notin\mathcal{A}$ .

Delayer’s strategy is called linearly described if Delayer can see only the set of requested variables and he does not know the values of the variables chosen by Prover and even by himself before. When he chooses a value by himself, he chooses a $\mathbb{F}_{2}$ -affine function from the values of previous variables, and the result of this function is used as a value chosen by Delayer. For a more detailed definition of linearly described strategies, we refer to [3].

Theorem 40 (Theorem 4.3 from [3]).

Let $\varphi$ be an unsatisfiable CNF formula. Let $\mathcal{A}$ be a set of partial assignments for $\mathrm{Vars}(\varphi)$ such that $\mathcal{A}$ is closed under restrictions and for any $\sigma\in\mathcal{A}$ , $\sigma$ does not falsify any clause of $\varphi$ . Assume that in the $(\varphi,\mathcal{A})$ -game, Delayer has a linearly described strategy with start position $\rho_{0}\in\mathcal{A}$ that guarantees him to earn $w$ white coins while paying at most $c$ black coins. Let $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a 2-stifling gadget. Consider a $\mathrm{Res}(\oplus)$ refutation of $\varphi\circ g$ .Let $C_{0}$ be a linear clause from this refutation. Assume that $\mathop{\mathrm{Cl}}(L(C_{0}))=\mathrm{Dom}(\rho_{0})$ and there is a solution $\tau$ of $\lnot C_{0}$ such that $\hat{\tau}$ extends $\rho_{0}$ . Let $\Sigma$ be the set of all full assigmnets $\pi$ such that $\pi$ satisfies $\lnot C_{0}$ and $\hat{\pi}$ extends $\rho_{0}$ . Let $t$ be integer number such that $t\leq w-|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{0}))|+|\rho_{0}|$ . Consider a random full assignment $\sigma\in\Sigma$ and make $t$ steps in the refutation from $C_{0}$ according to $\sigma$ : each time we go from a linear clause to its premise falsifying by $\sigma$ , and we count only applications of resolution rules (if we reach an initial clause earlier than in $t$ steps, we stay there). Assume that we stop in a node labeled with a linear clause $C$ . Then $\hat{\sigma}|_{\mathop{\mathrm{Cl}}(L(C))}\in\mathcal{A}$ with probability at least $2^{-c(\ell-1)}$ .

The only difference between Theorem 40 and Theorem 4.3 from [3] is that the inequality $t\leq w-|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{0}))|+|\rho_{0}|$ that was slightly stronger $t\leq w-|\mathrm{rk}(\lnot C_{0})|+|\rho_{0}|$ in Theorem 4.3 from [3]. It is easy to see that the proof from [3] works with the weaker inequality as well. This is because this inequality was only used to show that if a linear system $F$ has type $\lnot C_{0}\land H$ , where $H$ consists of at most $t$ equations, then $|\mathop{\mathrm{Cl}}(L(F))|\leq w+|\rho_{0}|$ . Using the weaker inequality $|\mathop{\mathrm{Cl}}(L(F))|$ can be estimated as follows: $|\mathop{\mathrm{Cl}}(L(F))|\mathop{\leq}\limits^{\mbox{\small(Lem.\leavevmode% \nobreak\ \ref{lem:cl-subseteq-acl})}}|\widetilde{\mathop{\mathrm{Cl}}}(L(F))|% \mathop{\leq}\limits^{\mbox{\small(Th.\leavevmode\nobreak\ \ref{acl-continious% })}}|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{0})|+t\leq w+|\rho_{0}|$ .

5.3 Size vs depth tradeoff

Theorem 41 (cf. Theorem 8.1 from [3]).

Let $\varphi$ be an unsatisfiable CNF formula. Let $\mathcal{A}$ be a set of partial assignments for $\mathrm{Vars}(\varphi)$ such that for any $\sigma\in\mathcal{A}$ , $\sigma$ does not falsify any clause of $\varphi$ and $\mathcal{A}$ is closed under restrictions (i.e., if $\rho\in\mathcal{A}$ and $\tau\subseteq\rho$ , then $\tau\in\mathcal{A}$ ). Assume that there are integers $t$ and $c$ such that for every $\rho\in\mathcal{A}$ such that $|\rho|<t$ , in the $(\varphi,\mathcal{A})$ -game with start position $\rho$ there is a linearly described strategy of Delayer that guarantees him to earn at least $t-|\rho|$ white coins while paying at most $c$ black coins. Let $g\colon\{0,1\}^{\ell}\to\{0,1\}$ be a 2-stifling gadget. Then any $\mathrm{Res}(\oplus)$ refutation of $\varphi\circ g$ has either size at least $2^{c}$ or depth at least $\frac{t^{2}}{4c\ell}$ .

Proof.

We say that a linear clause $C$ in lifted variables is $\mathcal{A}$ -good if there is a solution $\tau$ of $\lnot C$ such that $\hat{\tau}|_{\mathop{\mathrm{Cl}}(L(C))}\in\mathcal{A}$ .

Consider a $\mathrm{Res}(\oplus)$ refutation of $\varphi\circ g$ and denote is by $\Pi$ .

Claim 42.

Assume that $\Pi$ contains an $\mathcal{A}$ -good linear clause $C_{0}$ such that $|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{0}))|\leq r$ , where $r<t$ . Let $S_{t-r}(C_{0})$ denote the set of all $\mathcal{A}$ -good clauses $C$ such that there is a path from $C_{0}$ to $C$ of length $t-r$ in the branching program associated with $\Pi$ . Assume that for every $C\in S_{t-r}(C_{0})$ , $|\widetilde{\mathop{\mathrm{Cl}}}(L(C))|\geq r+c\ell$ holds. Then, the size of the refutation $\Pi$ is at least $2^{c}$ .

Proof.

Since $C_{0}$ is $\mathcal{A}$ -good, there is a solution $\tau_{0}$ of $\lnot C_{0}$ such that $\hat{\tau}_{0}|_{\mathop{\mathrm{Cl}}(L(C))}\in\mathcal{A}$ . Let us denote $\rho_{0}:=\hat{\tau}_{0}|_{\mathop{\mathrm{Cl}}(L(C_{0}))}$ . Then $|\rho_{0}|=|\mathop{\mathrm{Cl}}(L(C_{0}))|\leq|\widetilde{\mathop{\mathrm{Cl}% }}(L(C_{0}))|\leq r$ . By the conditions of the theorem, there is a linearly described strategy of Delayer in the $(\varphi,\mathcal{A})$ -game with starting position $\rho_{0}$ that guarantees him to earn $t-|\rho_{0}|$ white coins while paying at most $c$ black coins.

Let $\Sigma$ be the set of all assignments $\pi$ such that $\pi$ satisfies $\lnot C_{0}$ and $\hat{\pi}|_{\mathop{\mathrm{Cl}}(L(C_{0}))}=\rho_{0}$ . Since $\tau_{0}\in\Sigma$ , $\Sigma\neq\emptyset$ .

Consider a random assignment $\sigma\in\Sigma$ and make $t-r$ steps in the refutation $\Pi$ from $C_{0}$ according to $\sigma$ : each time we go from a linear clause to its premise falsifying by $\sigma$ , and we count only applications of resolution rules. Notice that $t-r\leq(t-|\rho_{0}|)+|\rho_{0}|-|\widetilde{\mathop{\mathrm{Cl}}}(L(C_{0}))|$ . Let $C$ be the linear clause at the end of the path. By Theorem 40, with probability at least $2^{-(\ell-1)c}$ , $C$ is $\mathcal{A}$ -good. By Lemma 34, $C$ is not a clause of $\phi\circ g$ , hence, $C\in S_{t-r}(C_{0})$ . Thus, $|\widetilde{\mathop{\mathrm{Cl}}}(L(C))|\geq r+c\ell$ .

If $\Psi$ is a satisfiable linear system such that $|\widetilde{\mathop{\mathrm{Cl}}}(\Psi)|\geq r+c\ell$ , then by Lemma 38, $\Pr[\mbox{$\sigma$ satisfies $\Psi$}]\leq 2^{-c\ell}$ . Hence, the refutation contains at least $2^{c}$ clauses $C$ such that $|\widetilde{\mathop{\mathrm{Cl}}}(L(C))\geq r+c\ell$ . $\hfill\vartriangleleft$

Let $D_{0}$ denote the empty clause from $\Pi$ . If for every $\mathcal{A}$ -good clause $C$ such that there is a path from $D_{0}$ to $C$ of length $t$ , $|\widetilde{\mathop{\mathrm{Cl}}}(L(C))|\geq c\ell$ , then by Claim 42, the size of the refutation $\Pi$ is at least $2^{c}$ . Otherwise, there is an $\mathcal{A}$ -good clause $D_{1}$ such that there is a path from $D_{0}$ to $D_{1}$ of length $t$ and $|\widetilde{\mathop{\mathrm{Cl}}}(L(D_{1}))|\leq c\ell$ . Let $k:=\lceil\frac{t}{2c\ell}\rceil$ , then $c\ell(k-1)\leq t/2$ . We repeat the same reasoning $k-1$ more times for all $i$ from $1$ to $k-1$ maintaining invariant $|\widetilde{\mathop{\mathrm{Cl}}}(L(D_{i}))|\leq c\ell i$ : if for every $\mathcal{A}$ -good clause $C$ such that there is a path from $D_{i}$ to $C$ of length $t-c\ell i$ , $|\widetilde{\mathop{\mathrm{Cl}}}(L(C))|\geq c\ell(i+1)$ , then by Claim 42, the size of $\Pi$ is at least $2^{c}$ . Otherwise, there is an $\mathcal{A}$ -good clause $D_{i+1}$ such that there is a path from $D_{i}$ to $D_{i+1}$ of length $t-c\ell i$ and $|\widetilde{\mathop{\mathrm{Cl}}}(L(D_{i+1}))|\leq c\ell(i+1)$ .

So we get that either the size of refutation is at least $2^{c}$ or depth is at least the length of the path from $D_{0}$ to $D_{1}$ , from $D_{1}$ to $D_{2}$ , etc, from $D_{k-1}$ to $D_{k}$ which is at least $kt/2\geq\frac{t^{2}}{4cl}$ . $\hfill\blacktriangleleft$

Corollary 43 (cf. Corollary 8.3 from [3]).

Let $\mathrm{T}(G,c)$ be an unsatisfiable Tseitin formula based on a spectral $(n,d,\alpha)$ -expander. Then, any $\mathrm{Res}(\oplus)$ refutation of $\mathrm{T}(G,c)\circ Maj_{5}$ has either size at least $2^{n}$ or depth at least $\frac{n}{20}\cdot\left\lfloor d\cdot\frac{(1-\alpha)}{8}\right\rfloor^{2}$ .

In particular, if $d=\Theta(\log n)$ and $\alpha<1$ is a constant, then $\mathrm{T}(G,c)\circ Maj_{5}$ is a formula with $m=5dn/2$ variables and of size $\mathrm{poly}(m)$ . And any $\mathrm{Res}(\oplus)$ refutation of $\mathrm{T}(G,c)\circ Maj_{5}$ has either size at least $2^{\Omega(m/\log m)}$ or depth at least $\Omega(m\log m)$ .

Proof.

The proof repeats the proof of Corollary 8.3 from [3], where the application of Theorem 8.1 from [3] is substituted by the application of Theorem 41. $\hfill\blacktriangleleft$

References

[1] M. Ajtai. $\sum_{1}^{1}$ -formulae on finite structures. Annals of Pure and Applied Logic, 24(1):1–48, 1983. doi:10.1016/0168-0072(83)90038-6.
[2] Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417–433, 1994. doi:10.1007/BF01302964.
[3] Yaroslav Alekseev and Dmitry Itsykson. Lifting to bounded-depth and regular resolutions over parities via games. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC ’25), June 23–27, 2025, Prague, Czechia. ACM, 2025. The full version is available as ECCC technical report TR24-128, Revision 1. doi:10.1145/3717823.3718150.
[4] Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323–334, 2008. Computational Complexity 2003. doi:10.1016/j.jcss.2007.06.025.
[5] Paul Beame and Sajin Koroth. On Disperser/Lifting Properties of the Index and Inner-Product Functions. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference (ITCS 2023), volume 251 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1–14:17, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITCS.2023.14.
[6] Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October 20-23, 2012, pages 351–360. IEEE Computer Society, 2012. doi:10.1109/FOCS.2012.48.
[7] Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvorák. Exponential separation between powers of regular and general resolution over parities. In Rahul Santhanam, editor, 39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, volume 300 of LIPIcs, pages 23:1–23:32. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CCC.2024.23.
[8] Sam Buss and Neil Thapen. A simple supercritical tradeoff between size and height in resolution. Electron. Colloquium Comput. Complex., TR24-001, 2024. URL: https://eccc.weizmann.ac.il/report/2024/001.
[9] Farzan Byramji and Russell Impagliazzo. Lifting to randomized parity decision trees. Electron. Colloquium Comput. Complex., TR24-202, 2024. URL: https://eccc.weizmann.ac.il/report/2024/202.
[10] Arkadev Chattopadhyay and Pavel Dvorak. Super-critical trade-offs in resolution over parities via lifting. In Srikanth Srinivasan, editor, 40th Computational Complexity Conference CCC 2025, August 05–08, 2025, Toronto, Canada, volume 339 of LIPIcs, 2025. Available as ECCC technical report TR24-132. URL: https://eccc.weizmann.ac.il/report/2024/132/.
[11] Arkadev Chattopadhyay, Nikhil S. Mande, Swagato Sanyal, and Suhail Sherif. Lifting to parity decision trees via stifling. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 33:1–33:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITCS.2023.33.
[12] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36–50, March 1979. doi:10.2307/2273702.
[13] Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and weisfeiler-leman. Electron. Colloquium Comput. Complex., TR24-185, 2024. URL: https://eccc.weizmann.ac.il/report/2024/185.
[14] Klim Efremenko, Michal Garlík, and Dmitry Itsykson. Lower bounds for regular resolution over parities. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 640–651. ACM, 2024. The full version is available as ECCC technical report TR23-187. doi:10.1145/3618260.3649652.
[15] Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely deep proofs. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 70:1–70:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.ITCS.2022.70.
[16] Merrick Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pages 260–270, 1981. doi:10.1109/SFCS.1981.35.
[17] Mika Göös, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. Electron. Colloquium Comput. Complex., TR24-186, 2024. URL: https://eccc.weizmann.ac.il/report/2024/186.
[18] Svyatoslav Gryaznov, Sergei Ovcharov, and Artur Riazanov. Resolution over linear equations: Combinatorial games for tree-like size and space. ACM Trans. Comput. Theory, July 2024. Just Accepted. doi:10.1145/3675415.
[19] Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Ann. Pure Appl. Log., 171(1), 2020. doi:10.1016/J.APAL.2019.102722.
[20] Vladimir Podolskii and Alexander Shekhovtsov. Randomized lifting to semi-structured communication complexity via linear diversity. Electron. Colloquium Comput. Complex., TR24-199, 2024. URL: https://eccc.weizmann.ac.il/report/2024/199.
[21] A. A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mat. Zametki, 41:598–607, 1987.
[22] Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1–16:14, 2016. doi:10.1145/2858790.
[23] Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77–82, 1987. doi:10.1145/28395.28404.
[24] D.J.A. Welsh. Generalized versions of Hall’s theorem. Journal of Combinatorial Theory, Series B, 10(2):95–101, 1971. doi:10.1016/0095-8956(71)90069-4.

[bib.bib1] [1] M. Ajtai. $\sum_{1}^{1}$ -formulae on finite structures. Annals of Pure and Applied Logic, 24(1):1–48, 1983. doi:10.1016/0168-0072(83)90038-6.

[bib.bib2] [2] Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417–433, 1994. doi:10.1007/BF01302964.

[bib.bib3] [3] Yaroslav Alekseev and Dmitry Itsykson. Lifting to bounded-depth and regular resolutions over parities via games. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC ’25), June 23–27, 2025, Prague, Czechia. ACM, 2025. The full version is available as ECCC technical report TR24-128, Revision 1. doi:10.1145/3717823.3718150.

[bib.bib4] [4] Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323–334, 2008. Computational Complexity 2003. doi:10.1016/j.jcss.2007.06.025.

[bib.bib5] [5] Paul Beame and Sajin Koroth. On Disperser/Lifting Properties of the Index and Inner-Product Functions. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference (ITCS 2023), volume 251 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1–14:17, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ITCS.2023.14.

[bib.bib6] [6] Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October 20-23, 2012, pages 351–360. IEEE Computer Society, 2012. doi:10.1109/FOCS.2012.48.

[bib.bib7] [7] Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvorák. Exponential separation between powers of regular and general resolution over parities. In Rahul Santhanam, editor, 39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, volume 300 of LIPIcs, pages 23:1–23:32. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CCC.2024.23.

[bib.bib8] [8] Sam Buss and Neil Thapen. A simple supercritical tradeoff between size and height in resolution. Electron. Colloquium Comput. Complex., TR24-001, 2024. URL: https://eccc.weizmann.ac.il/report/2024/001.

[bib.bib9] [9] Farzan Byramji and Russell Impagliazzo. Lifting to randomized parity decision trees. Electron. Colloquium Comput. Complex., TR24-202, 2024. URL: https://eccc.weizmann.ac.il/report/2024/202.

[bib.bib10] [10] Arkadev Chattopadhyay and Pavel Dvorak. Super-critical trade-offs in resolution over parities via lifting. In Srikanth Srinivasan, editor, 40th Computational Complexity Conference CCC 2025, August 05–08, 2025, Toronto, Canada, volume 339 of LIPIcs, 2025. Available as ECCC technical report TR24-132. URL: https://eccc.weizmann.ac.il/report/2024/132/.

[bib.bib11] [11] Arkadev Chattopadhyay, Nikhil S. Mande, Swagato Sanyal, and Suhail Sherif. Lifting to parity decision trees via stifling. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 33:1–33:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITCS.2023.33.

[bib.bib12] [12] Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36–50, March 1979. doi:10.2307/2273702.

[bib.bib13] [13] Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and weisfeiler-leman. Electron. Colloquium Comput. Complex., TR24-185, 2024. URL: https://eccc.weizmann.ac.il/report/2024/185.

[bib.bib14] [14] Klim Efremenko, Michal Garlík, and Dmitry Itsykson. Lower bounds for regular resolution over parities. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 640–651. ACM, 2024. The full version is available as ECCC technical report TR23-187. doi:10.1145/3618260.3649652.

[bib.bib15] [15] Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely deep proofs. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 70:1–70:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.ITCS.2022.70.

[bib.bib16] [16] Merrick Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pages 260–270, 1981. doi:10.1109/SFCS.1981.35.

[bib.bib17] [17] Mika Göös, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. Electron. Colloquium Comput. Complex., TR24-186, 2024. URL: https://eccc.weizmann.ac.il/report/2024/186.

[bib.bib18] [18] Svyatoslav Gryaznov, Sergei Ovcharov, and Artur Riazanov. Resolution over linear equations: Combinatorial games for tree-like size and space. ACM Trans. Comput. Theory, July 2024. Just Accepted. doi:10.1145/3675415.

[bib.bib19] [19] Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Ann. Pure Appl. Log., 171(1), 2020. doi:10.1016/J.APAL.2019.102722.

[bib.bib20] [20] Vladimir Podolskii and Alexander Shekhovtsov. Randomized lifting to semi-structured communication complexity via linear diversity. Electron. Colloquium Comput. Complex., TR24-199, 2024. URL: https://eccc.weizmann.ac.il/report/2024/199.

[bib.bib21] [21] A. A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mat. Zametki, 41:598–607, 1987.

[bib.bib22] [22] Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1–16:14, 2016. doi:10.1145/2858790.

[bib.bib23] [23] Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77–82, 1987. doi:10.1145/28395.28404.

[bib.bib24] [24] D.J.A. Welsh. Generalized versions of Hall’s theorem. Journal of Combinatorial Theory, Series B, 10(2):95–101, 1971. doi:10.1016/0095-8956(71)90069-4.

Amortized Closure and Its Applications in Lifting for Resolution over Parities

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Lifting

Theorem 1 ([3]).

Theorem 2 ([10]).

1.2 Our contributions

Theorem 3 (Theorem 37).

Theorem 4 (Informal restatement of Corollary 43).

1.2.1 Bounded-width lifting

Safe sets and closure

Proposition 5.

A (𝝋,𝒘)-game for resolution

A (𝝋,𝒘)-game for 𝐑𝐞𝐬⁢(⊕)

1.2.2 Amortized closure

Example 6.

Theorem 7.

1.2.3 Lower bound for depth-𝒄⁢𝒏⁢𝐥𝐨𝐠⁡𝒏 𝐑𝐞𝐬⁢(⊕)

Our improvement

Lemma 8 (Lemma 38).

1.3 Discussion about closures

1.4 Further research

2 Closure and amortized closure

2.1 Safe and dangerous sets of linear forms

Theorem 9 ([14]).

2.2 Closure

Lemma 10 (Uniqueness [14]).

Lemma 11 (Monotonicity [14]).

Lemma 12 (Span invariance [14]).

Lemma 13 (Size bound [14]).

Algorithm 14.

Lemma 15 ([14]).

Corollary 16.

2.3 Coverable sets

Theorem 17 ([24]).

Theorem 18.

2.4 Amortized closure and its properties

Lemma 19 (Size bound).

Proof.

Lemma 20 (Span invariance).

Proof.

Theorem 21 (Lipschitz continuity).

Proof.

Corollary 22 (Monotonicity).

Proof.

2.4.1 Relation between closures

Proposition 23.

Proof.

Lemma 24.

Proof.

Lemma 25.

Proof.

Lemma 26.

Proof.

Lemma 27.

Proof.

Lemma 28.

Proof.

2.5 Proof of Theorem 18

Proof of Theorem 18.

Claim 29.

Proof.

Claim 30.

Proof.

Claim 31.

Proof.

Lemma 32.

Proof.

3 Preliminary knowledge on resolution over parities and lifting

3.1 Resolution and resolution over parities

A $(\varphi,w)$ -game for resolution

A $(\varphi,w)$ -game for $\mathrm{Res}(\oplus)$

1.2.3 Lower bound for depth- $cn\log n$ $\mathrm{Res}(\oplus)$

5 Lower bound for depth- $\Omega(n\log n)$ $\mathrm{Res}(\oplus)$

$(\varphi,\mathcal{A})$ -games of Prover and Delayer with starting position $\rho_{0}\in\mathcal{A}$