Super-Critical Trade-Offs in Resolution over Parities via Lifting

Understanding trade-offs among complexity measures in a computational model is a well known interesting theme, with many published results (for example, time-space trade-offs [15, 16, 26], rounds-communication trade-offs [21, 10, 2] and space-size trade-offs in propositional proof complexity [6, 3, 5]). Typically, in these trade-offs, one showed that in various models of computation, simultaneous optimization of two complexity measures, like space and time, or rounds and total communication, or space and width (in refuting CNF formulas) is not always possible. In particular trying to optimize one complexity measure, necessarily leads to a huge blow-up in the other measure. For instance, in Yao’s 2-party model of communication, the Greater-Than function can be computed in $1$ round. It can also be computed using randomized protocols of communication cost $O(\log n)$. But every $O(1)$-round protocol, requires $\mathrm{\Omega }(n)$ communication cost. On the other hand, every function has a protocol of cost $O(n)$. In all of the trade-off results cited above, the general story was that trying to optimize the use of one resource, led to the cost with respect to to the other resource shooting up to the cost needed by a naive/generic algorithm.

In 2016, Razborov [24] exhibited formulas for which very different and extreme kind of trade-offs hold in the propositional proof system of resolution. Although these unsatisfiable $k$-CNF formulas on $n$ variables have refutations of $O(k)$ width, every one of their tree-like refutation of width less than $n^{1-ϵ}/k$ has size $\text{exp}(n^{\mathrm{\Omega }(k)})$. That is, despite the fact that every $n$-variable formula has a generic tree-like refutation of size $2^n$, these exhibited formulas that do have refutation of small width require super-critical tree-like refutation size whenever width is mildly restricted. Moreover, the super-critical size is in fact exponentially larger than the generic upper bound. Razborov remarked that such a phenomenon seemed extremely rare in the known body of tradeoff results in the computational complexity literature. In concluding his work, he urged finding more instances of such trade-offs. In response to that, follow-up works have appeared. They can be classified into two types. Ones which continue to focus on resolution and, others on more powerful proof systems. Examples of the former include work by Berkholz and Nordstrom [8], who showed super-critical trade-offs between width and space. A recent work of Berkholz, Lichter and Vinall-Smeeth [7] proves super-critical trade-offs for narrow resolution width and narrow tree-like size for refuting the isomorphism of two graphs.

The second type of work answers Razborov’s call by finding such trade-offs in stronger proof systems. This includes the recent work of Fleming, Pitassi and Robere [14] who first showed that the argument of Razborov extends to general resolution DAGs. They then use it along with appropriate lifting theorems to prove trade-offs between size and depth for DAG like Resolution, Res$(k)$, and cutting planes. In very recent progress in the area, De Rezende, Fleming, Jannet, Nordström, and Pang [12], and Göös, Maystre, Risse, Sokolov [18] independently showed super-critical trade-offs not only for various proof systems but also the first super-critical depth-size tradeoffs for monotone circuits. Our work also falls in this second type as we study tree-like resolution over parities, that generalizes tree-like resolution.

We exhibit super-critical trade-offs for width and tree-like size/depth in the style of Razborov for resolution over parities, denoted by $\text{Res}(\oplus )$. This system, introduced by Itsykson and Sokolov [19, 20], is one of the simplest generalizations of resolution for which obtaining super-polynomial lower bounds on size of refutations is a current, well known, challenge. Very recent works (see [13, 9]) managed to obtain exponential lower bounds on the size of regular proofs in this system.

Our work here will concern tree-like $\text{Res}(\oplus )$ proofs. Lower bounds for them were obtained by Itsykson and Sokolov [20] themselves. More recently, two independent works, one by Beame and Koroth [4] and the other by Chattopadhyay, Mande, Sanyal and Sherif [11], proved lifting theorems that yielded a systematic way of lifting tree-like resolution width complexity to strong lower bounds on size of tree-like $\text{Res}(\oplus )$ proofs for formulas lifted with constant-size gadgets. In this paper, we extend the lifting theorem by Chattopadhyay et al. [11] in the following manner. Their result was applicable to parity decision trees (duals of tree-like $\text{Res}(\oplus )$ proofs) that only had usual nodes where the algorithm queried (correspondingly the proof resolved on) an ${𝔽}_2$ linear form. We call such nodes query nodes. On the other hand, we want to deal here with width-bounded proofs that could be much deeper than $n$, the total number of variables of the formula. This would correspond to parity decision trees where the height is much larger than $n$, and therefore, necessarily there are nodes that forget. The affine space corresponding to such a forget node $u$ is strictly contained in the affine space corresponding to $u$’s only child node $v$. Alternatively, in the bottom-up view of the corresponding proof, the linear clause at $v$ is strictly weakened to get the linear clause at $u$. Dealing with such nodes, so that the width of the (ordinary) clauses in the extracted resolution proof never exceed the corresponding width of the linear clauses, is the main technical contribution of this work. Thus, we establish a depth-to-size lifting result from tree-like $\text{Res}(\oplus )$ of arbitrary depth to tree-like resolution, which also preserves the width of the refutation.

Applying Theorem 1 to the trade-off by Razborov [24], we immediately obtain an analogous trade-off in the $\text{Res}(\oplus )$ proof system.

The contradiction $\tau$ from the previous theorem is a lift of the contradiction ${\tau }^{\prime }$ constructed by Razborov [24] by an appropriate gadget $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ with a constant size. A caveat of ${\tau }^{\prime }$ (as Razborov also noted) is that the number of clauses of ${\tau }^{\prime }$ is $n^{\mathrm{\Theta }(k)}$. Naturally, this caveat is inherited by our contradiction $\tau$. This issue was addressed in very recent work of de Rezende et al. [12]. They provided a contradiction $\chi$ such that the size of its tree-like resolution with bounded width is super-exponential in not just in the number of variables but also in the size of the formula. However, the bound on width of the tree-like resolution for which super-critical size is needed is much more strict than in Razborov’s result. They showed the super-critical trade-off only for tree-like resolution of width smaller than $2w$, where $w$ is the width of the resolution refutation of $\chi$. Since our gadget has size 3, we can guarantee only resolution refutation with width at most $3w$ for the lifted formula $\chi \circ g$. Thus, we can not lift their super-critical trade-off to $\text{Res}(\oplus )$ as it is extremely sensitive to width. Razborov’s result [24], on the other hand, is more robust making it possible to be lifted by our Theorem 1.

If one were able to construct another formula $\tilde{\tau }$ improving state-of-the-art in supercritical trade-off between width and size of tree-like resolution that is not so sensitive to the width of the refutations, this improvement could be used with our simulation theorem (Theorem 1) and be lifted to tree-like $\text{Res}(\oplus )$.

A proof in a propositional proof system starts from a set of clauses $\mathrm{\Phi }$, called axioms, that is purportedly unsatisfiable. It generates a proof by deriving the empty clause from the axioms, using inference rules. The main inference rule in the standard resolution, called the resolution rule, derives a clause $A\vee B$ from clauses $A\vee x$ and $B\vee \neg x$ (i.e., we resolve the variable $x$). If we can derive the empty clause from the original set $\mathrm{\Phi }$, then it proves that the set $\mathrm{\Phi }$ is unsatisfiable.

Resolution over parities ($\text{Res}(\oplus )$) is a generalization of the standard resolution, using linear clauses (disjunction of linear equations in ${𝔽}_2$) to express lines of a proof. It consists of two rules:

Resolution Rule:

From linear clauses $A\vee (\mathrm{\ell }=0)$ and $B\vee (\mathrm{\ell }=1)$ derive a linear clause $A\vee B$.

Weakening Rule:

From a linear clause $A$ derive a linear clause $B$ that is semantically implied by $A$ (i.e., any assignment satisfying $A$ also satisfies $B$).

The length $|\mathrm{\Pi }|$ of a resolution (or $\text{Res}(\oplus )$) refutation $\mathrm{\Pi }$ of a formula $\mathrm{\Phi }$ is the number of applications of the rules above in order to refute the formula $\mathrm{\Phi }.$ The width $w(\mathrm{\Pi })$ of a resolution (or $\text{Res}(\oplus )$) refutation $\mathrm{\Pi }$ is the maximum width of any (linear) clause that is used in the resolution proof. A (linear) resolution proof is tree-like if the resolution rule is applied in a tree-like fashion. The depth $d(\mathrm{\Pi })$ of the tree-like proof $\mathrm{\Pi }$ is the depth of the underlying tree (i.e., the length of the longest path from the root to a leaf).

We can replace the general resolution rule with a canonical one:

Canonical Resolution Rule:

From linear clauses $C\vee (\mathrm{\ell }=0)$ and $C\vee (\mathrm{\ell }=1)$ derive a linear clause $C$.

Using the canonical resolution rule instead of the general one will not make the proof system substantially weaker. If we want to apply the resolution rule on the clauses $A\vee (\mathrm{\ell }=0)$ and $B\vee (\mathrm{\ell }=1)$, we can apply the weakening rule to both of them to get linear clauses $A\vee B\vee (\mathrm{\ell }=0)$ and $A\vee B\vee (\mathrm{\ell }=1)$ and then apply the canonical resolution rule to derive the clause $A\vee B$. Thus, from a tree-like $\text{Res}(\oplus )$ refutation $\mathrm{\Pi }$ of a contradiction $\mathrm{\Phi }$, we can derive an equivalent tree-like $\text{Res}(\oplus )$ refutation ${\mathrm{\Pi }}^{\prime }$ that uses only canonical resolution rule (and the weakening rule) with $|{\mathrm{\Pi }}^{\prime }|\le 3\cdot |\mathrm{\Pi }|$, $d({\mathrm{\Pi }}^{\prime })\le 2\cdot d(\mathrm{\Pi })$, and $w({\mathrm{\Pi }}^{\prime })\le w(\mathrm{\Pi })+1$ as for each application of the resolution rule in $\mathrm{\Pi }$ we add 2 applications of the weakening rule in ${\mathrm{\Pi }}^{\prime }$, and the width might increase by 1 as we introduce clause $A\vee B\vee (\mathrm{\ell }=0)$ and $A\vee B\vee (\mathrm{\ell }=1)$ but only the clause $A\vee B$ was present in $\mathrm{\Pi }$.

It is known that a tree-like resolution (or $\text{Res}(\oplus )$) proof, for an unsatisfiable set of clauses $\mathrm{\Phi }$, corresponds to a (parity) decision tree for a search problem $\text{Search}(\mathrm{\Phi })$ that is defined as follows. For a given assignment $\alpha$ of the $n$ variables of $\mathrm{\Phi }$, one needs to find a clause in $\mathrm{\Phi }$ that is not satisfied by $\alpha$ (at least one exists as the set $\mathrm{\Phi }$ is unsatisfiable). The correspondence holds even for general (not only tree-like) proofs (see for example Garg et al. [17], who credit it to earlier work of Razborov [23] that was simplified by Pudlák [22] and Sokolov[25]), but in this paper, we are interested only in tree-like proofs.

Let $R\subseteq {\{0,1\}}^m\times O$, where $O$ is a set of possible outputs. A forgetting parity decision tree (FPDT) computing $R$ is a tree $𝒯$ such that each node has at most two children and the following conditions hold:

• $\mathrm{■}$

  Each node $v$ is associated with an affine space $A_v\subseteq {𝔽}_2^m$.

• $\mathrm{■}$

  For every node $v$ with two children $u$ and $w$ is called a query nodes. There is a linear query $f_v$ such that $A_u=\{x\in A_v|⟨f_v,x⟩=0\}$ and $A_w=\{x\in A_v|⟨f_v,x⟩=1\}$, or vice versa. We say that $f_v$ is the query at $v$.

• $\mathrm{■}$

  Every node $v$ with exactly one child $u$ is called a forget node. It holds that $A_v\subseteq A_u$.

• $\mathrm{■}$

  Each leaf $\mathrm{\ell }$ is labeled by $o_{\mathrm{\ell }}\in O$ such that for all $x\in A_{\mathrm{\ell }}$, it holds that $(x,o_{\mathrm{\ell }})\in R$.

• $\mathrm{■}$

  For the root $r$, $A_r={𝔽}_2^m$.

The size $|𝒯|$ of an FPDT $𝒯$ is the number of nodes of $𝒯$ and the width $w(𝒯)$ of FPDT $𝒯$ is the largest integer $w$ such that there exists an affine space of co-dimension at least $w$ associated with some node of $𝒯$. The depth of $𝒯$ is denoted $d(𝒯)$. Note that there are no forget nodes in a standard parity decision tree. Thus, for such trees, the width is exactly the depth of the tree. It no longer holds for this model, because we may “forget” some linear queries that have been made earlier.

A forgetting decision tree (FDT) is defined similarly to FPDT but instead of affine spaces, cubes are associated with each node. Consequently, the width $w(𝒯)$ of FDT is the maximum number $w$ such that there exists a cube of width at least $w$ associated with some node of $𝒯$ and queries of single variables replace the linear queries at nodes.

The correspondence between an F(P)DT’s and tree-like resolution (or $\text{Res}(\oplus )$) proofs using only canonical resolution rule is the following: We represent a (linear) resolution proof as a tree where nodes are associated with (linear) clauses. The leaves are associated with clauses of $\mathrm{\Phi }$ and the root is associated with the empty clause. Each node with two children corresponds to an application of the canonical resolution rule and each node with exactly one child corresponds to an application of the weakening rule. To get an F(P)DT for $\text{Search}(\mathrm{\Phi })$ we just negate the clauses that are associated with the nodes. Thus, each node is associated with a cube (or an affine space in the case of $\text{Res}(\oplus )$/FPDT). Moreover, a cube $C_v$ (or an affine space $A_v)$ associated with the node $v$ of an F(P)DT $𝒯$ contains exactly the falsifying assignments of the (linear) clause that is associated with the corresponding node in the tree-like refutation $\mathrm{\Pi }$ that corresponds to $𝒯$. It is clear that the width and the depth of such decision tree $𝒯$ are exactly the same as the width and the depth of the corresponding tree-like refutation $\mathrm{\Pi }$ and the length $|\mathrm{\Pi }|$ equals the number of inner nodes of $𝒯$ (as the inner nodes of $𝒯$ correspond to the applications of the resolution rule).

We say an FPDT $𝒯$ is canonical if for each forget node $v$ of $𝒯$ and its only child $u$, it holds that $\text{co-dim}(A_v)=\text{co-dim}(A_u)+1$. We say an FPDT $𝒯$ is succinct if the parent of each forget node is a query node. Note that any FPDT can be transformed into an equivalent canonical (or succinct) FPDT by expanding forget nodes into paths of forget nodes (or contracting paths of forget nodes to single vertices).

Consider an FPDT $𝒯$ and its succinct form $\overline{𝒯}$. Note that the number of query nodes of $\overline{𝒯}$ and $𝒯$ is the same, and analogously the number of query nodes on a root-leaf path in $\overline{𝒯}$ equals the number of query nodes of the corresponding path in $𝒯$. Thus, for an FPDT $𝒯$ we define query size ${|𝒯|}_{𝗊}$ and query depth $d_{𝗊}(𝒯)$ to be the number of query nodes of $𝒯$ and the maximum number of query nodes on a root-leaf path of $𝒯$.

Let $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ be a boolean function. For a relation $R\subseteq {\{0,1\}}^n\times O$ we define its lift $R\circ g\subseteq {\{0,1\}}^{n\mathrm{\ell }}\times O$ as

where $\overrightarrow{g}(y_1^1,\mathrm{\dots },y_{\mathrm{\ell }}^1,\mathrm{\dots },y_1^n,\mathrm{\dots },y_{\mathrm{\ell }}^n)=(g(y_1^1,\mathrm{\dots },y_{\mathrm{\ell }}^1),\mathrm{\dots },g(y_1^n,\mathrm{\dots },y_{\mathrm{\ell }}^n))$.

For CNF $\mathrm{\Phi }$ over $n$ variables $\{x_1,\mathrm{\dots },x_n\}$, let $\mathrm{\Phi }\circ g$ be the following lift of $\mathrm{\Phi }$ over the variables $\{y_j^i\mid i\in [n],j\in [\mathrm{\ell }]\}$. For any clause $D$ of $\mathrm{\Phi }$, let $\text{Vars}(D)$ be the set of variables of $D$, and let ${\eta }_D\in {\{0,1\}}^{\text{Vars}(D)}$ be the only falsifying assignment of $D$. Then,

where $y_j^i\ne {\kappa }_j^i$ is the following literal:

Now, the clauses of $\mathrm{\Phi }\circ g$ are $\{D\circ g\mid D\text{ clause of }\mathrm{\Phi }\}$.

We use the following notation. For a vector $u$ we use both $u_i$ and $u[i]$ to denote the $i$-th entry of $u$, similarly for a matrix $M$ we use $M_{i,j}$ and $M[i;j]$ to denote the entry in the $i$-th row and $j$-th column. For an ordered set of indices $D$ we denote by $u[D]$ the subvector of $u$ given by $D$, i.e., $u[D]={(u_i)}_{i\in D}$. For an abbreviation, we use $u[-i]$ to denote the vector $u$ without the $i$-th entry, i.e., $u[-i]=(u_1,\mathrm{\dots },u_{i-1},u_{i+1},\mathrm{\dots },u_n)$.

In this section, we extend the notion of stifling introduced by Chattopadhyay et al. [11]. Let $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ be a Boolean function. For $i\in [\mathrm{\ell }]$ and $b\in \{0,1\}$, we say a partial assignment $\delta \in {\{0,1,\ast \}}^{\mathrm{\ell }}$ is an $(i,b)$-stifling pattern for $g$ if ${\delta }_j=\ast$ if and only if $j=i$, and for any $\gamma \in {\{0,1\}}^{\mathrm{\ell }}$ such that $\gamma [-i]=\delta [-i]$, we have $g(\gamma )=b$. In words, $\delta$ assigns a value to all but the $i$-th bit and when we extend $\delta$ to a full assignment $\gamma$, it holds that $g(\gamma )=b$ no matter how we set the value of the $i$-th bit.

Chattopadhyay et al. [11] defined a stifled function (namely 1-stifled) as a function $g:{\{0,1\}}^{\mathrm{\ell }}\to \{0,1\}$ such that for each $i\in [\mathrm{\ell }]$ and $b\in \{0,1\}$ there is an $(i,b)$-stifling pattern for $g$. In this work, we require not only the existence of the stifling patterns but a stronger property that we can convert the stifling patterns to each other. More formally, consider an $(i,b)$-stifling pattern ${\delta }^{i,b}$ from the collection $P$ (from the definition above). Let an adversary give us a set of coordinates $D\subseteq [\mathrm{\ell }]\setminus \{i\}$. Then, we are able to pick a coordinate $j\in D$ such that the stifling pattern ${\delta }^{j,b}$ is equal to ${\delta }^{i,b}$ on all coordinates in $D\setminus \{j\}$.

By a simple verification we can show that indexing of two bits ${\mathrm{𝖨𝖭𝖣}}_1:{\{0,1\}}^3\to \{0,1\}$ and majority of 3 bits ${\mathrm{𝖬𝖠𝖩}}_3:{\{0,1\}}^3\to \{0,1\}$ are strongly stifled functions, where ${\mathrm{𝖨𝖭𝖣}}_1(a,d_0,d_1)=d_a$ and ${\mathrm{𝖬𝖠𝖩}}_3(x)=1$ if and only if $\left|\{i\in [3]|x_i=1\}\right|\ge 2$.

Further, the strongly stifled notion is actually stronger than the original stifled notion, because the inner product function of 2-bit vectors ${\mathrm{𝖨𝖯}}_2:{\{0,1\}}^4\to \{0,1\}$ is stifled [11] but not strongly stifled, where ${\mathrm{𝖨𝖯}}_2(x_1,x_2,y_1,y_2)=x_1{x}_2+y_1{y}_{2}mod2$.

For more details, see the appendix.

Let $A\subseteq {𝔽}_2^m$ be an affine space over a field ${𝔽}_2$. A constraint representation of $A$ is a system of linear equations $(M|z)$ where $M\in {𝔽}_2^{q\times m}$ and $z\in {𝔽}_2^q$ for some $q\le m$ such that $A=\{y\mid My=z\}$. The columns of $M$ correspond to the variables of the system $(M|z)$ and rows of $M$ correspond to the constraints. We say a constraint $i$ contains a variable $a$ if $M_{i,a}=1$. A matrix $M\in {𝔽}_2^{q\times m}$ is in an echelon form if there are $q$ columns such that for all $i\in [q]$ it holds that

Thus, the submatrix of $M$ induced by the columns $c_1,\mathrm{\dots },c_q$ is the identity matrix $I_q\in {𝔽}_2^{q\times q}$. The variables corresponding to the columns $c_1,\mathrm{\dots },c_q$ are dependent variables of the system $(M|z)$ and the remaining variables are independent. The $c_i$-th entry of the $i$-th row of $M$ is called the pivot of the $i$-th row. We say a constraint representation $(M|z)$ is in an echelon form if the matrix $M$ is in an echelon form.

Let $C\in {𝔽}_2^{q\times m}$ be a matrix and $t\in {𝔽}_2^q$ be a non-zero vector. We define a matrix $C^{\prime }=\mathrm{𝖣𝖾𝗅}(C,t,i)\in {𝔽}_2^{q-1\times m}$ where $C^{\prime }$ arises from $C$ by adding the $i$-th row to all rows $j$ such that $t_j=1$ and then deleting the row $i$. Analogously, we define the $\mathrm{𝖣𝖾𝗅}$ operation for a constraint representation $(M|z)$ of an affine space $A\subseteq {𝔽}_2^m$, where we treat the vector $z$ as the last column of the matrix $C$. It turns out that the $\mathrm{𝖣𝖾𝗅}$ operation is the only operation needed to get a constraint representation for a super-space as shown in the following theorem that will be the key technical tool for us to process forget nodes while proving our main lifting theorem.

We call the vector $t$ given by Theorem 10 as forgetting vector because it allows us to forget one constraint in the representation of $A_1$ to get a representation of $A_2$. Note that the dimension of $t$ equals the number of equations in the system $(M_1|z_1)$. We say $t$ contains a constraint $i$ if $t_i=1$.

Theorem 10 follows from the following well-known lemma, which we will prove for completeness. Let $V_2\subseteq V_1\subseteq {𝔽}_2^n$ be two vector spaces such that $dim(V_2)=dim(V_1)-1$.

In this section, we prove our lifting theorem.

Razborov [24] showed the following trade-off between width and size of tree-like resolution.

By our simulation, given by Theorem 13, we can lift the trade-off (given by the previous theorem) to tree-like $\text{Res}(\oplus )$ and prove Theorem 3.