Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

To prove his trade-off, Razborov used a compression technique, known as hardness condensation [35, 15], that is based on xorification and variable reuse and converts large but hard formulas into smaller ones that are still hard. Xorification is a well-known technique which replaces every variable in a formula by an XOR of fresh variables. Xorification, or variable substitution in general, has found many applications in proof complexity (see e.g. [10, 8, 9, 6]). Razborov’s compression technique was adapted to the Weisfeiler-Leman (WL) algorithm – an important algorithm in the field of graph isomorphism [23, 4, 27]. The algorithm, parameterized by a dimension $k$, is a graph isomorphism heuristic, that is, whenever it distinguishes two graphs they are not isomorphic but, for every $k$, it fails to distinguish all non-isomorphic graphs [17]. Of particular interest is the number of iterations needed by the $k$-dimensional WL-algorithm to distinguish two graphs; this almost corresponds to the quantifier depth needed in $(k+1)$-variable first-order logic with counting to distinguish them. Berkholz and Nordström [15] adapted Razborov’s compression technique to construct $k$-ary relational structures for which the $k$-dimensional WL-algorithm requires $n^{\mathrm{\Omega }(k/\log k)}$ iterations; here the best known upper bound is $O(n^{k-1}/\log n)$ [24]. From the perspective of trade-offs, first-order logic (without a bound on the variables) requires at most quantifier depth $n$ to distinguish all non-isomorphic graphs, which means this trade-off is also supercritical. The lower bound was recently improved to $n^{\mathrm{\Omega }(k)}$ [24].

The trade-offs described above have a common drawback: They are supercritical with respect to the number of variables and the number of vertices of the structures, respectively, but not with respect to the formula size or the size of the structure (in terms of the number of tuples in the $k$-ary relations). The common reason is that hardness condensation turns $3$-CNF formulas into $k$-CNF formulas and $3$-ary structures into $k$-ary ones. But recently, Grohe, Lichter, Neuen, and Schweitzer [25] introduced a powerful new compression technique for the so-called Cai-Fürer-Immerman (CFI) graphs [17] to prove a lower bound of $\mathrm{\Omega }(n^{k/2})$ for the iteration number of the $k$-dimensional WL-algorithm on graphs of order $n$. The bound not only improves the known ones, it is also a bound on graphs and, as graphs have size $O(n^2)$, the lower bound is supercritical with respect to the structure size. The inspiration for this paper was to see if this new technique yields analogous proof complexity results.

Tree-like refutations can be (almost) exponentially larger than their non-tree-like counterparts [7]. The usual tool to prove width-$k$ tree-like size lower bounds is the Prover-Delayer game [34]. Prover maintains a partial assignment to at most $k$ variables. In each round, Prover forgets one variable and asks Delayer for an assignment to another one. Delayer can either give such an assignment or allow Prover to set it; in the latter case Delayer scores a point. Prover wants to find an inconsistent partial assignment and Delayer wants to gain as many points as possible. If Delayer has a strategy to score $p$ points, then every width-$k$ tree-like refutation has size at least $2^p$. On xorified formulas, where each variable $v$ is replaced with an XOR of $v_0$ and $v_1$, Delayer can always gain a point when Prover queries $v_0$ or $v_1$ so long as the other one is not already assigned. This leads to tree-like size lower bounds exponential in the depth of a refutation [43].

However, the xorification of a graph isomorphism formula is not necessarily a graph isomorphism formula. Since we are interested in such formulas, our idea is to instead apply xorification on the level of graphs. We show that twins in a graph, i.e., vertices with the same neighborhood, can play the role of XORs in a formula: When we isomorphically map a pair of twins in one graph to a pair of twins in the other graph, the image of the first twin can be chosen arbitrary. We consider twinned graphs, where every vertex is replaced by a pair of twins. Ultimately, we want to show that the narrow tree-like refutation size of a twinned graph is exponential in the refutation depth of the original graph. Unfortunately, there seems to be no generic argument for this. To show that this is indeed the case for the graphs we consider, we introduce a variant of the Prover-Delayer game suited for narrow resolution. Then we use techniques from finite model theory to show lower bounds for this game. For other examples of finite-model-theoretic techniques in proof complexity see, e.g. [11, 1, 22].

We cannot reuse the correspondence between width-$(k-1)$ narrow resolution and $k$-variable first-order logic [42], or equivalently the $k$-pebble game [29], because we care about tree-like size, not only about width and depth. The issue is that assigning a variable to one or to zero in graph isomorphism formulas is not symmetric: In terms of isomorphisms, fixing the image of a vertex is usually more restrictive than forbidding a single vertex as the image of another vertex. We introduce a new pebble game, called the $k$-pebble game with blocking, which captures this difference between one and zero assignments. Round lower bounds in the pebble game with blocking imply exponential size lower bounds for tree-like resolution.

Another game is involved in this lower bound. The hardness of uncompressed CFI graphs for $k$-variable first-order logic is captured by the $k$-Cops and Robber game [37, 25], which forgets about the CFI construction and instead considers the simpler underlying base graphs. For compressed CFI graphs, this game was modified to the compressed $k$-Cops and Robber game [25]. To obtain lower bounds for the $k$-pebble game with blocking, we have to introduce a blocking mechanism to the compressed $k$-Cops and Robber game. Via all these games, we obtain the $2^{\mathrm{\Omega }(n^{k/2})}$ narrow width-$k$ tree-like size lower bound in Theorem 1.

We lift Theorem 1 to (non-narrow) resolution. Since lower bounds for narrow resolution imply lower bounds for resolution, transferring the lower bounds is trivial. But it is unclear whether the relevant isomorphism formula can be refuted in (non-narrow) width $k$. By increasing the width by the maximal color class size of these graphs (which is $16$), we can simulate the narrow resolution refutation by a plain resolution refutation. But now the lower bound from Theorem 1 does not apply anymore. At this point, the aforementioned result from [19] comes to hand: The compression of the CFI graphs get modified to obtain, for every fixed , graphs whose isomorphism formula can be refuted in narrow width $k$ but every narrow width $k+t$ refutation has depth at least $\mathrm{\Omega }(n^{k/(t+1)})$. So the lower bound is robust within the range from $k$ to $k+t-1$. This construction can be seen as an interpolation between the original compression [25] with round lower bound $\mathrm{\Omega }(n^{k/2})$ and the linear round lower bound $\mathrm{\Omega }(n)$ by Fürer [20]; both appear as special cases for $t=1$ and $t=k$. Our approach with twinned graphs also applies to the improved construction implying a narrow width-$(k+t)$ tree-like size lower bound of $2^{\mathrm{\Omega }(n^{k/(t-1)})}$, but we need to restrict the range of $t$ even further. For $k$ large enough and $t>16$ we can actually refute isomorphism of the graphs in (non-narrow) width $k+t$ and finally obtain a supercritical trade-off between width and tree-like size for resolution with respect to formula size (Theorem 2).

How the robust compressed CFI construction [19] yields a supercritical width-depth trade-off for resolution was presented at the Oberwolfach workshop Proof Complexity and Beyond [2]. The resulting preprint [19] also contains a trade-off for tree-like resolution. A key difference is that our trade-off applies to graph-isomorphism formulas. Also, different techniques are used. We cannot apply hardness condensation techniques to graph isomorphism formulas but apply a form of xorification on the level of graphs and analyze them using model theoretic techniques. In contrast, the trade-off of [19] is obtained via xorification; the parameters obtained are within a constant factor of one-another.

An (undirected) graph $𝒢$ is a tuple $(V,E)$ where $V$ is a finite set of vertices and $E\subseteq \left(\genfrac{}{}{0pt}{}{V}{2}\right)$ is a set of edges. The vertex set of $𝒢$ is denoted by $V_{𝒢}$ and the edge set of $𝒢$ by $E_{𝒢}$. For $W\subseteq V_{𝒢}$, the subgraph of $𝒢$ induced by $W$ is denoted by $𝒢[W]$. The distance between two vertices $u,v\in V_{𝒢}$ is the number of edges in a shortest path between $u$ and $v$ in $𝒢$. The distance between $U,W\subseteq V_{𝒢}$ is the minimal distance of all $u\in U$ and $v\in W$. We will sometimes consider directed graphs, where the set of edges is a subset of $V_{𝒢}^2$, but we mention this explicitly. A directed graph is acyclic, if it does not contain a (directed) cycle. A source (or sink) is a vertex without incoming (or outgoing) edges. A colored graph $𝒢$ is a tuple $(V,E,\chi )$ such that $(V,E)$ is a graph and $\chi$ is a map $V\to \mathbb{N}$. We interpret $\chi$ as a vertex coloring of $𝒢$ and denote it by ${\chi }_{𝒢}$. The color class of $u\in V_{𝒢}$ is the set ${\chi }_{𝒢}^{-1}({\chi }_{𝒢}(u))$ of vertices of the same color as $u$. The color class size of $𝒢$ is the maximal cardinality of its color classes. The graph $𝒢$ is ordered if $\chi$ is injective. We can see every graph as a colored graph in which every vertex is colored $0$. An isomorphism of colored graphs $𝒢$ and $\mathscr{H}$ is a bijection $f:V_{𝒢}\to V_{\mathscr{H}}$ such that, for all $u,v\in V_{𝒢}$, we have ${\chi }_{𝒢}(u)={\chi }_{\mathscr{H}}(f(u))$, and $\{u,v\}\in E_{𝒢}$ if and only if $\{f(u),f(v)\}\in E_{\mathscr{H}}$. If there is such an isomorphism, $𝒢$ and $\mathscr{H}$ are isomorphic.

A literal is a proposition variable $x$ or its negation $\overline{x}:=\neg x$. We set $\overline{\neg x}=x$. A clause $C$ is a finite set of literals $\{{\lambda }_1,\mathrm{\dots },{\lambda }_k\}$. We may write clauses as disjunctions, e.g., $C=({\lambda }_1\vee \mathrm{\cdots }\vee {\lambda }_k)$. A CNF formula $F$ is a finite set of clauses $\{C_1,\mathrm{\dots },C_m\}$, which we may write as a conjunction $F=(C_1\wedge \mathrm{\cdots }\wedge C_m)$. The set of variables occurring in a clause $C$ is $\mathrm{𝗏𝖺𝗋}(C)$ and for a CNF formula $F$ it is $\mathrm{𝗏𝖺𝗋}(F):={\bigcup }_{C\in F}\mathrm{𝗏𝖺𝗋}(C)$. A (partial) assignment for a CNF formula $F$ is a (partial) map $\sigma :\mathrm{𝗏𝖺𝗋}(F)\to \{0,1\}$. The domain of $\sigma$ is $\mathrm{𝖽𝗈𝗆}(\sigma )$. The size of $\sigma$ is $|\mathrm{𝖽𝗈𝗆}(\sigma )|$. The assignment $\sigma$ violates a clause $C\in F$ if $\mathrm{𝗏𝖺𝗋}(C)\subseteq \mathrm{𝖽𝗈𝗆}(\sigma )$ and $\sigma$ satisfies no literal in $C$. For a variable $x\in \mathrm{𝗏𝖺𝗋}(F)$ and a Boolean value $\delta \in \{0,1\}$, let $\sigma [x\mapsto \delta ]$ be the assignment with domain $\mathrm{𝖽𝗈𝗆}(\sigma )\cup \{x\}$ derived from $\sigma$ that sets $x$ to $\delta$, i.e., $\sigma [x\mapsto \delta ](x)=\delta$ and $\sigma [x\mapsto \delta ](y)=\sigma (y)$ for all $y\in \mathrm{𝖽𝗈𝗆}(\sigma )\setminus \{x\}$. For partial assignments $\sigma$ and ${\sigma }^{\prime }$, we write ${\sigma }^{\prime }\subseteq \sigma$ if $\mathrm{𝖽𝗈𝗆}({\sigma }^{\prime })\subseteq \mathrm{𝖽𝗈𝗆}(\sigma )$ and ${\sigma }^{\prime }(x)=\sigma (x)$ for all $x\in \mathrm{𝖽𝗈𝗆}({\sigma }^{\prime })$. For $k\in \mathbb{N}$, we write $[k]:=\{1,\mathrm{\dots },k\}$. We now introduce the proof systems studied in this paper.

A resolution derivation is a narrow resolution derivation using only Rules 1 and 2. The derivation $\pi$ is tree-like if $\pi$ is a tree. In this case we call the unique source the root and the sinks leaves. The size $|\pi |$ of the derivation $\pi$ is the number of vertices $|V|$. The depth of $\pi$ is the length of the longest directed path in it. The width of a clause $C$ is its number of literals. The width of a derivation $w(\pi )$ is the maximal width of all clauses in $\pi$. The narrow width of a derivation $w^{\ast }(\pi )$ is the maximal number of literals among all those clauses in $\pi$ that are not axioms. A $k$-narrow derivation is a narrow resolution derivation of narrow width at most $k$. A derivation of the empty clause from $F$ is a refutation of $F$.

Let $𝒢$ and $\mathscr{H}$ be non-isomorphic colored graphs. The $k$-narrow Prover-Delayer game on $𝒢,\mathscr{H}$ is played by two players, Prover and Delayer, who construct partial assignments for $\mathrm{𝖨𝖲𝖮}(𝒢,\mathscr{H})$ as follows. The game begins with the empty assignment ${\sigma }_0=\mathrm{\varnothing }$. Let ${\sigma }_{t-1}$ be the assignment after the $(t-1)$-th round. In round $t$, Prover chooses $\sigma \subseteq {\sigma }_{t-1}$ with $|\mathrm{𝖽𝗈𝗆}(\sigma )|\le k-1$ and makes one of the following kinds of moves.

1. 1.

   Resolution Move: Prover chooses a variable $x\notin \mathrm{𝖽𝗈𝗆}(\sigma )$. Delayer chooses a response.

   1. (a)

      Committal Response: Delayer responds with $\delta \in \{0,1\}$ and sets ${\sigma }_t:=\sigma [x\mapsto \delta ]$.

   2. (b)

      Point Response: Delayer gets a point; Prover picks $\delta \in \{0,1\}$ and sets ${\sigma }_t:=\sigma [x\mapsto \delta ]$.

2. 2.

   Narrow Move: Prover chooses a color clause $C$ from $\mathrm{𝖨𝖲𝖮}(𝒢,\mathscr{H})$. Again Delayer chooses one of two response types.

   1. (a)

      Committal Response: Delayer chooses some $x\in C\setminus {\sigma }^{-1}(0)$ and sets ${\sigma }_t:=\sigma [x\mapsto 1]$.

   2. (b)

      Point Response: Delayer chooses distinct $x,y\in C\setminus {\sigma }^{-1}(0)$ and gets a point; Prover chooses $z\in \{x,y\}$ and sets ${\sigma }_t:=\sigma [z\mapsto 1]$.

If the assignment ${\sigma }_t$ violates a clause of $\mathrm{𝖨𝖲𝖮}(𝒢,\mathscr{H})$, the game ends and Prover wins. Otherwise, the game continues in round $t+1$. Prover has an $r$-point strategy if, no matter how Delayer plays, Prover can always win the game while limiting Delayer to at most $r$ points. If Prover does not have an $r$-point strategy, then Delayer has an $(r+1)$-point strategy. It will be useful to start the $k$-narrow Prover-Delayer game on $𝒢,\mathscr{H}$ from assignments $\sigma \ne \mathrm{\varnothing }$. In this case, the game starts at ${\sigma }_0=\sigma$. By constructing strategies for Delayer, the game can be used to show tree-like size lower bound for resolution refutations of graph isomorphism formulas.

Prover follows $\pi$ starting at the empty clause at the root. If a resolution rule is applied to a variable $x$, then Prover makes a resolution move for $x$. Similarly, Prover follows narrow resolution moves. If Delayer makes a committal response, Prover moves to the corresponding child in $\pi$. If Delayer makes a point response, Prover moves to the child with the smallest subtree “below it”, at least halving the size of the subtree at the current position. Prover wins if a leaf is reached, so Delayer can score at most $\lceil \log (|\pi |)\rceil$ points. $◀$

We next recall the connection between $(k-1)$-narrow resolution refutations and the $k$-variable fragment of first order logic [42]. For an integer $k$, we write ${ℒ}_k$ for the set of first order formulas using at most $k$ distinct variables. We denote the set of ${ℒ}_k$-formulas with quantifier depth at most $r$ by ${ℒ}_{k,r}$. If two graphs $𝒢$ and $\mathscr{H}$ satisfy the same sentences of ${ℒ}_k$ or ${ℒ}_{k,r}$, the graphs are ${ℒ}_k$-equivalent or ${ℒ}_{k,r}$-equivalent, respectively, and we write $𝒢{\simeq }^k\mathscr{H}$ or $𝒢{\simeq }^{k,r}\mathscr{H}$, respectively.

These equivalences are characterized by the following game: Let $𝒢$ and $\mathscr{H}$ be (colored) graphs and $k,r\in \mathbb{N}$. The $r$-round $k$-pebble game on $𝒢,\mathscr{H}$ is played by two players, Spoiler and Duplicator. A position of the game is a pair $(\alpha ,\beta )$ of partial assignments $\alpha :[k]\to V_{𝒢}$ and $\beta :[k]\to V_{\mathscr{H}}$ such that $\mathrm{𝖽𝗈𝗆}(\alpha )=\mathrm{𝖽𝗈𝗆}(\beta )$. These maps define positions of up to $k$ pebble pairs on $𝒢$ and $\mathscr{H}$. Duplicator aims to show that $𝒢$ and $\mathscr{H}$ are isomorphic; Spoiler tries to show they are not. Initially, no pebbles are placed. Let $({\alpha }_t,{\beta }_t)$ be the position at the end of round . At the beginning of round $t+1$, Spoiler picks one of the graphs, say $𝒢$, and $i\in [k]$. The $i$-th pebble pair is picked up and Spoiler places the $i$-th pebble for $𝒢$ on some $u\in V_{𝒢}$ yielding the map ${\alpha }_{t+1}$. Duplicator responds by placing the $i$-th pebble for $\mathscr{H}$ on a vertex of $\mathscr{H}$ yielding ${\beta }_{t+1}$. If $({\alpha }_{t+1},{\beta }_{t+1})$ does not induce a partial isomorphism, meaning that $\alpha (i)\mapsto \beta (i)$ is not an isomorphism of the induced subgraphs $𝒢[\{\alpha (i)\mid i\in \mathrm{𝖽𝗈𝗆}(\alpha )\}]$ and $\mathscr{H}[\{\beta (i)\mid i\in \mathrm{𝖽𝗈𝗆}(\beta )\}]$, then Spoiler wins. Otherwise, if , the play continues in the next round. If $t+1=r$, then Duplicator wins. A player (Spoiler or Duplicator) has a winning strategy, if they can win independently of the moves of the other player.

It will sometimes be convenient to start the game from position $({\alpha }_0,{\beta }_0)\ne (\mathrm{\varnothing },\mathrm{\varnothing })$; nothing else in the rules of the games changes in this case. Similarly, we may sometimes not specify the number of rounds in advance; in this case the game only ends if Spoiler wins.

Let $𝒢$ and $\mathscr{H}$ be colored graphs and $k,r\in \mathbb{N}$. We define the $r$-round $k$-pebble game with blocking on $𝒢$ and $\mathscr{H}$ as follows. The game is played in rounds by Spoiler and Duplicator. A position in the game is a triple $(\alpha ,\beta ,c)$ of partial maps $\alpha :[k]\to V_{𝒢}$, $\beta :[k]\to V_{\mathscr{H}}$, and $c:[k]\to \{\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋},\mathrm{𝖻𝗅𝗈𝖼𝗄𝗂𝗇𝗀}\}$ with $\mathrm{𝖽𝗈𝗆}(\alpha )=\mathrm{𝖽𝗈𝗆}(\beta )=\mathrm{𝖽𝗈𝗆}(c)$. The first two maps give the positions of the pebbles and $c$ marks each pair of pebbles as either regular or blocking. Regular pebbles (possibly) define partial isomorphisms as before, but blocking ones forbid certain ones as follows.

In the initial position $({\alpha }_0,{\beta }_0,c_0)$, all maps are empty. Let $({\alpha }_t,{\beta }_t,c_t)$ be the position after the $t$-th round. At the beginning of the $(t+1)$-th round, Spoiler can make either a regular move or a blocking move. A regular move works in the same way as a move in the $k$-pebble game; the pebble pair moved in this turn is then marked $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$. For a blocking move, Spoiler picks $p\in [k]$ and places the $p$-th pebble in $𝒢$ on some vertex $u\in V_{𝒢}$ and in $\mathscr{H}$ on some vertex $v\in V_{\mathscr{H}}$. Duplicator next decides how to mark this pair. If Duplicator chooses $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$, then the round ends. If instead Duplicator chooses $\mathrm{𝖻𝗅𝗈𝖼𝗄𝗂𝗇𝗀}$, then the round continues and Spoiler can again choose to make either a regular or a blocking move. If $({\alpha }_{t+1},{\beta }_{t+1},c_{t+1})$ does not induce a partial isomorphism with blocking, then Spoiler wins and the game ends. Otherwise if , the game continues in round $t+2$. If $t+1=r$, then Duplicator wins.

We write $𝒢{\simeq }_{ℬ}^{k,r}\mathscr{H}$ if Duplicator has a winning strategy in the $r$-round $k$-pebble game with blocking. If $𝒢{\simeq }_{ℬ}^{k,r}\mathscr{H}$ for all $r\in \mathbb{N}$, then we write $𝒢{\simeq }_{ℬ}^k\mathscr{H}$. As for the $k$-pebble game, it will also be convenient to consider variants of the $k$-pebble game with blocking where we start from arbitrary positions or do not specify the number of rounds in advance. Note that while in the (non-blocking) $k$-pebble game it never makes sense for Spoiler to place a pebble on an already pebbled vertex, this is not the case in the $k$-pebble game with blocking.

We end the section by connecting the $k$-pebble game with blocking to the $k$-narrow Prover-Delayer game via the following lemma.

In the $k$-narrow Prover-Delayer game on $𝒳(𝒢),𝒳(\mathscr{H})$, Delayer simulates positions of the $k$-pebble game with blocking on $𝒢$, $\mathscr{H}$. Intuitively, whenever a $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$ pebble pair is placed on vertices $u$ and $v$ (and there is not already a pebble pair on $u$ and $v$), Delayer should score a point since it “does not matter” whether we map $u_0$ to $v_0$ or to $v_1$. As the round counter of the $k$-pebble game with blocking only advances when a pebble pair is marked as $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$, filling in the details is relatively straightforward. $◀$ Lemmas 4 and 9 finally connect the pebble game with blocking to tree-like refutation size.

Let $𝒢=(V_{𝒢},E_{𝒢})$ be a connected ordered graph, called a base graph, and $f:E_{𝒢}\to {𝔽}_2$ be a function, where ${𝔽}_2$ is the two-element field. From $𝒢$ and $f$ we derive the colored CFI graph $\mathrm{𝖢𝖥𝖨}(𝒢,f)$: Vertices of $𝒢$ are called base vertices. Every base vertex of $𝒢$ is replaced by a CFI gadget and gadgets of adjacent vertices are connected. The vertices of the CFI gadget for a degree $d$ base vertex $u\in V_{𝒢}$ are the pairs $(u,\overline{a})$ for all $d$-tuples $\overline{a}=(a_1,\mathrm{\dots },a_d)\in {𝔽}_2^d$ with ${\sum }_{i=1}^d{a}_i=0$. The vertex $(u,\overline{a})$ has origin $u$. Vertices inherit the color of their origin. Since every vertex of the base graph has a unique color, the vertices of each gadget form a color class of the CFI graph. For all adjacent base vertices $u,v\in V_{𝒢}$, we add the following edges between the gadgets for $u$ and $v$: Let $u$ be the $i$-th neighbor of $v$ and $v$ be the $j$-th neighbor of $u$ according to the order on $V_{𝒢}$. There is an edge between vertices $(u,\overline{a})$ and $(v,\overline{b})$ if and only if $a_i+b_j=f(\{u,v\})$, where $a_i$ is the $i$-th entry of $\overline{a}$ and $b_j$ is the $j$-th entry of $\overline{b}$. See Figure 1 for an example. We say that two functions $f,g:E_{𝒢}\to {𝔽}_2$ twist an edge $e\in E_{𝒢}$ or the edge $e\in E_{𝒢}$ is twisted by $f$ and $g$ if $f(e)\ne g(e)$. It is known that $\mathrm{𝖢𝖥𝖨}(𝒢,f)\cong ̸\mathrm{𝖢𝖥𝖨}(𝒢,g)$ if and only if $f$ and $g$ twist an odd number of edges [17].

CFI graphs are a well-studied tool to derive lower bounds for $k$-variable logic with counting or other logics, see e.g. [17, 20, 15, 18, 31]. This construction and its generalizations have also been used to derive proof complexity lower bounds on graph isomorphism in various proof systems [40, 12, 13, 32, 41, 36]. We now discuss the method of compressing CFI graphs [25]. The goal is to reduce the size of the resulting graph while essentially preserving the hardness of it. The main idea is to identify the gadgets of certain base vertices. The hardness of the resulting compressed CFI graphs heavily depends on which gadgets get identified and can be analyzed using a variant of the Cops and Robber game. We now present this framework.

Let $\equiv \subseteq V_{𝒢}^2$ be a $𝒢$-compression. It induces an equivalence relation on $\mathrm{𝖢𝖥𝖨}(𝒢,f)$ (independently of the function $f:E\to {𝔽}_2$), which we also denote by $\equiv$, via $(u,\overline{a})\equiv (v,\overline{b})$ if and only if $u\equiv v$ and $\overline{a}=\overline{b}$. Contracting all $\equiv$-equivalence classes in $\mathrm{𝖢𝖥𝖨}(𝒢,f)$ into a single vertex yields the colored graph $\mathrm{𝖢𝖥𝖨}(𝒢,f){/}_{\equiv }$: the vertices of $\mathrm{𝖢𝖥𝖨}(𝒢,f){/}_{\equiv }$ are the $\equiv$-equivalence classes $u{/}_{\equiv }:=\{w\in V_{\mathrm{𝖢𝖥𝖨}(𝒢,f)}|w\equiv u\}$, and $u{/}_{\equiv }$ and $v{/}_{\equiv }$ are adjacent if there are $u^{\prime }\equiv u$ and $v^{\prime }\equiv v$ such that $u^{\prime }$ and $v^{\prime }$ are adjacent in $\mathrm{𝖢𝖥𝖨}(𝒢,f)$. Observe that $\mathrm{𝖢𝖥𝖨}(𝒢,f){/}_{\equiv }$ is loop-free by the condition on $\equiv$ that equivalent vertices of $𝒢$ are non-adjacent. The color of a $\equiv$-equivalence class in $\mathrm{𝖢𝖥𝖨}(𝒢,f){/}_{\equiv }$ is the minimal color of one of its members in $\mathrm{𝖢𝖥𝖨}(𝒢,f)$. To obtain reasonable graphs, $f$ has to be compatible with the compression $\equiv$ in the following sense.

Precompressed CFI graphs can also be seen as edge-colored graphs that use two colors for the edges – one the the regular edges and one for the equivalence relation. An example is shown in Figure 1. The round number of the bijective $k$-pebble game (a variant of the $k$-pebble game that characterizes equivalence of $k$-variable first order logic with counting quantifiers) on precompressed and compressed CFI graphs are almost equal [25]. The corresponding statement for the $k$-pebble game with blocking is proved similarly.

The ability of the bijective $k$-pebble game to distinguish non-isomorphic CFI graphs is captured by the $k$-Cops and Robber game [37, 25]. A variant of this game – the compressed $k$-Cops and Robber game – provides lower bounds for compressed CFI graphs. To see this, we consider isomorphisms of CFI graphs. These always twist an even number of edges and can be described in terms of paths in the base graphs by twistings (defined below). Moreover, if these paths are compatible with the compression, they induce isomorphisms of compressed CFI graphs. For ordered base graphs, these twistings correspond one-to-one with isomorphisms of the (compressed) CFI graphs.

To obtain a reasonable notion of twistings for isomorphisms of compressed CFI graphs, the twistings have to be compatible with the compression. For more details on (compressed) CFI graphs, their isomorphisms, and twistings, we refer to the original paper [25].

The compressed $k$-Cops and Robber game [25] is played on a base graph $𝒢$ and a $𝒢$-compression $\equiv$. The Cops Player places cops on up to $k$ $\equiv$-equivalence classes and the robber is placed on one edge of $𝒢$. Initially, only the robber is placed. The game proceeds in rounds:

1. 1.

   The Cops Player picks up a cop and announces a new $\equiv$-equivalence class $C$ for this cop.

2. 2.

   The robber moves. To move from the current edge $e_1$ to another edge $e_2$, the robber has to provide a $\equiv$-compressible $𝒢$-twisting that only twists the edges $e_1$ and $e_2$ and that fixes every vertex contained in a cop-occupied $\equiv$-equivalence class.

3. 3.

   The cop that was picked up in Step 1 is placed on $C$. The next round starts.

The robber is caught if the two endpoints of the robber-occupied edge are contained in cop-occupied $\equiv$-classes. The cops have a winning strategy in $r$ rounds, if they can catch the robber in $r$ rounds independently of the moves of the robber. Similarly, the robber has a strategy for the first $r$ rounds if the robber can avoid being caught for $r$ rounds independently of the moves of the Cops Player. The winner of the compressed game depends on the initial position of the robber. This game yields lower bounds for the (bijective) $k$-pebble game:

To obtain lower bounds for the $k$-pebble game with blocking, we add “roadblocks” to the compressed Cops and Robber game and prove a blocking analogue of Lemma 17. Let $𝒢$ be an ordered graph. A roadblock for a vertex $u\in V_{𝒢}$ is a nonempty set $N\subseteq \{(u,v)|\{u,v\}\in E_{𝒢}\}$ of (directed) edges incident to $u$ of even size. A $𝒢$-twisting $T$ avoids a roadblock $N$ for a vertex $u$ if $T\cap \{u\}\times V_{𝒢}\ne N$. In particular, $T$ may contain a strict superset or subset of $N$. If $T$ does not avoid $N$, then $T$ uses $N$. A roadblock for a $\equiv$-equivalence class $C$ is a nonempty set $N\subseteq [d]$ of even size, where $d$ is the unique degree of the vertices in $C$. A $𝒢$-twisting $T$ avoids the roadblock $N$ on $C$ if, for every vertex $u\in C$, the twisting $T$ avoids the roadblock $N_u:=\{(u,v_i)|i\in N\}$ for $u$, where $v_i$ denotes the $i$-th neighbor of $u$. If $T$ is $\equiv$-compressible and does not avoid $N$, then $T$ uses $N_u$ for every vertex $u\in C$; we say that $T$ uses $N$. Let $M\subseteq [d]$ be the set of all $i\in [d]$ such that $T$ contains the edge to the $i$-th neighbor of some and, since $T$ is $\equiv$-compressible, of every $u\in C$. We write $T(N)$ for the symmetric difference of $N$ and $M$.

The compressed and blocking $k$-Cops and Robber game is played on a base graph $𝒢$ and a $𝒢$-compression $\equiv$. The Cops Player controls cops and roadblocks. The total number of cops and roadblocks is $k$ but the number of each may vary during the game. Cops and roadblocks are placed on $\equiv$-equivalence classes and the robber is located on an edge. Initially, only the robber is placed. A round of the game proceeds as follows: The Cops Player picks up a cop or a roadblock and can choose to play a cop move or a blocking move.

1. 1.

   A cop move proceeds similarly to the non-blocking game. First, the Cops Player announces a $\equiv$-equivalence class $C$. Next, the robber moves. To move from an edge $e_1$ to another edge $e_2$, the robber provides a $\equiv$-compressible $𝒢$-twisting $T$ that only twists the edges $e_1$ and $e_2$, fixes every vertex contained in a cop-occupied $\equiv$-equivalence class, and avoids every roadblock. Afterwards, a cop is placed on the announced class $C$.

2. 2.

   For a blocking move, the Cops Player announces a $\equiv$-equivalence class $C$ and a roadblock $N$ for $C$. Next, the robber moves with a $\equiv$-compressible $𝒢$-twisting $T$ as in the cop move. If $T$ uses $N$, then a cop is placed on $C$. Otherwise, the roadblock $N$ is placed on $C$.

3. 3.

   The existing roadblocks are updated. If a roadblock $N^{\prime }$ is placed on a class $C^{\prime }$, then it is replaced by the roadblock $T(N^{\prime })$ on $C^{\prime }$. Because in both a cop and a blocking move $T$ avoids all roadblocks, $T(N^{\prime })$ will always be a nonempty set. If a roadblock was placed in this move, the Cops Player can again choose to play either a cop or a blocking move without increasing the round counter.

The notion of the robber being caught or having a strategy for the first $r$ round is the same as in the non-blocking game. As in the non-blocking game, the starting edge of the robber is important. The following lemma is proved similarly to Lemma 17.

The $\equiv$-compressible twistings of the robber induce isomorphisms of the compressed CFI graphs, which respect all currently placed pebbles. These are used to move the twisted edge (“the robber”) away from the pebbles. Cops correspond to $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$ pebble pairs and roadblocks to $\mathrm{𝖻𝗅𝗈𝖼𝗄𝗂𝗇𝗀}$ ones. The case distinction in Point 2 whether a cop roadblock is placed ensures that in a blocking move in the pebble game with blocking the pebble pair gets marked as $\mathrm{𝗋𝖾𝗀𝗎𝗅𝖺𝗋}$ or $\mathrm{𝖻𝗅𝗈𝖼𝗄𝗂𝗇𝗀}$ consistently with the current isomorphism. Updating the roadblocks in Point 3 corresponds to applying the isomorphism induced by the twisting $T$ to them.

Let $k\ge 3$ and $1\le t\le \frac{2}{5}k-1$. By Theorem 25, for all $n\in \mathbb{N}$, there are graphs $𝒢$ and $\mathscr{H}$ of color class size $8$ and order $\mathrm{\Theta }(n)$ such that $𝒢{\simeq ̸}^{k+1}\mathscr{H}$ and $𝒢{\simeq }_{ℬ}^{k+t,\mathrm{\Omega }(n^{k/(t+2)})}\mathscr{H}$. It is easy to see that $𝒳(𝒢)$ and $𝒳(\mathscr{H})$ have color class size $16$. By Theorem 5 and Lemma 6, there is a $k$-narrow resolution refutation for $\mathrm{𝖨𝖲𝖮}(𝒳(𝒢),𝒳(\mathscr{H}))$. Moreover, from Lemma 9 it follows that Delayer has a strategy to score $\mathrm{\Omega }(n^{k/(t+1)})$ points in the $(k+t)$-narrow Prover-Delayer game on $𝒳(𝒢),𝒳(\mathscr{H})$. Therefore, by Lemma 4, the result follows. $◀$ Theorem 1 is the case $t=1$ of Theorem 26. We now lift Theorem 26 to usual resolution (without the narrow resolution rule). First, if $𝒢$ and $\mathscr{H}$ have color class size $c$, then we can convert every $k$-narrow refutation of $\mathrm{𝖨𝖲𝖮}(𝒢,\mathscr{H})$ into a (usual) refutation of $\mathrm{𝖨𝖲𝖮}(𝒢,\mathscr{H})$ of width $k+c$. Second, a width-$k$ refutation is in particular a width-$k$ narrow refutation. Theorem 2 follows immediately. Note that while Assertion 2 of Theorem 2 provides a lower bound for all $t\le \frac{2}{5}k-1$, Assertion 1 only guarantees a refutation of width $k+16$. Therefore, the existing refutation must be large only for $k\ge 45$ and $17\le t\le \frac{2}{5}k-1$ .

We established a new super-critical (narrow) width vs. tree-like size trade-off on graph isomorphism formulas for resolution. The lower bound of $2^{\mathrm{\Omega }(n^{k/2})}$ obtained for $t=1$ in Theorems 2 and 26 is close to the upper bound of $2^{n^k}$ for the tree-like size of resolution of (narrow) width $k$. We exploited a compressed variant of the CFI graphs and round number lower bounds in the $k$-pebble game on them. However, we had to move from the $k$-pebble game to the $k$-pebble game with blocking, and reprove the round number lower bounds in this setting. This raises the question of whether there is a generic translation from round number lower bounds in the $k$-pebble game to tree-like size resolution lower bounds. Another question is whether the decrease in the robustness in the trade-off from $2k$ in [19] to $\frac{7}{5}k$ in Theorem 26 is necessary. More broadly, we ask for a more robust compression or trade-off that can be applied to a much wider range than $2k$.