Cited By
View all- Torán JWörz F(2024)Cutting Planes Width and the Complexity of Graph Isomorphism RefutationsACM Transactions on Computational Logic10.1145/367712125:4(1-25)Online publication date: 18-Jul-2024
Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas
Article No.: 23, Pages 1 - 25
Abstract
We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution.
Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the minimum number of variables needed to distinguish two graphs with n vertices each, then there is an nO(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2k-1 and k for the treelike resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp (Ω (k2/n)) for the case of colored graphs with constant color class sizes.
Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.
1 Introduction
In an attempt to give a logical characterization of polynomial-time decidable graph properties, as well as a description of general classes of graph canonization algorithms, Immerman identified certain fragments of first-order logic suitable for expressing graph properties [26, 27]. In this setting, for such a logic \(\mathscr{L}\) of first-order logic sentences, two graphs G and H are \(\mathscr{L}\)-equivalent, denoted by \(G \equiv _{\mathscr{L}} H\), if for all sentences \(\psi \in \mathscr{L}\) it holds that \(G \vDash \psi \Longleftrightarrow H \vDash \psi\). Immerman noticed that the number of variables needed for expressing a property is a good complexity measure and defined the k-variable fragment of first-order logic \({\mathscr{L}}_{k}\) as the set of first-order logic formulas with the edge and equality relations that use at most k different variables (possibly re-quantifying them). He also defined the stronger class \({\mathscr{C}}_{k}\) by adding counting quantifiers to the class \({\mathscr{L}}_{k}\) and defined two pebble games for proving (non)equivalence of structures in these classes.
It was shown in Reference [9] that two graphs are \({\mathscr{C}}_{k}\)-equivalent if and only if they cannot be distinguished by the \((k-1)\)-dimensional Weisfeiler–Leman algorithm, a well-known method for testing graph isomorphism. Roughly speaking, the one-dimensional Weisfeiler–Leman algorithm, or color refinement algorithm, identifies non-isomorphic colored graphs by updating in a series of steps the original vertex colors according to the multiset of colors of their neighbors. This basic step is applied repeatedly until the coloring stabilizes. This procedure can be generalized to the k-dimensional Weisfeiler–Leman algorithm (\(k\text{-}\mathrm{WL}\)) [47, 48] by partitioning the set of k-tuples of vertices into automorphism-invariant equivalence classes (see, e.g., References [9, 28, 29] for excellent overviews of the powers and limits of this procedure).
The graph isomorphism problem (GraphIso), i.e., deciding whether two given graphs are isomorphic, has been intensively studied, as it is one of the few problems in \(\mathsf {NP}\) that is not known to be complete for this class nor to be in \(\mathsf {P}\). Also unknown is whether the problem is in \(\mathsf {co}\text{-}\mathsf {NP}\). It had been conjectured that \(\mathrm{GraphIso}\) is solvable using the k-dimensional Weisfeiler–Leman algorithm, with k being sublinear in the number of vertices of the graphs. However, this was shown to be false in the seminal work of Cai, Fürer, and Immerman [9] using the \({\mathscr{C}}_{k}\) pebble game as a central tool. The Weisfeiler–Leman method still plays a central role in the algorithmic research on \(\mathrm{GraphIso}\); for example, Babai’s celebrated algorithm for \(\mathrm{GraphIso}\) [5] uses the \(k\text{-}\mathrm{WL}\) method as a subroutine, with k being polylogarithmic in the number of vertices.
The field of proof complexity provides a different approach for studying the complexity of the \(\mathrm{GraphIso}\) problem. Roughly speaking, in this setting, one tries to find out the smallest size of a proof in a concrete system of the fact that two graphs are non-isomorphic. It holds that \(\mathrm{GraphIso}\) is in \(\mathsf {co}\text{-}\mathsf {NP}\) if and only if there is a concrete proof system with polynomial-size proofs of non-isomorphism. Similarly to the Cook–Reckhow program [11] for the unsatisfiability problem \(\mathrm{UNSAT}\), this defines a clear line of research trying to provide superpolynomial size lower bounds for refuting graph (non)isomorphism formulas in stronger and stronger proof systems. The situation is even more interesting here than in the \(\mathrm{SAT}\) case since it would not be too surprising if \(\mathrm{GraphIso}\in \mathsf {co}\text{-}\mathsf {NP}\), and this would imply the existence of polynomial-size proofs for the problem in some system. In fact, \(\mathrm{GraphIso}\) is in \(\mathsf {co}\text{-}\mathsf {AM}\) [6], a randomized version of \(\mathsf {co}\text{-}\mathsf {NP}\).
The first example of such a lower bound was given in Reference [43], where it was shown that a family of unsatisfiable formulas encoding pairs of non-isomorphic graphs in a natural way requires exponential-size resolution refutations. These graphs are based on the CFI construction from Reference [9]. The lower bound can be explained as an “encoding” of the Tseitin tautologies [45] into graph isomorphism instances. This result has been extended to stronger proof systems: In Reference [8], the authors proved linear degree lower bounds for the algebraic systems Polynomial Calculus and Positivstellensatz by studying graphs arising from Tseitin tautologies. They furthermore characterized exactly the power of the Weisfeiler–Leman algorithm in terms of an algebraic proof system lying between degree-k Nullstellensatz and degree-k Polynomial Calculus. Moreover, it has been shown in References [4, 23, 35] that the expressive power of \(k\text{-}\mathrm{WL}\) lies between the kth and \((k+1)\)-st level of the canonical Sherali–Adams LP hierarchy [41]. By the construction in Reference [9], no sublinear level of Sherali–Adams suffices to decide \(\mathrm{GraphIso}\). Again, building on the work of Reference [9], it was shown in Reference [37] and independently in Reference [10] that there exist pairs of non-isomorphic n-vertex graphs such that any Sum-of-Squares proof of non-isomorphism must have degree \(\Omega (n)\). These results imply linear lower bounds on resolution width. While resolution width lower bound for isomorphism formulas were known already [43], the advantage of the results in our article is a direct connection between resolution width and the number of variables in descriptive complexity.
Very recently, a different view was considered by Schweitzer and Seebach [40] by introducing symmetry rules into the picture. The authors proved that resolution extended with the well-known symmetry rule SRC-2 from Krishnamurthy [33] has polynomial-size refutations for all the instances of the graph isomorphism problem for which exponential size lower bounds for (normal) resolution are known. They pointed to the search for hard instances of graph isomorphism for resolution extended with the existing symmetry rules that define the proof systems SRC-1, SRC-2, and SRC-3, a hierarchy of systems with more and more powerful symmetry rules [2, 42]. They pose the question of whether graph non-isomorphism formulas have superpolynomial resolution complexity in any of these proof systems. These are very interesting questions since finding symmetries in a formula to be able to apply Krishnamurthy’s rules is closely related to graph isomorphism. Finding lower bounds for non-isomorphism in a system with symmetry rules can be seen as finding lower bounds for proving non-isomorphism with the help of an “isomorphism subroutine.”
1.1 Our Results
We show a strong connection between the \({\mathscr{L}}_{k,m}\) fragment of first-order logic and the propositional resolution proof system. This is done by proving that the number of variables and the quantifier depth simultaneously needed to distinguish two graphs G and H in first-order logic exactly corresponds to the width and the depth of a narrow resolution refutation of the unsatisfiable formula \(\mathrm{ISO}(G,H)\) stating that the graphs are isomorphic (Theorem 3.3). Narrow resolution [20] is a slight variation of (normal) resolution that allows a distinction by cases rule, allowing to deal with the inconveniences of having long clauses in the formula. As in the case of the clause width measure [7], narrow width allows, in our case, to derive upper and lower bounds for the size of the resolution refutations of non-isomorphism. Furthermore, we show that narrow width also provides a lower bound for the clause space needed in resolution, as is the case for the standard width measure. In particular, we prove that for any pair of non-isomorphic graphs \((G, H)\) with n vertices each and \(k \in \mathbb {N}\):
•
If \(G \not\equiv _{{\mathscr{L}}_{k}} H\), then there is a (normal) resolution refutation of \(\mathrm{ISO}(G,H)\) of size \(n^{\mathrm{O}(k)}\); this implies, using known results, that the average case size-complexity for refuting \(\mathrm{ISO}(G,H)\) in resolution is \(n^{\mathrm{O}(\log n)}\);
•
if \(G \equiv _{{\mathscr{L}}_{k}} H\), then every treelike resolution refutation of \(\mathrm{ISO}(G,H)\) has size \(\ge 2^k\);
•
if \(G \equiv _{{\mathscr{L}}_{k}} H\), then every (normal) resolution refutation of \(\mathrm{ISO}(G,H)\) has clause space \(\ge k + 1\); and
•
for a pair of graph colorings \((\lambda , \mu)\) with \((G, \lambda) \equiv _{{\mathscr{L}}_{k}} (H, \mu)\), every (normal) resolution refutation of \(\mathrm{ISO}(G,H)\) has size \({\exp } (\Omega (k^2/m))\), where \(m := \sum _{v \in V_G} |\text{ color-class}_H(v)|\).
The last result allows us to directly derive resolution size lower bounds from Immerman’s pebble game for \({\mathscr{L}}_{k}\). For example, when the color classes defined by the colorings have constant size and \(G \equiv _{{\mathscr{L}}_{k}} H\) for \(k \in \Omega (n)\), then any resolution refutation of \(\mathrm{ISO}(G,H)\) must have size \({\exp } (\Omega (n))\). We use this last result to prove that a version of the multipede graphs defined in Reference [12] has exponential resolution size lower bounds. We also observe that Krishnamurthy’s SRC-1 symmetry rule cannot be applied to the isomorphism formulas for asymmetric graphs and conclude that the resolution size lower bound for the multipede graphs also holds for the SRC-1 system. This provides the first example of a class of graphs whose isomorphism formulas have exponential size lower bounds for the size of resolution refutations with one of the symmetry rules, thus solving a question from Reference [40].
1.2 Organization of This Article
The rest of this article is organized as follows. In Section 2, we introduce resolution complexity measures, narrow resolution, and Krishnamurthy’s symmetry rules, as well as the graph isomorphism formulas and Immerman’s pebble game. Then, in Section 3, we prove the connection between narrow resolution width and \({\mathscr{L}}_{k}\). This yields the upper bounds on resolution size and the lower bounds on treelike resolution size for refuting \(\mathrm{ISO}(G,H)\). The exponential lower bound for the size of SRC-1 graph isomorphism formula refutations is shown in Section 4. Finally, in Section 5, clause space lower bounds for proving graph non-isomorphism in resolution are shown.
2 Preliminaries
We let \(\mathbb {N}\) denote the set of positive integers. For \(n \in \mathbb {N}\), we let \([n] := \lbrace k \in \mathbb {N} \,\mid \, 1 \le k \le n \rbrace\).
A literal \(\ell\) over a Boolean variable x is either x itself or its negation \(\overline{x} := \lnot x\). For a literal \(\ell\), we put \(\overline{\ell } := \lnot x\) if \(\ell = x\) and \(\overline{\ell } := x\) if \(\ell = \lnot x\) and call \(\ell\) and \(\overline{\ell }\) complementary literals. A clause \(C = (\ell _1 \vee \dots \vee \ell _k)\) is a (possibly empty) disjunction of literals \(\ell _i\). We let the symbol \(\square\) denote the contradictory empty clause (the clause without any literals). A CNF formula \(F = C_1 \wedge \dots \wedge C_m\) is a conjunction of clauses. It is often advantageous to think of clauses as sets of literals and CNF formulas as sets of clauses (i.e., sets of sets). The set of variables occurring in a clause C will be denoted by \(\mathrm{Vars}({C})\). The notion of the set of variables in a clause is extended to CNF formulas by taking unions. An assignment/restriction \({\alpha }\) for a CNF formula F is a function that maps some subset of \(\mathrm{Vars}({F})\), denoted by \(\operatorname{Dom}(\alpha)\), to \(\lbrace 0,1 \rbrace\). We will consider the graph of this function and call this set also an assignment. We let \(|\alpha | := | \operatorname{Dom}(\alpha) |\) be the size of \(\alpha\). We denote the empty assignment with \(\varepsilon\). By naturally extending \(\alpha\) by the definition \(\alpha (\overline{x}) := \overline{\alpha (x)}\), we can define the result of applying \(\alpha\) to C, which we denote by \(C|_{{\alpha }}\): One deletes all occurrences of literals \(\ell\) from C, where \({\alpha }(\ell)=0\); if there is a literal \(\ell \in C\) with \({\alpha }(\ell)=1\), then \(C|_{{\alpha }} = 1\). The notation \(F|_{{\alpha }}\) denotes the formula, where all clauses containing a literal \(\ell\) with \(\alpha (\ell) = 1\) are deleted and each remaining clause C is replaced by \(C|_{{\alpha }}\). If \(\ell\) is a literal that is not assigned by \(\alpha\), and \(b \in \lbrace 0,1 \rbrace\), then \(\alpha \lbrace \ell =b \rbrace\) denotes the extension of \(\alpha\) with \((\alpha \lbrace \ell = b \rbrace)(x) := \alpha (x)\) for all \(x \not\in \lbrace \ell , \overline{\ell } \rbrace\) and \((\alpha \lbrace \ell = b \rbrace)(\ell) = b\) as well as \((\alpha \lbrace \ell = b \rbrace)(\overline{\ell }) = 1 - b\).
2.1 Resolution and Complexity Measures
If \(B \vee x\) and \(C \vee \overline{x}\) are clauses, then the resolution rule allows the derivation of the clause \(R := B \vee C\). In the resolution rule, we call \(B \vee x\) and \(C \vee \overline{x}\) the parents and R the resolvent.
A resolution derivation of a clause D from a CNF formula F (denoted by \({{\pi } :{F} \, {\mathrel {\mathop \vdash }}\, {D}}\)) is a sequence of clauses \(\pi = (C_1, \dots , C_t)\) such that \(C_t= D\), and each clause \(C_i\), for \(i\in [t]\), is
(1)
either an axiom clause \(C_i\in F\),
(2)
or is derived from clauses \(C_j\) and \(C_k\) with \(j \lt k \lt i\) by the resolution rule.
A derivation of the empty clause from an unsatisfiable CNF formula F is called refutation.
To every refutation \(\pi\), we can associate a refutation DAG \(G_{\pi }\): The clauses of the refutation label the vertices of the DAG, and for every application of the resolution rule, we include edges from the parents to the resolvent. We say that a resolution refutation \(\pi\) is treelike if \(G_{\pi }\) is a tree.
The size of a resolution refutation \(\pi = (C_1, \dots , C_t)\), denoted \(\mathrm{Size}(\pi)\), is defined to be the number of vertices in the underlying refutation DAG \(G_{\pi }\).
The width of a clause C is defined by \(\text{Width}(C) := | C |\), whereas the width of a formula F is given by \(\text{Width}(F) := \max _{C \in F} \text{Width}(C)\). Similarly, we put \(\text{Width}({\pi }) := \max _{i\in [t]} \text{Width}({C_{i}})\) for a refutation \(\pi = (C_1,\dots ,C_t)\).
The depth \(\mathrm{Depth_{}}(\pi)\) of a refutation \(\pi\) is the length of a longest path in the underlying refutation DAG \(G_{\pi }\).
We will also use the clause space measure for resolution. Intuitively, the clause space of a refutation \(\pi\) is the maximum number of clauses that need to be kept in memory simultaneously when verifying the proof \(\pi\). For a more formal definition of clause space, we consider the following definition of the resolution proof system from References [1, 16].
A resolution refutation \({{\pi } :{F} \, {\mathrel {\mathop \vdash }}\, {\square }}\) of an unsatisfiable CNF formula F is a sequence of memory configurations (sets of clauses) \(\pi = (\mathbb {M}_0,\dots ,\mathbb {M}_{t})\) such that \(\mathbb {M}_0 = \varnothing\), \(\square \in \mathbb {M}_{t}\) and for each \(i\in [t]\), the configuration \(\mathbb {M}_{i}\) is obtained from \(\mathbb {M}_{i-1}\) by applying exactly one of the following rules:
Axiom Download:
\(\mathbb {M}_i= \mathbb {M}_{i-1} \cup \lbrace C\rbrace\) for some axiom \(C \in F\).
Erasure:
\(\mathbb {M}_i= \mathbb {M}_{i-1} \setminus \lbrace C\rbrace\) for some \(C \in \mathbb {M}_{i-1}\).
Inference:
\(\mathbb {M}_i= \mathbb {M}_{i-1} \cup \lbrace R\rbrace\) for some resolvent R inferred from clauses \(C_1, C_2 \in \mathbb {M}_{i-1}\) by the resolution rule.
The clause space of a memory configuration \(\mathbb {M}\) is defined as \(\mathrm{CS_{}}(\mathbb {M}) := | \mathbb {M}|\), i.e., the number of clauses in \(\mathbb {M}\). The clause space of a refutation \(\pi = (\mathbb {M}_0,\dots ,\mathbb {M}_{t})\) is defined by \(\mathrm{CS_{}}(\pi) := \max _{i\in [t]} \mathrm{CS_{}}(\mathbb {M}_i)\).
2.1.1 Narrow Resolution, Narrow Width, and Narrow Depth.
The standard definition of width is not well suited for proving size lower bounds for formulas having large widths themselves (cf. Reference [7]), like the isomorphism formulas (cf. Section 2.2). A more natural way to deal with the width concept in such formulas was introduced by Galesi and Thapen [20] together with the concept of narrow resolution that does not take into account the width of the axioms.
A narrow resolution derivation of a clause D from a CNF formula F is a sequence of clauses \(\pi = (C_1, \dots , C_{t})\) such that \(C_{t} = D\), and for each \(i \in [t]\), the clause \(C_i\) is obtained by Rule (1) or (2) of a (normal) resolution derivation (cf. Definition 2.1) or by the following distinction by cases step:
(3)
If \((B \vee \ell _1 \vee \dots \vee \ell _m) \in F\), and if there are clauses \(C_{j_1} = (A_1 \vee \overline{\ell _1})\), \(\dots\), \(C_{j_m} = (A_m \vee \overline{\ell _m})\) with \(j_1 \lt \dots \lt j_m \lt i\), then we can derive \(C_{i} := (B \vee A_1 \vee \dots \vee A_m)\) in one step.
The definition here is a natural generalization of the original one in Reference [20], since, in Rule (3), we do not require all the \(A_j\) clauses to coincide, and we allow for a subclause B to be present in the axiom clause (note, however, that the width of each \(A_j\) and B will be counted). Moreover, the literals \(\ell _i\) can be positive or negated variables, and not just positive as in Reference [20]. The modifications allow an exact characterization of the number of pebbles and the number of moves needed in Immerman’s game in terms of the width and depth measures in narrow resolution, as shown in Theorem 3.3. We introduce these notions next.
The refutation DAG of a narrow resolution naturally corresponds to the graph where for each application of Rule (3), edged are included from the clauses \((B \vee \ell _1 \vee \dots \vee \ell _m), C_{j_1}, \dots , C_{j_m}\) to \(C_i\). Again, \(\mathrm{Size}(\pi)\) of a narrow refutation \(\pi\) is defined as the number of vertices in its refutation DAG.
For a narrow resolution derivation \(\pi = (C_1, \dots , C_{t})\), we let \(\mathrm{N\text{-}Width}(\pi)\) be the minimum k such that \(\text{Width}({C_{i}}) \le k\) for all \(i \in [t]\) with \(C_i \not\in F\). We also define \(\mathrm{N\text{-}Depth}(\pi)\) as the length of the longest path in the underlying narrow refutation graph.
For a measure \(\mathcal {C} \in \lbrace {\mathrm{Size}}_{}, {\mathrm{Width}}_{}, {\mathrm{Depth}}_{}, {\mathrm{CS}}_{} \rbrace\), by taking the minimum over all (normal) refutations \(\pi\) of an unsatisfiable formula F, we define \({\mathcal {C}}_{}{(F \mathrel {\mathop \vdash }\!\square)} := \min _{{{\pi } :{F} \, {\mathrel {\mathop \vdash }}\, {\square }}} \mathcal {C}(\pi)\) as the size, width, depth, and clause space of refuting F in resolution, respectively.
Similarly, for a measure \(\mathcal {C} \in \lbrace {\mathrm{N\text{-}Width}}_{}, {\mathrm{N\text{-}Depth}}_{} \rbrace\), we define \({\mathcal {C}}_{}{(F \mathrel {\mathop \vdash }\!\square)} := \min _{{{\pi } :{F} \, {\mathrel {\mathop \vdash }}\, {\square }}} \mathcal {C}(\pi)\) by taking the minimum over all narrow refutations \(\pi\) of F and call it the narrow width, and narrow depth of refuting F, respectively.
Observe that there can be a significant difference between width and depth and their narrow counterparts. For example, the formula consisting of the clause \((x_1 \vee \dots \vee x_n)\) and one clause for each negated variable \(\overline{x_i}\), has width and depth n but narrow width 0 and narrow depth 1. For our results, we do not need to define versions for narrow resolution complexity measures different from width and depth.
2.1.2 The Weakening Rule.
Weakening is a further proof step introduced to simplify some of the resolution proofs:
(4)
in a resolution derivation \(\pi =(C_1,\dots , C_t)\), a clause \(C_i\) can be derived by weakening of a clause \(C_j\) with \(j \lt i\), meaning that \(C_i\supseteq C_j\).
The refutation DAG for a resolution using weakening is defined by additionally including edges from the original to the weakened clause for every application of the weakening rule. The complexity measures \(\textrm {Size}\), \(\textrm {Width}\), \(\textrm {N-Width}\), \(\textrm {Depth}\), and \(\textrm {N-Depth}\) can be defined for refutations using weakening, as was described above. It is well known that weakening does not affect the complexity of a resolution proof. For completeness, we show that this is also true for narrow resolution.
Let F be a formula in CNF. If there is a derivation \(\pi\) of a clause C from F in narrow resolution with weakening, then there is a narrow resolution derivation \(\tau\) of a clause D from F, where \(D \subseteq C\), using no weakening steps with \(\mathrm{Size}(\tau) \le \mathrm{Size}(\pi)\), \(\mathrm{N\text{-}Width}(\tau) \le \mathrm{N\text{-}Width}(\pi)\), and \(\mathrm{N\text{-}Depth}(\tau) \le \mathrm{N\text{-}Depth}(\pi)\).
Let \(\pi = (C_1, \ldots , C_t)\) with \(C_t = C\). We extract a narrow resolution refutation without weakening, \(\tau = (D_1, \ldots , D_t)\) with \(D_t = D \subseteq C\), from the clauses in \(\pi\). Each clause \(D_i \subseteq C_i\) and it is defined inductively on \(i \in [t]\) as follows:
•
if \(C_i\) is an axiom in F, then \(D_i = C_i\);
•
if \(C_i\) is the resolvent of \(C_j\) and \(C_k\) on variable x, with \(x \in C_j\) and \(\overline{x} \in C_k\), then:
–
if \(x \in D_j\) and \(\overline{x} \in D_k\), then \(D_i\) is the resolvent of \(D_j\) and \(D_k\) on variable x;
–
otherwise, \(D_i\) is one of the clauses \(D_j,D_k\) that does not contain variable x.
•
if \(C_i\) is the narrow resolvent of the axiom \(C_j \in F\) and the clauses \(C_{j_1}, \dots , C_{j_m}\) on variables \(x_{j_1}, \dots , x_{j_m}\), then:
–
if for every \(k \in [m]\), \(x_{j_k}\) is a variable in \(D_{j_k}\), then \(D_i\) is the narrow resolvent of \(D_j \subseteq C_i\) and \(D_{j_1}, \dots , D_{j_m}\);
–
otherwise \(D_i\) is any of the clauses \(D_{j_1}, \dots , D_{j_m}\) that does not contain the corresponding \(x_{j_k}\)-variable.
•
if \(C_i\) is obtained by weakening from \(C_j\), say, \(C_i = (C_j \vee B)\), then \(D_i = D_j\).
By induction on i, we can observe that each clause \(D_i\) is contained in \(C_i\); therefore, its width cannot be larger than that of \(C_i\). If \(C_t = \square\), then \(D_t\) is also the empty clause. After removing duplicate clauses from the sequence \((D_1, \dots , D_t)\), we have a narrow resolution derivation for D.□
Observe that in the above proof, weakening steps are removed by repeating a clause, and therefore, they disappear when removing repetitions. This means that for giving an upper bound on the resolution depth, instead of transforming a proof with weakening into one without the rule as described, we can also measure the depth in the proof with weakening, considering that the weakening steps do not contribute to the depth measure.
2.1.3 Krishnamurthy’s Symmetry Rules.
Krishnamurthy [33] observed that symmetries arise naturally in proofs of combinatorial principles and suggested some rules to simplify such proofs.
Let L be a finite set of complementary literals. Then, a bijective mapping \(f:L \rightarrow L\) is called a renaming if for every \(\ell \in L\) we have \(\overline{f(\ell)} = f(\overline{\ell })\). For a clause \(C \subseteq L\) and a renaming f, we set \(f(C) := \lbrace f(\ell) \,\mid \, \ell \in C \rbrace\). For a CNF formula F with \(\mathrm{Lits}({F}) := \bigcup _{C \in F} C \subseteq L\), we put \(f(F) := \lbrace f(C) \,\mid \, C \in F \rbrace\).
Let F be a CNF formula and C a clause that can be derived by a proof \({{\pi } :{F^\prime } \, {\mathrel {\mathop \vdash }}\, {C}}\) from a subformula \(F^\prime \subseteq F\). If there exists a renaming \(f:\mathrm{Lits}({F}) \rightarrow \mathrm{Lits}({F})\) with \(f(F^\prime) \subseteq F\), then the local symmetry rule with complementation allows the derivation of \(f(C)\) from C in one step in the extended proof system. If we have the additional restriction \(F^\prime = F\), then we speak of the global symmetry rule with complementation. Adding the global or local rule, respectively, to the proof system resolution (i.e., we consider proofs in which each clause is inferred by resolution from two clauses listed earlier in the proof or by the respective symmetry rule from one clause earlier in the proof) yields the proof systems SRC-1 and SRC-2.
Allowing also to use so-called dynamic symmetries, i.e., symmetries in the clauses already resolved, and not restricting ourselves to symmetries in the original axioms, one can define the proof system SRC-3. We refer to Reference [42].
2.2 Graph Isomorphism and GI Formulas
An (undirected) graph is a tuple \(G=(V_G, E_G)\), where \(V_G\) is a finite set of vertices and \(E_G \subseteq \binom{V_G}{2} =: \mathscr{E}\) is the set of edges. For a graph G, we let \(\overline{G} := (V_G, \mathscr{E} \setminus E_G)\) be the complement graph of G. With \(K_n\) we denote the complete graph with n vertices. Given two graphs \(G = (V_G, E_G)\) and \(G^\prime =(V_{G^\prime }, E_{G^\prime })\) with disjoint vertex sets, we let the disjoint graph union \(G \uplus G^\prime\) be the graph with vertex set \(V_G \uplus V_{G^\prime }\) and edge set \(E_G \uplus E_{G^\prime }\).
A colored graph \((G, \lambda)\) is a graph G together with a function \(\lambda :V_G \rightarrow \mathcal {C}\), called coloring, where \(\mathcal {C}\) is some set of colors. We treat every uncolored graph as a monochromatic graph.
Two colored graphs \((G,\lambda)\) and \((H,\mu)\) are isomorphic, denoted by \((G,\lambda) \cong (H,\mu)\), if there is a color- and edge-respecting bijection \(\varphi :V_G \rightarrow V_H\), called (color-preserving) isomorphism from G to H, i.e., \(\lbrace u,v \rbrace \in E_G \Longleftrightarrow \lbrace \varphi (u), \varphi (v) \rbrace \in E_H\) and \(\lambda (v) = \mu (\varphi (v))\) holds for all \(u,v \in V_G\). An automorphism of a colored graph \((G, \lambda)\) is an isomorphism from \((G, \lambda)\) to \((G, \lambda)\). We denote by \(\mathrm{Iso}(G,H)\) the set of isomorphisms between G and H and by \(\mathrm{Aut}(G)\) the set of automorphisms of G.
We refer to Figure 1 for an example of non-isomorphic graphs. Every coloring \(\lambda :V_G \rightarrow \mathcal {C}\) of a graph G induces a partition of \(V_G\): For a color \(c \in \operatorname{Im}(\lambda)\), we call \(\lambda ^{-1}(c) \subseteq V_G\) a color class of G. The color class size of G is the cardinality of its largest color class. It is known that the \(\mathrm{GraphIso}\) problem can be solved in polynomial time when the color classes have constant size [19].
Fig. 1.
We encode instances of the \(\mathrm{GraphIso}\) problem as Boolean formulas. As explained below, the formulas used here are a slight modification of those in Reference [43]. Throughout the article, we will consider only isomorphism formulas corresponding to pairs of graphs having the same number of vertices.
Let \(G=(V_G,E_G)\) and \(H=(V_H,E_H)\) be two graphs with \(V_G = \lbrace v_1, \dots , v_n \rbrace\) and \(V_H = \lbrace w_1, \dots , w_n \rbrace\). The formula \(\mathrm{ISO}(G,H)\) is defined by the following clauses:
Type 1 clauses:
For every \(i \in [n]\), we include the clause \((x_{i,1} \vee x_{i,2} \vee \dots \vee x_{i,n})\) indicating that vertex \(v_i \in V_G\) is mapped to some vertex in \(V_H\); and for every \(j \in [n]\), we include the clause \((x_{1,j} \vee x_{2,j} \vee \dots \vee x_{n,j})\) indicating that vertex \(w_j \in V_H\) is the image of some vertex in \(V_G\).
Type 2 clauses:
For every \(i,j,k \in [n]\) with \(i \not= j\), we include the clause \((\overline{x_{i,k}} \vee \overline{x_{j,k}})\) indicating that no two different vertices are mapped to the same one; and for every \(i,j,k \in [n]\) with \(j \not= k\), the clause \((\overline{x_{i,j}} \vee \overline{x_{i,k}})\) indicating that the variables encode a function.
Type 3 clauses:
For every \(i,j,k,\ell \in [n]\) with \(i \lt j\) and \(k \not= \ell\) with \(\lbrace v_i,v_j \rbrace \in E_G \Leftrightarrow \lbrace v_k,v_{\ell } \rbrace \not\in E_H\), we include the clause \((\overline{x_{i,k}} \vee \overline{x_{j,\ell }})\) expressing the adjacency relation (an edge cannot be mapped to a non-edge and vice versa).
The formula \(\mathrm{ISO}(G,H)\) has \(n^2\) variables and \(\mathrm{O}(n^4)\) clauses. The clauses of Type 2 and Type 3 have width 2, while the clauses of Type 1 have width n.
Clearly, these formulas are satisfiable if the corresponding graphs are isomorphic. In the original definition of the \(\mathrm{ISO}(G,H)\) formulas [43], the second possibility of Type 1 and Type 2 clauses was not considered. The formulas with and without these clauses are equivalent under satisfiability. We include these clauses here to obtain an exact characterization of Immerman’s pebble game. Including these clauses can only make the lower bounds for the resolution of these formulas for non-isomorphic graphs stronger. The situation is similar to that for other principles, like the Pigeon-Hole-Principle, where the formulas with the additional Type 1 and Type 2 clauses are called onto-functional-PHP formulas (see, e.g., Reference [39]). We remark that \(\mathrm{PHP}^{n+1}_{n}\) has exponential-size resolution proofs [25], but as noticed in References [33, 46], polynomial-size proofs in SRC-1.
An advantage of the isomorphism formulas is that one can express colorings of the involved graphs G and H as partial assignments of the variables.
Let G and H be as in Definition 2.12 and let \(\lambda :V_G \rightarrow \mathcal {C}\) and \(\mu :V_H \rightarrow \mathcal {C}\) be two graph colorings. Set \(\rho := \lbrace x_{i,j} = 0 \,\vert \, i,j \in [n] \text{ with } \lambda (i) \ne \mu (j) \rbrace .\) Define the ISO-formula for the colored graphs as \(\mathrm{ISO}_{\lambda ,\,\mu }(G,H) := \mathrm{ISO}(G,H)|_{\rho }.\)
Observe that while every coloring can be represented by a restriction, a restriction is just a partial assignment, and it does not always encode a coloring. A coloring can drastically reduce the number of variables in the isomorphism formula. We will later make use of this fact. It is not hard to see that we have \(\mathrm{ISO}_{\lambda ,\,\mu }(G,H) \in \mathrm{UNSAT}\Longleftrightarrow (G,\lambda) \not\cong (H,\mu)\).
Since every pair of colorings \((\lambda , \mu)\) of a pair of graphs \((G, H)\) can be encoded as a restriction \(\rho\) of the formula \(\mathrm{ISO}(G,H)\) as explained, a lower bound on the size of a resolution refutation of the ISO\(_{\lambda ,\,\mu }\)-formula for colored graphs also holds for the ISO-formula of the corresponding monochromatic graphs.
It is illustrative to contrast the \(\mathrm{ISO}_{\lambda ,\,\mu }\)-formulas with the \(\mathrm{ListIso}\) problem that asks, given two graphs G and H, where each vertex \(v \in V_G\) is equipped with a list \(\mathfrak {L}(v) \subseteq V_H\), if there exists an isomorphism \(\varphi :V_G \rightarrow V_H\) such that \(\varphi (v) \in \mathfrak {L}(v)\) for all \(v \in V_G\). This problem can also be easily expressed as a satisfiability problem by restricting the first kind of Type 1 clauses to contain only the possibilities for each vertex (and doing analogously with the second kind of Type 1 clauses). However, this restriction would not encode a graph coloring in general. Moreover, \(\mathrm{ListIso}\) might be harder than \(\mathrm{GraphIso}\) as it was shown in Reference [34] (see also Reference [31]) that this problem is \(\mathsf {NP}\)-complete.
2.3 Immerman’s Pebble Game
In this section, we are going to introduce Immerman’s pebble game and its connection to the k-variable fragment of first-order logic. The pebble game will be an instrumental tool for our proofs.
For a given logic \(\mathscr{L}\) (of first-order logic sentences), we say that two graphs G and H are \(\mathscr{L}\)-equivalent, denoted by \(G \equiv _{\mathscr{L}} H\), if for all sentences \(\psi \in \mathscr{L}\) it holds that \(G \vDash \psi \Longleftrightarrow H \vDash \psi .\) Otherwise, we say that \(\mathscr{L}\) can distinguish G from H, denoted by \(G \not\equiv _{\mathscr{L}} H\).
In the following, we will consider the following subsets of first-order logic formulas.
The k-variable fragment of first-order logic \({\mathscr{L}}_{k}\) is the set of first-order logic formulas that use at most k different variables (possibly re-quantifying them). Furthermore, \({\mathscr{L}}_{k,m}\) is the subclass of \({\mathscr{L}}_{k}\) where the quantifier depth in the formulas is restricted to m.
By allowing counting quantifiers, we can extend \({\mathscr{L}}_{k}\) to the more expressive fragment \({\mathscr{C}}_{k}\).
For a graph G, we say that it has Weisfeiler–Leman dimension at most k if and only if \(G \not\equiv _{{\mathscr{C}}_{k+1}} H\) for all graphs H non-isomorphic to G.
We next describe a pebble game that is equivalent to testing \({\mathscr{L}}_{k,m}\)-equivalence (or \({\mathscr{L}}_{k}\)-equivalence for the game with an unrestricted number of rounds) and is a variant of an Ehrenfeucht-Fraïssé game [13, 17]. In Reference [26], the author has shown that \(G \not\equiv _{{\mathscr{L}}_{k,m}} H\) if and only if Player I has a winning strategy in Immerman’s m-move k-pebble game. To introduce this game, we borrow the notation from Reference [28].
Let \(m, k \in \mathbb {N}\). For graphs \(G =(V_G, E_G)\) and \(H=(V_H, E_H)\) with an equal number of vertices, we define the m-move k-pebble game of Immerman as follows: The game is played by two players called Player I and Player II1 on the graphs G and H with k pairs of pebbles. The game proceeds in rounds, each of which is associated with a position consisting of pebble placements. The position after move \(r \in [m]\) of the game is denotes by \((\vec{v}_r, \vec{w}_r) \in V_G^{\ell } \times V_H^{\ell }\) with \(0 \le \ell \le k\). The initial position is the pair \(((),())\) of empty tuples.
We now describe a round of the game. Suppose the current position of the game is \((\vec{v}_r, \vec{w}_r) = ((v_1, \dots , v_{\ell }), (w_1, \dots , w_{\ell }))\).
•
First, Player I chooses whether he wants to remove a pebble pair first (only possible if \(\ell \gt 0\)) or wants to place a new pair of pebbles directly (only possible if \(\ell \lt k\)).
–
If he wants to remove a pair of pebbles, then he chooses some \(i \in [\ell ]\) and the position of the game changes to \(((v_1, \dots , v_{i-1}, v_{i+1}, \dots , v_{\ell }), (w_1, \dots , w_{i-1}, w_{i+1}, \dots , w_{\ell }))\).
–
To place a new pebble pair, he picks a graph \(K \in \lbrace G, H \rbrace\) and a vertex \(v \in V_K\).
•
Player II then picks a vertex \(w \in V_{\hat{K}}\), where \(\hat{K} := \lbrace G,H \rbrace \setminus \lbrace K \rbrace\) is the graph not chosen by Player I. The position of the game changes toand the next round begins.
\begin{equation*} (\vec{v}_{r+1}, \vec{w}_{r+1}) := \left\lbrace \begin{array}{ll} \big ((v_1, \dots , v_{\ell }, v), (w_1, \dots , w_{\ell }, w) \big) & \mbox{if } K = G, \\ \big ((v_1, \dots , v_{\ell }, w), (w_1, \dots , w_{\ell }, v) \big) & \mbox{otherwise} , \end{array} \right. \end{equation*}
We say that Player II survives round r of the game if and only if \(G[\vec{v}_r] \cong H[\vec{w}_r]\), i.e., the map \(v_i \mapsto w_i\) (for \(i \in [\ell ]\)) is an isomorphism of the subgraphs induced by the pebbled vertices. If any difference between the induced ordered subgraphs is exposed within at most m rounds, then we say that Player I wins the m-move game. This is precisely the case when there are \(i,j \in [\ell ]\) such that \(v_i = v_j \not{\Leftrightarrow } w_i = w_j\) or \(\lbrace v_i, v_j \rbrace \in E_G \not{\Leftrightarrow } \lbrace w_i, w_j \rbrace \in E_H\) or there is an \(i \in [\ell ]\) such that the colors of \(v_i\) and \(w_i\) are different.
If there is no restriction on the number of rounds m being played, then Player I wins the game if he wins some round, while Player II survives the game if she can survive forever.
The interpretation of a configuration \(((v_1, \dots , v_\ell), (w_1, \dots , w_\ell))\) is that the ith pebble pair is placed on the vertices \(v_i\) and \(w_i\) (for \(i \in [\ell ]\)). An example of Immerman’s game is depicted in Figure 2.
Fig. 2.
3 CONNECTION BETWEEN NARROW RESOLUTION AND \(\boldsymbol {\mathscr{L}}_{\boldsymbol {k,m}}\)
Immerman’s pebble game can be directly translated as a Spoiler–Duplicator type game played on the \(\mathrm{ISO}(G,H)\) formulas. This kind of game has often been used in proof complexity arguments. The game defined here is a version of the game for the characterization of resolution width from Reference [3] except that now Spoiler cannot choose variables, but clauses and Duplicator has to satisfy some literal in the chosen clause. Very similar games have already been defined in Reference [15] and Reference [20]. The only difference is that in our game, Spoiler can only choose Type 1 clauses (instead of any clause as in Reference [15] or even variables as in Reference [20]). For some of our proofs, we need to define the witnessing games also on restricted isomorphism formulas \(\mathrm{ISO}(G,H)|_\gamma\) for some restriction \(\gamma\). In this case, we say that the Type of an axiom \(C|_\gamma\) in \(\mathrm{ISO}(G,H)|_\gamma\) (1, 2, or 3) is the same as that of the original axiom C.
For \(k \in \mathbb {N}\setminus \lbrace 1 \rbrace\) and a restriction \(\gamma\), Spoiler and Duplicator construct in rounds a partial assignment for the formula \(\mathrm{ISO}(G,H)|_\gamma\). Initially, \(\alpha _0=\varepsilon\). At the beginning of round i, Spoiler chooses a subset of \(\alpha _{i-1}\) of size at most \(k-1\) and a Type 1 clause \(C|_\gamma\) in \(\mathrm{ISO}(G,H)|_\gamma\). Then Duplicator extends the chosen subset to one positive variable x in \(C|_\gamma\) (the obtained assignment \(\alpha _i := \alpha _{i-1} \cup \lbrace x=1 \rbrace\) is of size at most k), satisfying this clause and not falsifying any clause in \(\mathrm{ISO}(G,H)|_\gamma\). If this is not possible, then Duplicator loses the game.
It holds that \(G \not\equiv _{{\mathscr{L}}_{k,m}} H\) if and only if Spoiler wins the k-witnessing game on the formula \(\mathrm{ISO}(G,H)\) in m moves.
The moves of Player I in Immerman’s game, placing a pebble on a vertex \(v_i \in V_G\) (or a vertex \(w_j \in V_H\)), correspond to Spoiler choosing a Type 1 clause of the kind \((x_{i,1} \vee \dots \vee x_{i,n})\) (respectively one of the kind \((x_{1,j} \vee \dots \vee x_{n,j})\)). Player II’s answer corresponds to the variable in these clauses satisfied by Duplicator. Since Duplicator only assigns variables with 1, only Type 2 or Type 3 clauses can be falsified. Player I wins Immerman’s game when two pebbles on different vertices in one graph are answered with two pebbles on the same vertex in the other graph, corresponding to a Type 2 clause being falsified, or when the pebbles contradict the local isomorphism condition, and this corresponds to a Type 3 clause being falsified in the witnessing game. We also notice the number of rounds in both games matches.□
Using this game, we can show an equivalence between the number of variables needed to distinguish two graphs and the width measure in narrow resolution and between the quantifier depth needed to distinguish the graphs and the depth measure in narrow resolution. Since our witnessing game is a restriction of the game in Reference [20], the proof of the result in one direction follows similar arguments as in the result for general formulas from the mentioned paper, but the bound we obtain is slightly better.
For \(k \in \mathbb {N}\), it holds that \(G \not\equiv _{{\mathscr{L}}_{k,m}} H\) if and only if there is a narrow width resolution refutation \(\pi\) of \(\mathrm{ISO}(G,H)\) with \(\mathrm{N\text{-}Width}(\pi) \le k-1\) and \(\mathrm{N\text{-}Depth}(\pi) \le m\) simultaneously.
For the direction from left to right, suppose \(G \not\equiv _{{\mathscr{L}}_{k,m}} H\). By Observation 3.2, there is a winning strategy for Spoiler in the k-witnessing game on \(\mathrm{ISO}(G,H)\) in m moves. This strategy has to be able to let Spoiler decide for each reachable partial assignment \(\alpha\) in the game what variables can be deleted from the assignment and what Type 1 clause C to query next. Such a strategy can be represented as a graph whose vertices store the information \((\alpha , C)\) with \(|\alpha | \le k-1\). From such a vertex and for every literal \(\ell \in C\), there is a directed edge pointing to the vertex \((\alpha ^{\prime }_\ell , C_\ell)\). Here, \(\alpha ^{\prime }_\ell\) is the assignment obtained from \(\alpha\) by setting \(\ell =1\) and maybe deleting some values (according to the strategy of Spoiler after knowing the answer of Duplicator for C). Furthermore, \(C_\ell\) is the Type 1 clause queried next or a clause falsified by \(\alpha _\ell ^\prime\). In this last case, \((\alpha _\ell ^\prime , C_\ell)\) is a winning position for Spoiler and a sink in the strategy graph. The only source of the graph is the initial vertex \((\alpha _0, C_0)\), where \(\alpha _0 = \varepsilon\) and \(C_0\) is the first Type 1 clause queried by Spoiler. We refer to Figure 3. Observe that since we have supposed that Spoiler has a winning strategy, this graph is acyclic. It is not necessarily a tree.
Fig. 3.
We can construct a resolution refutation DAG of \(\mathrm{ISO}(G,H)\) by following the strategy backwards, i.e., by inverting the strategy graph. For this, we associate with each vertex \((\alpha , C)\) the clause \(K_{\alpha }\), defined as the set of literals falsified by \(\alpha\). We refer to Figure 4 for an example continuing the example given in Figure 3.
Fig. 4.
With an inductive argument, starting at the sinks, we show that \(K_{\alpha }\) can be resolved by narrow resolution from the clauses associated with the successor vertices of \((\alpha , C)\). For the sink vertices \((\alpha , C)\), by the way the strategy graph and the witness game are defined, C is an axiom of width 2 falsified by \(\alpha\). Since C is an axiom, it does not count for the narrow width. Using weakening, we can identify \(K_{\alpha }\) with this vertex.
For an interior vertex \((\alpha , C)\) with \(C=(\ell _1 \vee \dots \vee \ell _n)\) and with successor vertices \((\beta _1, C_1), \dots , (\beta _n, C_n)\), we can suppose by induction that there are clauses \(K_{\beta _1}, \dots K_{\beta _n}\) associated with the successor vertices. Each assignment \(\beta _i\) has the form \(\beta _i = \alpha _i \cup \lbrace \ell _i=1 \rbrace\) with \(\alpha _i \subseteq \alpha\) and \(|\beta _i| \le k-1\). Because of this, C and each \(K_{\beta _i}\) have exactly the pair of complementary literals \((\ell _i, \overline{\ell _i})\) and can be resolved. Using a narrow resolution step, we can resolve all these clauses with C in one step, obtaining a clause \(K_{\alpha ^{\prime }}\) with \(\alpha ^{\prime } \subseteq \alpha\), and with weakening, we obtain \(K_{\alpha }\).
Since the clause mapped to the source vertex has to be falsified by the empty assignment, this is the empty clause, and the process defines a correct narrow resolution of \(\mathrm{ISO}(G,H)\). Notice that all the non-axiom clauses in the refutation have at most \(k-1\) literals.
The depth of the strategy graph for Spoiler in the k-witnessing game is the maximum number of rounds m needed for Spoiler to defeat Duplicator in Immerman’s \({\mathscr{L}}_{k}\)-game. One can notice that the depth of the strategy graph also coincides with the depth of the narrow resolution proof extracted from it (notice from the observation after the proof of Lemma 2.8 that weakening steps do not increase the depth).
By the correspondence between the game positions \((\beta _i, C_i)\) and the clauses \(K_{\beta _i}\) of the proof \(\pi\) constructed above, this shows that we have \(\mathrm{N\text{-}Width}(\pi) \le k-1\) and \(\mathrm{N\text{-}Depth}(\pi) \le m\) simultaneously.
For the other direction, consider a narrow resolution refutation \(\pi\) for \(\mathrm{ISO}(G,H)\) of width \(k-1\) and depth m. We describe a strategy for Spoiler to win the k-witnessing game in m moves. Spoiler queries Type 1 clauses, and with the variables satisfied by Duplicator, he keeps a set S of at most k variables \(x_{i,j}\) assigned with value 1 by Duplicator. For a clause \(C \in \pi\) and such a set S, we say that S contradicts C if the following conditions happen:
(1)
For every negated variable \(\overline{x_{i,j}}\) in C: \(x_{i,j} \in S\); and
(2)
for every positive variable \(x_{i,j}\) in C:
(2a)
\(x_{i,j}\not\in S\), and
(2b)
\([ (\exists k \in [n]\) such that \((x_{i,k} \in S\) or \(x_{k,j} \in S))\)
or \((\exists x_{k,\ell }\) with \(x_{k,\ell } \in S\) and \((\overline{x_{i,j}} \vee \overline{x_{k,\ell }})\in \mathrm{ISO}(G,H)) ]\).
Intuitively, this means that the set of positive variables in S either falsifies C or an axiom in \(\mathrm{ISO}(G,H)\). Starting at the empty clause and with \(S = \emptyset\), the set S determines the predecessor clause in the refutation \(\pi\) where Spoiler moves to. At each step, Spoiler makes a query, updates S while also deleting from S all the variables that are not needed for contradicting the new clause, and always moves to the predecessor clause contradicted by the current S (if Duplicator has not immediately lost the game by her answer). Let C be Spoiler’s clause at a certain stage and S the corresponding set of variables. We distinguish between different cases, depending on the origin of C in the proof:
Case 1a: Let us first treat the case where C is the (normal) resolvent of two clauses \((A \vee x_{i,j})\) and \((B \vee \overline{x_{i,j}})\) and where \((A \vee x_{i,j})\) is a Type 1 axiom. Without loss of generality, we can suppose \((A \vee x_{i,j}) = (x_{i,1} \vee \dots \vee x_{i,j} \vee \dots \vee x_{i,n})\); the other kind of Type 1 axiom can be treated analogously. The strategy for Spoiler is to query this Type 1 parent clause.
If Duplicator assigns \(x_{i,j} = 1\), then the parent clause \((B \vee \overline{x_{i,j}})\) is contradicted by \(S^\prime := S \cup \lbrace x_{i,j} \rbrace\). If, however, Duplicator assigns \(x_{i,\ell } = 1\) for some \(\ell \in [n] \setminus \lbrace j \rbrace\), then a Type 2 or Type 3 clause will immediately be violated, and Duplicator loses. This is due to the fact that \(x_{i,\ell } \in C\), and C was contradicted by S.
Case 1b: In the case where both parent clauses \((A \vee x_{i,j})\) and \((B \vee \overline{x_{i,j}})\) are not of Type 1, Spoiler queries any of the two Type 1 clauses in \(\mathrm{ISO}(G,H)\) containing \(x_{i,j}\). To simplify the exposition, let us, once again, suppose without loss of generality that this Type 1 clause is of the form \((x_{i,1} \vee \dots \vee x_{i,j} \vee \dots \vee x_{i,n})\); the other case is analogous.
If Duplicator assigns value 1 to variable \(x_{i,j}\), then Spoiler moves to the contradicted parent clause \((B \vee \overline{x_{i,j}})\) and sets \(S^\prime := S \cup \lbrace x_{i,j} \rbrace\), as before. If some other variable is given value 1 by Duplicator, say, \(x_{i,\ell } = 1\) for some \(\ell \in [n] \setminus \lbrace j \rbrace\), then we must, additionally, distinguish between two cases. If \(x_{i,\ell } \not\in (A \vee x_{i,j})\), then \((A \vee x_{i,j})\) is contradicted by \(S^\prime := S \cup \lbrace x_{i,\ell } \rbrace\). If, however, \(x_{i,\ell } \in (A \vee x_{i,j})\), then \(x_{i,\ell }\) is also present in the resolvent C. But since this clause was contradicted by S, this means that \(S^\prime := S \cup \lbrace x_{i,\ell } \rbrace\) contradicts a Type 2 or Type 3 clause.
Case 2a: If C is the result of a narrow resolution step involving a Type 1 axiom D, then Spoiler queries the clause D. Duplicator’s answer must satisfy some variable \(x_{i,j} \in D\). If \(x_{i,j}\) is resolved at this step and it is not present in C, then the set \(S^\prime = S \cup \lbrace x_{i,j} \rbrace\) contradicts some predecessor clause \(C^\prime \ne D\). Spoiler thus moves to this predecessor \(C^\prime\), and he then deletes from \(S^\prime\) all the variables that are not necessary in \(S^\prime\) for contradicting the new clause. This means keeping one variable for each negated literal in \(C^\prime\) and at most one variable for each positive literal in \(C^\prime\). Because the clauses in \(\pi\) have narrow width at most \(k-1\), Spoiler needs to keep at most k variables in \(S^\prime\) at any moment.
If, however, \(x_{i,j}\) is not resolved at this step and thus still present in the resolvent C, then \(S^\prime = S \cup \lbrace x_{i,j} \rbrace\) contradicts a Type 2 or a Type 3 clause. As before, Spoiler needs to keep at most k variables in \(S^\prime\) at any moment.
Case 2b: Let C be the result of a narrow resolution step without a Type 1 axiom but involving a Type 2 or Type 3 axiom D. The situation is analogous to Case 2a, where Spoiler moves to a parent clause \(C^\prime \ne D\).
Let us first consider the case with a Type 3 axiom \(D = (\overline{x_{i,j}} \vee \overline{x_{k,\ell }})\) narrow resolved with two clauses \((A \vee x_{i,j})\) and \((B \vee {x_{k,\ell }})\). In this case, Spoiler can query the axiom \((x_{i,1} \vee \dots \vee x_{i,n})\). Suppose Duplicator’s answer is \(x_{i,j}\). If \(x_{k,\ell } \in S\), then D is falsified by \(S^\prime = S \cup \lbrace x_{i,j} \rbrace\); otherwise \((B \vee x_{k,\ell })\) is contradicted by this very \(S^\prime\). When Duplicator’s reply is \(x_{i,m}\) for some \(m \in [n] \setminus \lbrace j \rbrace\), if \(x_{i,j} \in S\), then a Type 2 axiom is falsified by \(S^\prime = S \cup \lbrace x_{i,m} \rbrace\); otherwise \((A \vee x_{i,j})\) is contradicted by \(S^\prime\).
For the case where a Type 2 axiom, say, \(D = (\overline{x_{i,j}} \vee \overline{x_{i,\ell }})\), is narrow resolved with the clauses \((A \vee x_{i,j})\) and \((B \vee x_{i,\ell })\), again, Spoiler queries the Type 1 clause \((x_{i,1} \vee \dots \vee x_{i,j} \vee \dots \vee x_{i,\ell } \vee \dots \vee x_{i,n})\). If Duplicator replies \(x_{i,j}\), then \((B \vee x_{i,\ell })\) is contradicted by the updated set \(S^\prime\). If she answers \(x_{i,\ell }\), then \((A \vee x_{i,j})\) is contradicted by the respectively updated set \(S^\prime\). Finally, we consider the case where Duplicator chooses to answer \(x_{i,m}\) for a \(m \in [n] \setminus \lbrace j, \ell \rbrace\). We can assume that \(x_{i,j}, x_{i,\ell } \not\in S\), as otherwise a Type 2 axiom will be falsified by \(S^\prime = S \cup \lbrace x_{i,m} \rbrace\). But then, both parent clauses \((A \vee x_{i,j})\) and \((B \vee x_{i,\ell })\) are contradicted by the new \(S^\prime\).
Case 3: If C comes from a weakening step, then Spoiler just needs to forget some of the variables in S.
Eventually, some axiom is reached. This axiom is contradicted by the current S. This axiom cannot be of Type 1 since, by the definition of the strategy, each time such an axiom is a parent clause of the actual contradicted clause, it is queried, and therefore, it must be satisfied by S. If the reached axiom is of Type 2 or Type 3, then S falsifies it (these axioms have only negated literals), and Spoiler wins.
In the described construction of a winning strategy, Spoiler always moves to the contradicted predecessor of the clause he is currently standing on. Such a move can increase the depth at most by one. Thus he needs at most m moves to win the Immerman game, where m is the depth of the narrow refutation.□
Not surprisingly, the result above holds also for colored graphs, that is, the number of pebbles and rounds in Immerman’s game on colored graphs corresponds exactly to the narrow width and depth required by resolution to refute the isomorphism formula under the restriction encoding the coloring. We need, in fact, a version of the result for general restrictions, not only for colorings, and therefore we have to make use of the witnessing game, which is also well defined for restrictions. The proof follows the same steps as that for the result above. We state the part of the result that we will need for our results.
For \(k \in \mathbb {N}\), and for every restriction \(\gamma\), Spoiler has a winning strategy for the k-witnessing game on \(\mathrm{ISO}(G,H)|_\gamma\) if and only if \({\mathrm{N\text{-}Width}}_{}{(\mathrm{ISO}(G,H)|_\gamma \mathrel {\mathop \vdash }\!\square)} \le k-1\).
The equivalence between the number of variables for graph differentiation and narrow width allows us to give upper and lower bounds for the size of resolution proofs for isomorphism formulas.
Let \(k \in \mathbb {N}\), and let G and H be two non-isomorphic graphs with n vertices each. If \(G \not\equiv _{{\mathscr{L}}_{k}} H\), then there is a (normal) resolution refutation of \(\mathrm{ISO}(G,H)\) of size \(n^{\mathrm{O}(k)}\).
By the above result, if \(G \not\equiv _{{\mathscr{L}}_{k}} H\), then the narrow resolution width of \(\mathrm{ISO}(G,H)\) is at most \(k-1\). Since there are \(n^2\) variables in this formula, there are at most \(\sum _{i=0}^{k-1} \binom{n^2}{i} 2^i\) clauses that can appear in a \((k-1)\)-narrow resolution refutation of the formula. But a narrow resolution refutation is just like a normal one in which the distinction by cases is made in just one step. This can be simulated by at most n steps (with at most \(n-1\) intermediate clauses that might be wider than k) in normal resolution. Bounding the partial sum of binomial coefficients by the largest one, the total number of different clauses in the refutation is thus bounded by \(n^{\mathrm{O}(k)}\).□
Observe that Theorem 3.5 suggests a way to automatically generate short proofs for (non)isomorphism formulas, following the same ideas as those in the algorithm proposed in References [7, 20, 21] for general formulas. The algorithm would generate in stages all clauses that can be derived by narrow resolution of width \(1,2,3,\dots\) until the empty clause is derived. By the above result, the running time of this algorithm is \(n^{\mathrm{O}(k)}\). This is a polynomial for constant k.
Even more interestingly, Theorem 3.5 also has a consequence for the average-case resolution complexity. For this, we use the upper bounds on the quantifier depth of random graphs from [30].
Let \(0 \lt p \le \frac{1}{2}\) be a constant. If \(G, H \sim \mathcal {G}(n,p)\) are independent and non-isomorphic random n-vertex graphs, or if \(G \sim \mathcal {G}(n,p)\) is random and H is an arbitrary non-isomorphic graph, then, with high probability, \(\mathrm{ISO}(G,H)\) has a (normal) resolution refutation of size \(n^{\mathrm{O}(\log n)}\).
A first-order logic sentence \(\psi\) is said to define a graph G if \(G \models \psi\), while \(H \not\models \psi\) for any graph \(H \not\cong G\). Let \(\operatorname{qd}(G)\) be the smallest quantifier depth of a sentence defining the graph G. Let \(G \sim \mathcal {G}(n,p)\) be a random n-vertex graph, and H either an independent non-isomorphic random graph with n vertices and same edge probability, or any arbitrary non-isomorphic n-vertex graph. It was shown in Reference [30, Theorem 2] that, with high probability,Since every sentence of quantifier depth m can be rewritten with at most m variables, we have that the graphs G and H are not \({\mathscr{L}}_{\log _{1/p} n + \mathrm{O}(\ln \ln n)}\)-equivalent. By Theorem 3.5, we know that there is a (normal) resolution refutation of \(\mathrm{ISO}(G,H)\) with size \(n^{\mathrm{O}(\log n)}\).□
\begin{equation*} \operatorname{qd}(G) = \log _{1/p}n + \mathrm{O}(\ln \ln n). \end{equation*}
Lower bounds for narrow width also imply lower bounds on the size of a resolution refutation for \(\mathrm{ISO}(G,H)\), in the same way that width lower bounds imply size lower bounds in normal resolution, as shown by Ben-Sasson and Wigderson [7]. For this, we follow the same steps as in the mentioned paper, adapted to narrow width. The general fact that narrow width provides lower bounds for resolution size has also been proved in Reference [20]. By concentrating on the isomorphism formulas, we obtain tighter results. The next lemma is the basis for our lower bounds. It is a version in our context of Reference [7, Lemma 3.2] or Reference [20, Lemma 6].
Let \(\gamma\) be a restriction and let \(\ell\) be any literal in \({\mathrm{ISO}(G,H)|_\gamma }\). If Spoiler has a winning strategy for the k-witnessing game on \({\mathrm{ISO}(G,H)}|_{\gamma \lbrace \ell =1\rbrace }\) as well as for the \((k-1)\)-witnessing game on \({\mathrm{ISO}(G,H)}|_{\gamma \lbrace \ell =0\rbrace }\), then he wins the k-witnessing game on \({\mathrm{ISO}(G,H)|_\gamma }\).
We distinguish two cases depending on whether \(\ell\) is a positive or a negated variable:
Case 1: \(\ell =x_{i,j}\). The formula \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=1\rbrace }\) is like \({\mathrm{ISO}(G,H)|_\gamma }\) without the two Type 1 clauses containing literal \(x_{i,j}\) and without all occurrences of the literal \(\overline{x_{i,j}}\). If Spoiler selects in the game on \({\mathrm{ISO}(G,H)|_\gamma }\) the same sequence of Type 1 clauses as in the game on \({\mathrm{ISO}(G,H)}|_{\gamma \lbrace x_{i,j}=1\rbrace }\), then Duplicator either loses the game or sets a literal \(x_{a,b}\) to 1, which appears in a clause \(C=(\overline{x_{a,b}} \vee \overline{x_{i,j}}) \in \mathrm{ISO}(G,H)|_\gamma\). When this happens, Spoiler restricts the assignment to \(\gamma \lbrace x_{a,b}=1\rbrace\), forgetting all other assigned variables, and then simulates the strategy for \({\mathrm{ISO}(G,H)}|_{\gamma \lbrace x_{i,j}=0\rbrace }\) on \({\mathrm{ISO}(G,H)|_\gamma }\), thus keeping at most \(1+(k-1)=k\) variables in memory. If Duplicator does not assign \(x_{i,j}=1\), then she loses the game eventually by the assumption. If she does, then the clause C is falsified, and she also loses. Spoiler needs to keep an assignment of size at most k at any moment.
Case 2: \(\ell =\overline{x_{i,j}}\). In this case, Spoiler simulates the strategy for \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=0\rbrace }\) on the formula \(\mathrm{ISO}(G,H)|_\gamma\), either winning the game or forcing Duplicator to assign \(x_{i,j}=1\) (by a Type 1 clause that contains \(x_{i,j}\) and which was falsified in the \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j} = 0\rbrace }\)-game). Restricting then the assignment to this literal, Spoiler now plays the strategy for \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=1\rbrace }\) and Duplicator loses.□
From this result, lower bounds as in Reference [7] follow directly. The advantage here is that the width of the axioms of \(\mathrm{ISO}(G,H)\) is not subtracted from the exponent of the lower bound results, as it is done in Reference [7, Corollary 3.4].
Let \(k \in \mathbb {N}\), and G and H be two non-isomorphic graphs with n vertices each. If \(G \equiv _{{\mathscr{L}}_{k}} H\), then the size of a treelike resolution refutation of \(\mathrm{ISO}(G,H)\) is at least \(2^{k}\).
We show for any restriction \(\gamma\), that if there is a treelike resolution refutation \(\pi\) of the formula \(\mathrm{ISO}(G,H)|_\gamma\) of size at most \(2^b\) for \(b \in \mathbb {N}\), then the narrow resolution width of \(\mathrm{ISO}(G,H)|_\gamma\) is at most b. This is done by induction on b and m, the number of variables in \(\mathrm{ISO}(G,H)|_\gamma\). The result follows by considering \(\gamma\) to be the empty assignment.
For the base case \(b=0\), we have that \(\mathrm{ISO}(G,H)|_\gamma\) contains the empty clause, and there is nothing to prove. For the other base case, i.e., \(m=1\), the formula \(\mathrm{ISO}(G,H)|_\gamma\) is unsatisfiable and contains only one variable x. Thus, the formula is \(x \wedge \overline{x}\). Clearly, this formula can be refuted in narrow width 1.
For the induction step, let \(x_{i,j}\) be the last variable resolved in \(\pi\). The two literals \(x_{i,j}\) and \(\overline{x_{i,j}}\) have two treelike derivations \(\pi _1\) and \(\pi _2\) and at least one of them, without loss of generality \(\pi _1\), has size at most \(2^{b-1}\). There is then a treelike refutation of \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=0\rbrace }\) of size \(2^{b-1}\), and by induction hypothesis the narrow width of \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=0\rbrace }\) is at most \(b-1\). The formula \(\mathrm{ISO}(G,H)|_{\gamma \lbrace x_{i,j}=1\rbrace }\) has at most \(m-1\) variables and a treelike refutation of size bounded by \(2^b\). By the induction on m, the narrow resolution width of this formula is at most b. Applying the equivalence of narrow width and the witnessing game from Observation 3.4 and applying Lemma 3.8, we obtain the result.□
Let \(k \in \mathbb {N}\setminus \lbrace 1 \rbrace\), and let \(G_{2k} := K_k \uplus \overline{K_k}\) and \(H_{2k} := K_{k+1} \uplus \overline{K_{k-1}}\). Then, \(n := |V(G_{2k})| = |V(H_{2k})| = 2k\), and \(G_{2k} \not\cong H_{2k}\). Furthermore, Reference [38, Example 2.6] shows that \(G_{2k} \equiv _{{\mathscr{L}}_{k-1}} H_{2k}\). Thus, Theorem 3.9 implies that the size of any treelike resolution refutation of \(\mathrm{ISO}(G_{2k},H_{2k})\) is at least \(2^{\frac{n}{2}-1}\).
This lower bound is essentially the best possible achievable with this approach since it was shown in Reference [38, Theorem 3.1] that any two graphs with n vertices can be distinguished by a first-order logic sentence that uses at most \(\frac{n+3}{2}\) variables.
Lower bounds on narrow width also imply, as noted in Reference [20], lower bounds on normal resolution size. We include a version of Reference [7, Theorem 3.5] adapted to the isomorphism formulas since it makes use of Lemma 3.8. Because the number of variables in the isomorphism formulas is quadratic in the number of graph vertices, this result only provides trivial lower bounds when applied to general graphs. A way to decrease the number of variables in the formula is by considering colored graphs. Since a coloring can be expressed as a restriction \(\rho\) applied to \(\mathrm{Vars}({\mathrm{ISO}(G,H)})\), and using the fact that for every restriction \(\rho\), the size of a resolution refutation of \(\mathrm{ISO}(G,H)\) is at least the size of the refutation of the formula under the restriction, \(\mathrm{ISO}(G,H)|_\rho\), we obtain Theorem 3.12 below.
Let \((G, \lambda)\) and \((H, \mu)\) be two colored graphs. For a vertex \(v \in V_G\), we set
i.e., the set of vertices in \(V_H\) that have the same color as v.
If \((G, \lambda)\) and \((H, \mu)\) are two colored graphs in n vertices each, then \(m := \sum _{v\in V_G} |\text{ color-class}_H(v)|\) is between n and \(n^2\).
Let \(G=(V_G,E_G)\) and \(H=(V_H,E_H)\) be two non-isomorphic graphs with n vertices each, for which there is a \(k \in \mathbb {N}\) and two colorings \(\lambda , \mu\) such that \((G, \lambda) \equiv _{{\mathscr{L}}_{k}} (H, \mu)\). Then, the size of every resolution refutation of \(\mathrm{ISO}(G,H)\) is at least \({\exp } (\Omega (k^2/m))\), where \(m := \sum _{v \in V_G} |\text{ color-class}_H(v)|\) is the sum of the sizes of the color classes.
Let \(\rho := \lbrace x_{i,j} = 0\, |\, i,j \in [n] \text{ with } \lambda (i) \ne \mu (j) \rbrace\), and consider the unsatisfiable formula \(\mathrm{ISO}(G,H)|_\rho\). The set of variables of this formula is \(\lbrace x_{i,j} \,\vert \, i,j \in [n] \text{ with } \lambda (i) = \mu (j) \rbrace\) and contains exactly \(m = \sum _{v \in V_G} |\text{ color-class}_H(v)|\) variables. Since \((G, \lambda) \equiv _{{\mathscr{L}}_{k}} (H, \mu)\), by Observation 3.4, \({\mathrm{N\text{-}Width}}_{}{(\mathrm{ISO}(G,H)|_\rho \mathrel {\mathop \vdash }\!\square)} \ge k\). We follow the same steps as that of Reference [7, Theorem 3.5], with the modifications needed to deal with restrictions as done in Theorem 3.9.
For simplicity, let us denote \(\mathrm{ISO}(G,H)|_\rho\) by F and let \(\pi\) be a (normal) resolution refutation of minimal size s of F. We define d and a to beA clause in \(\pi\) is called fat if it contains more than d literals. Let \(\pi ^*\) be the set of fat clauses in \(\pi\). We will prove by induction on m that
\begin{equation*} d := \lceil \sqrt {2m\ln s} \rceil , \quad \text{and} \quad a := \left(1 - \frac{d}{2m} \right)^{-1}. \end{equation*}
(1)
We proceed by showing Inequality (1) inductively. The base case \(m=1\) holds trivially. For the induction case, observe that F contains at most 2m literals and therefore one literal \(\ell\) appears in at least \({\frac{d}{2m}}|\pi ^*|\) fat clauses. We consider the two refutations of the formulas \(F|_{\ell =1}\) and \(F|_{\ell =0}\) obtained from \(\pi\) by setting \(\ell\) to 1 and to 0, respectively. Setting \(\ell =1\) removes all the clauses that include literal \(\ell\) and leaves a refutation of \(F|_{\ell =1}\) with at most \((1-\frac{d}{2m})|\pi ^*|=a^{-1}|\pi ^*|\) fat clauses and one variable less. By the induction hypothesis, we have
Setting \(\ell =0\) produces a refutation of the formula \(F|_{\ell =0}\) with less than m variables, and again by induction on m it holds
By applying Lemma 3.8 to Inequalities (2) and (3) we indeed obtain Inequality (1). This finishes the induction.
(2)
(3)
The result follows from this inequality because \({\log _a} (|\pi ^*|)\) is bounded by \(\sqrt {2n \ln s}\). This can be seen in the following way: Since \(s \lt 2^{m+1} \lt \mathrm{e}^{2m}\), we have that \(d \lt 2m\), and thus \(a \gt 1\). Also,where the last inequality follows from the fact that \(\ln (1+x) \le x\) for \(x \gt -1\). Therefore,
\begin{equation*} \ln a = - \ln \left(1 - \frac{d}{2m} \right) \ge \frac{d}{2m}, \end{equation*}
\begin{equation*} {\log _a} \big (| \pi ^* | \big) \le \log _a(s) = \frac{\ln s}{\ln a} \le \frac{\ln s}{\frac{d}{2m}} \le \frac{\ln s}{\sqrt {\frac{\ln s}{2m}}} = \sqrt {2m \ln s}. \end{equation*}
Observe that since we are dealing with narrow resolution, we do not need the width of the axioms in \(\mathrm{ISO}(G,H)|_\rho\) as an additional term, as in the result from Reference [7]. It follows that \({\mathrm{Size}}_{}{(\mathrm{ISO}(G,H)|_\rho \mathrel {\mathop \vdash }\!\square)}={\exp }(\Omega (k^2/m))\). The last fact needed is that for every restriction \(\rho\) it holds that
□
This result can then be automatically applied to graphs in which the maximum size of a color class is small.
Let G and H be two non-isomorphic graphs with n vertices each, and let \(k \in \mathbb {N}\) and \(\lambda , \mu\) be colorings with constant size color classes such that \((G, \lambda) \equiv _{{\mathscr{L}}_{k}} (H, \mu)\). Then, any resolution refutation of \(\mathrm{ISO}(G,H)\) has a size of at least \({\exp }(\Omega (k^2/n))\).
Such constant size color classes are the case for the colored CFI graphs [9, 43] and the variant of the multipede graphs from Reference [12]. In both examples, the maximum size of a color class is 4, while the number of variables needed to distinguish the graphs is linear in n.
A subtle point in the application of the above result to the mentioned graph classes is that the non-isomorphism of graphs G and H does not automatically follow from the non-isomorphism of the colored graphs \((G,\lambda)\) and \((H,\mu)\). If the non-colored versions of G and H were isomorphic, then there would not be a refutation of \(\mathrm{ISO}(G,H)\). A standard way to avoid this complication is to replace the colors by attaching gadgets to the vertices in the graphs (see, e.g., Reference [32]). Each of the possible n colors can be encoded with a gadget of at most \(\mathrm{O}(\log n)\) vertices using rooted trees encoding the binary representation of the respective color. This has the disadvantage, however, that the number of vertices in the resulting graphs increases by a \(\log n\) factor and the resolution size lower bound in the result would become \({\exp } (\Omega (k^2/n \log n))\), which is worse than that in Corollary 3.13.
Another way to achieve this for classes of CFI graphs with certain additional conditions is suggested in Reference [18, Lemma 4.3], where a regularized and discolored version of the CFI graphs is presented, in which the CFI graphs retain their properties even without colors.
A simpler way to satisfy the condition that the non-isomorphism of the colored CFI graphs implies the non-isomorphism of the non-colored CFI graphs is to observe that the colors in such graphs are basically only needed to simplify the arguments. In a CFI transformation of a graph G, there are two kinds of vertices, one kind corresponding to the edges and the other kind corresponding to the vertices in the original graph G. The only condition needed is that in an isomorphism \(\varphi\) between CFI graphs, two vertices encoding an original edge e are mapped to vertices encoding an edge \(\varphi (e)\) (not necessarily the same as e) and that the vertices encoding an original vertex v are mapped to vertices encoding \(\varphi (v)\). This condition can be achieved with two simple constant-size gadgets, one kind joining together both vertices encoding an edge and the other kind joining together all the vertices encoding an original vertex. With this observation in mind, every pair of colored CFI graphs can be transformed into a pair of uncolored graphs that are only a constant factor larger. A result like, for example, Reference [43, Lemma 4.6] implies that if the colored CFI graphs are non-isomorphic, then this is also true for the uncolored graphs.
Thus, for both examples above, the corollary gives a resolution size lower bound of \({\exp }(\Omega (n))\). One can also imagine this result being useful for proving resolution size lower bounds in cases in which not all color classes of the graphs have constant size, but the sum of the class sizes is still smaller than the number of variables needed to distinguish the graphs.
4 An Exponential Lower Bound for the Size of SRC-1 Proofs for Graph (Non)Isomorphism
In this section, we show that there is a family of non-isomorphic graph pairs \((G_n, H_n)\) that has only exponentially long proofs of \(\mathrm{ISO}(G_n,H_n)\) in the SRC-1 system. Exponential size lower bounds in SRC-1 are known [46] but not for graph isomorphism formulas. Our result is proven by observing that the global symmetry rule cannot be applied to formulas corresponding to graphs having only trivial automorphisms and restricting ourselves to such graphs.
A colored graph \((G, \lambda)\) is called asymmetric if \(\mathrm{Aut}(G) = \lbrace \mathrm{id} \rbrace\).
To characterize the possible symmetries in an isomorphism formula, we need the notions of graph anti-automorphism and anti-isomorphism.
Let \(G=(V_G, E_G)\) and \(H=(V_H, E_H)\) be two graphs. An anti-isomorphism \(\sigma\) from G to H is a bijection between the vertices of G and H exchanging edges and non-edges, i.e., for all \(u,v \in V_G\) with \(u \ne v\):An anti-automorphism of a graph G is an anti-isomorphism from G to G. We denote by \(\mathrm{A\text{-}Iso}(G,H)\) the set of anti-isomorphisms between G and H and by \(\mathrm{A\text{-}Aut}(G)\) the set of anti-automorphisms of G.
\begin{equation*} \lbrace u,v \rbrace \in E_G \Longleftrightarrow \big \lbrace \sigma (u),\sigma (v) \big \rbrace \not\in E_H. \end{equation*}
We will also need the following simple observation.
Asymmetric graphs do not have any anti-automorphisms.
Let \(G=(V_G, E_G)\) be an asymmetric graph, and suppose \(\sigma\) is an anti-automorphism in G. Then \(\sigma ^2\) is an automorphism since it maps edges to edges and non-edges to non-edges, and because G is asymmetric, \(\sigma ^2=\mathrm{id}\). Choose any \(u \in V_G\), and let \(v := \sigma (u)\). Since \(\sigma\) is an anti-automorphism we have \(\lbrace u,v \rbrace = \lbrace u,\sigma (u) \rbrace \in E_G\) if and only if \(\lbrace \sigma (u), \sigma (\sigma (u)) \rbrace \not\in E_G\), but this is a contradiction since \(\lbrace \sigma (u), \sigma (\sigma (u)) \rbrace = \lbrace v,u \rbrace\).□
Urquhart observed in Reference [46, Proof of Theorem 3.4] (see also Reference [42, Lemma 10]) that if a formula is asymmetric (meaning it has no non-trivial renamings), then the size of a resolution refutation and an SRC-1 refutation of the formula is equal. The next lemma shows that if two graphs are asymmetric, then the corresponding isomorphism formula is also asymmetric.
Let G and H be two graphs with \(|V_G| = |V_H| =: n \ge 3\), and let \(F := \mathrm{ISO}(G,H)\). Further, let \(f:\mathrm{Lits}({F}) \rightarrow \mathrm{Lits}({F})\) be a renaming of the literals in F. Then, \(f(F) \subseteq F\) if and only if one of the following two cases hold:
(1)
There are two permutations \(\sigma , \gamma \in S_n\) such that for every \((i,j) \in [n] \times [n]\), \(f(x_{i,j}) = x_{\sigma (i),\gamma (j)}\) and \((\sigma , \gamma) \in \mathrm{Aut}(G) \times \mathrm{Aut}(H)\) or \((\sigma , \gamma) \in \mathrm{A\text{-}Aut}(G) \times \mathrm{A\text{-}Aut}(H)\); or
(2)
there are two permutations \(\sigma , \gamma \in S_n\) such that for every \((i, j) \in [n] \times [n]\), \(f(x_{i,j})=x_{\gamma (j),\sigma (i)}\) and \((\sigma ,\gamma ^{-1})\in \mathrm{Iso}(G,H)\times \mathrm{Iso}(G,H)\) or \((\sigma ,\gamma ^{-1})\in \mathrm{A\text{-}Iso}(G,H)\times \mathrm{A\text{-}Iso}(G,H)\).
From left to right, let f be a renaming of the literals in \(F = \mathrm{ISO}(G,H)\) with \(f(F) \subseteq F\). Since the Type 1 clauses have a width of at least 3, and the clauses of width two have only negative literals, the sign of the literals remains under f. We can consider the Type 1 clauses of \(\mathrm{ISO}(G,H)\) represented in the form of an \((n \times n)\)-matrix, in which in position \((i, j)\), we have variable \(x_{i,j}\). The Type 1 clauses are the rows and the columns of this matrix, and f can be seen as a transformation mapping the set of rows and columns to itself. The image of two literals in a row i, for example, \(f(x_{i,1})\) and \(f(x_{i,2})\), determines whether this row is mapped to a row or to a column. In the first case, there is a permutation \(\sigma\) so that row i is mapped to row \(\sigma (i)\). Since, in this case, columns have to be mapped to columns, there has to be another permutation \(\gamma\) such that for each pair \((i,j)\), we have that \(f(x_{i,j}) = x_{\sigma (i),\gamma (j)}\). In the case in which rows are mapped to columns, we would have \(f(x_{i,j}) = x_{\gamma (j),\sigma (i)}\). We analyze the first situation; the other case is analogous.
If \(\sigma\) and \(\gamma\) are both anti-automorphisms, then there is nothing to prove. Thus, suppose \(\gamma\) is not an anti-automorphism in H; then there are two vertices \(u,v \in V_H\) such that \(\lbrace u,v \rbrace \in E_H \Leftrightarrow \lbrace \gamma (u), \gamma (v) \rbrace \in E_H\). If \(\sigma \not\in \mathrm{Aut}(G)\), then there are two vertices \(a,b \in V_G\) such that \(\lbrace a, b \rbrace \in E_G \Leftrightarrow \lbrace \sigma (a), \sigma (b) \rbrace \not\in E_G\), but then we would havecontradicting the fact that \(f(F) \subseteq F\). Therefore, if \(\gamma\) is not an anti-automorphism, then \(\sigma\) is an automorphism. By a symmetric argument, if \(\sigma\) is an automorphism (and therefore not an anti-automorphism), then \(\gamma\) also has to be an automorphism. This shows that \(\sigma\) and \(\gamma\) are both automorphisms or both anti-automorphisms.
\begin{equation*} (\overline{x_{a,u}} \vee \overline{x_{b,v}}) \in F \Leftrightarrow (\overline{x_{\sigma (a),u}} \vee \overline{x_{\sigma (b),v}}) \not\in F \Leftrightarrow (\overline{x_{\sigma (a),\gamma (u)}} \vee \overline{x_{\sigma (b),\gamma (v)}}) \not\in F, \end{equation*}
For the direction from right to left, we prove the second case; the first one is similar. If f is defined as \(f(x_{i,j}) = x_{\gamma (j),\sigma (i)}\) with \(\sigma , \gamma ^{-1} \in \mathrm{Iso}(G,H)\), then Type 1 row clauses are transformed into column clauses and vice versa.
Every Type 2 clause \((\overline{x_{i,k}} \vee \overline{x_{j,k}})\) with \(i \ne j\) is transformed into \((x_{\gamma (k),\sigma (i)} \vee x_{\gamma (k),\sigma (j)})\), which is also a Type 2 clause in F since \(\sigma\) and \(\gamma\) are bijections.
Finally, for every Type 3 clause \((\overline{x_{a,u}} \vee \overline{x_{b,v}}) \in F\), we would have \(\lbrace a,b \rbrace \in E_G \Leftrightarrow \lbrace u,v \rbrace \not\in E_H\), and this implies \(\lbrace \sigma (a),\sigma (b) \rbrace \in E_H \Leftrightarrow \lbrace \gamma (u),\gamma (v) \rbrace \not\in E_G\), and therefore \((\overline{x_{\gamma (u),\sigma (a)}} \vee \overline{x_{\gamma (v),\sigma (b)}})\) also belongs to F. The situation in which \(\sigma\) and \(\gamma\) are both anti-isomorphisms is completely analogous.□
Notice that if G is non-isomorphic to H and G is also non-isomorphic to the complementary graph \(\overline{H}\), then in case there is a renaming \(f(F) \subseteq F\), we can only be dealing with Case 1 in the lemma. Moreover, by Observation 4.3, if the graphs G and H do not have any non-trivial automorphisms, they cannot have anti-automorphisms either. In this case, a non-trivial renaming f with \(f(F)\subseteq F\) cannot exist, and therefore the global symmetry rule cannot be applied. This implies that size lower bounds for the resolution of (non)isomorphism formulas for asymmetric graphs coincide with their size lower bounds for the system SRC-1.
Cai, Fürer, and Immerman [9] constructed pairs of graphs \((G, H)\) with a large Weisfeiler–Leman dimension. They showed a linear lower bound (in the number of vertices) of the WL-dimension k. These graphs have bounded degree, and therefore it also holds that G is non-isomorphic to \(\overline{H}\). A related construction of graphs satisfying this property, known as multipedes, was given in Reference [24]. However, the resulting graphs are very large in terms of the WL-dimension. Neuen and Schweitzer improved in Reference [36] the multipede construction, combining it with size reduction techniques. Using a different construction, Dawar and Khan [12] showed that there is a random process that produces with high probability graphs whose Weisfeiler–Leman dimension is linear in the number of their vertices (as with the CFI graphs) and without any non-trivial automorphisms.
For \(k \in \mathbb {N}\), there is a family of asymmetric pairs of graphs \((G_k, \lambda _k)\) and \((H_k, \mu _k)\) with \(\mathrm{O}(k)\) vertices, color classes of size 4, and Weisfeiler–Leman dimension k. It also holds \(G_k \not\cong H_k\) and \(G_k \not\cong \overline{H_k}\).
In Reference [12], it was furthermore demonstrated by conducting experiments that the resulting graphs provide hard examples for graph isomorphism solvers, matching the hardest-known benchmarks for graph isomorphism. The following result can be seen as a theoretical insight into this phenomenon.
The discussion following Corollary 3.13 implies that the isomorphism formulas for the pairs \((G_k, H_k)\) of non-isomorphic graphs from the above-mentioned construction have resolution refutations of size \({\exp } (\Omega (n))\), where n is the number of vertices in the graphs (linear in the WL-dimension k). Since these graphs are asymmetric, from Lemma 4.4, we conclude as follows:
There is a family of non-isomorphic graph pairs \((G_n, H_n)\) with \(\mathrm{O}(n)\) vertices each, such that any refutation of \(\mathrm{ISO}(G_n,H_n)\) requires size \({\exp }(\Omega (n))\) in the SRC-1 proof system.
5 Lower Bounds On Clause Space for Proving Non-isomorphism
Atserias and Dalmau [3] gave a combinatorial characterization of resolution width and used it to show the relation \({\mathrm{CS}}_{}{(F \mathrel {\mathop \vdash }\!\square)} \ge {\mathrm{Width}}_{}{(F \mathrel {\mathop \vdash }\!\square)} - \text{Width}(F) + 1\) for every \(F \in \mathrm{UNSAT}\). We will show in this section that this also holds for narrow width, with the advantage that, in this case, again, we do not have to worry about the width of the axioms. From this result, we obtain clause space lower bounds for the (normal) resolution of isomorphism formulas. Our first step will be to adapt the concept of a width-family of assignments (or AD-family) from Reference [3] to narrow resolution, defining narrow-width-families:
Given an unsatisfiable CNF formula F and a natural number \(w \in \mathbb {N}\), we say that a family of assignments \(\mathscr{F}\) for F is a w-NW family if all of the following properties hold:
(1)
\(\mathscr{F}\ne \varnothing\),
(2)
\(\forall \alpha \in \mathscr{F}\) and \(\forall C \in F\): \(C|_\alpha \ne \square\),
(3)
\(\forall \alpha \in \mathscr{F}\): \(|\operatorname{Dom}(\alpha)| \le w\),
(4)
\(\forall \alpha \in \mathscr{F}\) and \(\forall \beta \subseteq \alpha\): \(\beta \in \mathscr{F}\),
(5)
\(\forall \alpha \in \mathscr{F}\) with \(| \operatorname{Dom}(\alpha) | \le w-1\) and \(\forall x \in \mathrm{Vars}({F|_{\alpha }})\): \(\alpha \lbrace x = 0 \rbrace \in \mathscr{F}\) or \(\alpha \lbrace x = 1 \rbrace \in \mathscr{F}\),
(6)
\(\forall \alpha \in \mathscr{F}\) with \(| \operatorname{Dom}(\alpha) | \le w-1\) and \(\forall C \in F|_{\alpha }\): \(\exists \ell \in C\) such that \(\alpha \lbrace \ell = 1 \rbrace \in \mathscr{F}\).
Notice, that Properties (1)–(5) are as in the definition of Atserias and Dalmau [3]. We added Property (6) to deal with narrow width. The following theorem adapts [3] to narrow width.
Let F be an unsatisfiable CNF formula. Then it holds:
From left to right, let \({\mathrm{N\text{-}Width}}_{}{(F \mathrel {\mathop \vdash }\!\square)} \ge w\). We will construct a w-NW family \(\mathscr{F}\) for F by first considering the setWe can define the w-NW family for F asWe proceed by verifying Properties (1)–(6) for the constructed family \(\mathscr{F}\). Since \({\mathrm{N\text{-}Width}}_{}{(F \mathrel {\mathop \vdash }\!\square)} \ge w\), we know that \(\square \not\in \mathscr{C}\), thus \(\varepsilon \in \mathscr{F}\), implying that \(\mathscr{F}\ne \varnothing\). By construction, \(\mathscr{F}\) clearly also has Properties (2) and (3). Property (4) is trivial.
\begin{equation*} \mathscr{C} := \lbrace C \,\vert \, \mathrm{N\text{-}Width}(F \vdash C) \le w-1 \rbrace . \end{equation*}
\begin{equation*} \mathscr{F}:= \lbrace \alpha \,\vert \, \forall C \in \mathscr{C} \cup F: \: C|_\alpha \ne \square \rbrace \cap \lbrace \alpha \,\vert \, |\operatorname{Dom}(\alpha)| \le w \rbrace . \end{equation*}
To show Property (5), suppose we have an \(\alpha \in \mathscr{F}\) with \(|\operatorname{Dom}(\alpha)| \le w-1\) and suppose further that there is a variable \(x \not\in \operatorname{Dom}(\alpha)\) such that \(\alpha _0 := \alpha \lbrace x = 0 \rbrace \not\in \mathscr{F}\) and \(\alpha _1 := \alpha \lbrace x=1 \rbrace \not\in \mathscr{F}\). By construction of the family, \(\alpha _0\) falsifies some clause \(C_0 \in \mathscr{C} \cup F\). Similarly, \(\alpha _1\) falsifies some clause \(C_1 \in \mathscr{C} \cup F\). However, since \(\alpha \in \mathscr{F}\) it cannot falsify \(C_0\) nor \(C_1\). Because \(\alpha _0\) and \(\alpha _1\) only differ from \(\alpha\) in one literal, the clauses thus must have the form \(C_0 = C_0^\prime \vee x\) with \(C_0^\prime |_\alpha = 0\) and \(C_1 = C_1^\prime \vee \overline{x}\) with \(C_1^\prime |_{\alpha } = 0\). Since \(|\operatorname{Dom}(\alpha)| \le w-1\), at most \(w-1\) literals can be falsified by \(\alpha\). Thus, \(|C_0^\prime \vee C_1^\prime | \le w-1\). In case both \(C_0\) and \(C_1\in \mathscr{C}\) then using resolution, one can derive \(C_0^\prime \vee C_1^\prime\) from \(C_0\) and \(C_1\), implying \(C_0^\prime \vee C_1^\prime \in \mathscr{C}\). Thus, \(\alpha\) would satisfy this clause, which is a contradiction. In the case at least one of the clauses \(C_0, C_1\) is in F, one could obtain \(C_0^\prime \vee C_1^\prime\) using a narrow resolution of width at most \(w-1\), and the same contradiction would follow.
It is only left to show that (6) holds: Suppose we have an \(\alpha \in \mathscr{F}\) with \(|\operatorname{Dom}(\alpha)| \le w-1\) and a clause \(C = (\ell _1 \vee \dots \vee \ell _m) \in F|_{\alpha }\) such that for all \(i \in [m]\) we have \(\alpha _{\ell _{i}} := \alpha \lbrace \ell _i = 1 \rbrace \not\in \mathscr{F}\). By construction of the family \(\mathscr{F}\), this means that each \(\alpha _{\ell _{i}}\) falsifies a clause \(C_{\ell _{i}} \in (\mathscr{C} \cup F)|_{\alpha }\). But since by assumption, \(\alpha\) does not falsify any clause in \(\mathscr{C} \cup F\), and each \(\alpha _{\ell _{i}}\) only differs from \(\alpha\) in the literal \(\ell _i\), we have \(C_{\ell _{i}} = (\overline{\ell _{i}})\). Thus, there are clauses \(B, A_1, \dots , A_m\) being falsified by \(\alpha\) such that \((B \vee C)\in F\), \((A_1 \vee \overline{\ell _1}), \dots , (A_m \vee \overline{\ell _m}) \in \mathscr{C} \cup F\) andis a valid narrow resolution step. Hence, it is possible to derive the clause \(B \vee A_1 \vee \dots \vee A_m\) from F in narrow resolution width \(|B \vee A_1 \vee \dots \vee A_m| \le | \operatorname{Dom}(\alpha) | \le w-1\). This clause is falsified by \(\alpha\). This is a contradiction to the definition of \(\mathscr{F}\).
\begin{equation*} \frac{(B \vee C) \:\:\:\:\:\: (A_1 \vee \overline{\ell _1}) \:\:\:\: \cdots \:\:\:\: (A_m \vee \overline{\ell _m})}{B \vee A_1 \vee \dots \vee A_m} \end{equation*}
For the other direction, suppose that there is a refutation \(\pi\) with \(\mathrm{N\text{-}Width}(\pi) \le w-1\). To reach a contradiction, assume that there is also a w-NW family \(\mathscr{F}\) for F. Beginning at the empty clause in \(G_{\pi }\), we will construct a path to an axiom of F such that for each clause C in this path, there is an assignment \(\alpha _C \in \mathscr{F}\) of size at most w that falsifies C. We do this by using induction over the length of the path. At the beginning, we can choose \(\alpha _{\square } := \varepsilon\). For the induction step, we distinguish between two cases.
First, suppose that \(C = (D_1 \vee D_2)\) is the resolvent of \((D_1 \vee x)\) and \((D_2 \vee \overline{x})\). Since \(\mathrm{N\text{-}Width}(\pi) \le w-1\), we can apply Property (5) to \(\alpha _C\) and obtain a value \(b \in \lbrace 0,1 \rbrace\) such that \(\alpha := \alpha _C \lbrace x=b \rbrace \in \mathscr{F}\). If \(b=0\), then we can follow the path toward \(D_1 \vee x\); otherwise toward \(D_2 \vee \overline{x}\). Using Property (4), the assignment can then be restricted to only use variables occurring in the new clause.
In the second case, we suppose that \((B \vee A_1 \vee \dots \vee A_m)\) is falsified by \(\alpha \in \mathscr{F}\) and that this clause is the narrow resolvent of the clauses \((B \vee \ell _1 \vee \dots \vee \ell _m), (A_1 \vee \overline{\ell _1}), \dots , (A_m \vee \overline{\ell _m})\). Since \(\mathrm{N\text{-}Width}(\pi) \le w-1\), we can apply Property (6) to \(\alpha\) and the axiom clause \((B \vee \ell _1 \vee \dots \vee \ell _m)\). Since \(B|_{\alpha } = \square\), this guarantees the existence of an \(i \in [m]\) such that \(\alpha _i := \alpha \lbrace \ell _i = 1 \rbrace \in \mathscr{F}\). But \(\alpha _i\) falsifies the clause \((A \vee \overline{\ell _i})\).
We end up in an axiom \(A \in F\) that is being falsified by an assignment \(\alpha _A \in \mathscr{F}\). This violates Property (2), a contradiction to the existence of the family \(\mathscr{F}\).□
The next result shows that the w parameter in an NW-family for a formula F provides a lower bound for the resolution clause space of F. The theorem is an adaptation of References [3, Lemma 5]. We notice that the original constant for the initial width of the formula, \(\text{Width}(F)\), vanishes by modifying Property (6) of the definition of an Atserias–Dalmau family, as we did.
If there is a w-NW family for an unsatisfiable CNF formula F, then
Let \(\mathscr{F}\) be a w-NW family for F. Assume, toward a contradiction, that there is a configurational refutation \(\pi = (\mathbb {M}_0, \dots , \mathbb {M}_{t})\) of F with \(\mathrm{CS_{}}(\pi) \lt w+1\). We will show that then every \(\mathbb {M}_i\) is satisfiable (which is clearly absurd because \(\square \in \mathbb {M}_{t}\)). This is done by using induction on i to obtain a sequence of partial assignments \(\alpha _i \in \mathscr{F}\) such that \(\alpha _i\) satisfies \(\mathbb {M}_i\) and \(|\operatorname{Dom}(\alpha _i)| \le | \mathbb {M}_i | \lt w+1\).
The base case can be chosen as \(\alpha _0 := \varepsilon\). For the induction step, suppose that \(\alpha _{i-1}\) has already been constructed. We distinguish three cases for \(\mathbb {M}_i\).
Case 1 (Axiom Download): \(\mathbb {M}_i = \mathbb {M}_{i-1} \cup \lbrace C \rbrace\) for some axiom \(C \in F\). If \(\alpha _{i-1}\) already assigns all literals in the downloaded resolvent C, then we can simply choose \(\alpha _{i} = \alpha _{i-1}\). Property (2) guarantees that C is not falsified by \(\alpha _{i}\), and since all literals are assigned, C must be satisfied by \(\alpha _{i}\). Furthermore, obviously \(|\operatorname{Dom}(\alpha _i)| \le | \mathbb {M}_i |\).
If, however, there is an unassigned literal in the downloaded resolvent under \(\alpha _{i-1}\), then we have to argue more carefully. Since we have, by assumption, \(\mathrm{CS_{}}(\pi) \lt w+1\), it must hold that \(\mathrm{CS_{}}(\mathbb {M}_{i-1}) \le w-1\) (since otherwise we had no more memory capacity for the newly downloaded clause C in \(\mathbb {M}_i\)). Since \(| \operatorname{Dom}(\alpha _{i-1}) | \le | \mathbb {M}_{i-1} | \le w-1\) and because \(\mathscr{F}\) is a w-NW family for F, Property (6) guarantees the existence of a literal \(\ell \in C|_{\alpha _{i-1}}\) such that \(\alpha _i := \alpha _{i-1} \lbrace \ell = 1 \rbrace \in \mathscr{F}\) satisfies C, and thus also \(\mathbb {M}_i\). It also holds \(|\operatorname{Dom}(\alpha _i)| = | \operatorname{Dom}(\alpha _{i-1}) | + 1 \le | \mathbb {M}_{i-1} | + 1 = | \mathbb {M}_i |\).
Case 2 (Inference): \(\mathbb {M}_i = \mathbb {M}_{i-1} \cup \lbrace R \rbrace\). In this case, we can simply set \(\alpha _i := \alpha _{i-1}\). Since \(\alpha _{i-1}\) satisfied \(\mathbb {M}_{i-1}\), the soundness of the resolution rule guarantees that the assignment also satisfies the resolvent R. Also, \(| \operatorname{Dom}(\alpha _i) | \le | \mathbb {M}_{i-1} | \le | \mathbb {M}_{i} |\) and \(\alpha _i \in \mathscr{F}\).
Case 3 (Erasure): \(\mathbb {M}_i = \mathbb {M}_{i-1} \setminus \lbrace C \rbrace\). The assignment \(\alpha _{i-1}\) still satisfies \(\mathbb {M}_i\). Since we need at most one satisfied literal for each clause in \(\mathbb {M}_i\), the assignment \(\alpha _i\) can be chosen as a subset of \(\alpha _{i-1}\) of size at most \(|\mathbb {M}_i|\) that still satisfies \(\mathbb {M}_i\) and belongs to \(\mathscr{F}\).□
For every unsatisfiable formula F, we have
Using the equivalence of narrow width and Immerman’s game (cf. Theorem 3.3), we obtain:
Let \(k \in \mathbb {N}\) and let G and H be two non-isomorphic graphs with \(G \equiv _{{\mathscr{L}}_{k}} H\). Then,
If \(G \equiv _{{\mathscr{L}}_{k}} H\), then \({\mathrm{N\text{-}Width}}_{}{(\mathrm{ISO}(G,H) \mathrel {\mathop \vdash }\!\square)} \gt k-1\), according to Theorem 3.3. Corollary 5.4 then yields \({\mathrm{CS}}_{}{(\mathrm{ISO}(G,H) \mathrel {\mathop \vdash }\!\square)} \ge {\mathrm{N\text{-}Width}}_{}{(\mathrm{ISO}(G,H) \mathrel {\mathop \vdash }\!\square)} + 1 \ge k +1\).□
There is a family of non-isomorphic pairs of graphs, \(((G_n,H_n))_{n \in \mathbb {N}}\), such that for every \(n \in \mathbb {N}\), the graphs \(G_n\) and \(H_n\) have n vertices and
Using the non-isomorphic graphs \(G_{2k}\) and \(H_{2k}\) from Remark 3.10, having \(n:= 2k\) vertices each, we know from Reference [38, Example 2.6] that \(G_{2k} \equiv _{{\mathscr{L}}_{k-1}} H_{2k}\). Thus, by the above result, we have the lower bound \({\mathrm{CS}}_{}{(\mathrm{ISO}(G_{2k},H_{2k}) \mathrel {\mathop \vdash }\!\square)} \ge k\). Since \(| \mathrm{Vars}({\mathrm{ISO}(G_{2k},H_{2k})}) | = n^2 = 4k^2\), the claim follows.□
To the best of our knowledge, this is the first resolution clause space lower bound for graph isomorphism formulas.
6 Conclusions
We have given an exact characterization for the number of variables needed to distinguish two graphs in first-order logic in terms of the narrow resolution width needed for refuting the corresponding isomorphism formulas. This fact allowed us to obtain upper and lower bounds for the size and space of (normal) resolution refutation of such formulas. The size upper bound justifies a clause length increasing algorithm for the resolution (and solving) of isomorphism formulas of the kind proposed in Reference [7] for general formulas.
The lower bound techniques provide a simplified method to obtain resolution size lower bounds directly from the structure of the graphs, using the \({\mathscr{L}}_{k}\)-logic, and without having to deal with resolution or with the isomorphism formulas directly. All the known resolution size lower bounds for isomorphism formulas can be easily derived from this result. Moreover, we have been able to use the method to obtain exponential lower bounds for isomorphism formulas in the stronger system of SRC-1, which includes a global symmetry rule, answering a question posed in Reference [40].
The obvious open question is to prove superpolynomial size lower bounds for isomorphism formulas in the stronger systems SRC-2 and SRC-3. However, one would need different ideas for this, since, as shown recently in Reference [40], the families of graphs based on the CFI construction, like the ones used in all known lower bounds, have polynomial-size SRC-2 refutations.
The role that the size of the color classes plays in Theorem 3.12 seems unintuitive. When the size of the color classes is large, the lower bounds become trivial, although in general, it becomes harder to decide non-isomorphism. It would be interesting to obtain resolution size lower bounds for isomorphism formulas without the color class restriction.
Related Version
An extended abstract of this article has been presented at Computer Science Logic (CSL) 2022; see Reference [44].
Acknowledgments
The authors thank Pascal Schweitzer for helpful discussions. Furthermore, the authors appreciate the many insightful comments of all the reviewers.
Footnote
1
The players are also called Spoiler and Duplicator in the literature. However, we will not use these names here as we will also consider (a version of) the Spoiler–Duplicator game later.
References
[1]
Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. 2002. Space complexity in propositional calculus. SIAM J. Comput. 31, 4 (2002), 1184–1211.
[2]
Noriko H. Arai and Alasdair Urquhart. 2000. Local symmetries in propositional logic. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’00). 40–51.
[3]
Albert Atserias and Víctor Dalmau. 2008. A combinatorial characterization of resolution width. J. Comput. Syst. Sci. 74, 3 (2008), 323–334. Earlier conference version in CCC’03.
[4]
Albert Atserias and Elitza N. Maneva. 2013. Sherali–Adams relaxations and indistinguishability in counting logics. SIAM J. Comput. 42, 1 (2013), 112–137. Earlier conference version in ITCS’12.
[5]
László Babai. 2016. Graph isomorphism in quasipolynomial time [extended abstract]. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing (STOC’16). 684–697.
[6]
László Babai and Shlomo Moran. 1988. Arthur–Merlin games: A randomized proof system, and a hierarchy of complexity classes. J. Comput. Syst. Sci. 36, 2 (1988), 254–276.
[7]
Eli Ben-Sasson and Avi Wigderson. 2001. Short proofs are narrow—Resolution made simple. J. ACM 48, 2 (2001), 149–169.
[8]
Christoph Berkholz and Martin Grohe. 2015. Limitations of algebraic approaches to graph isomorphism testing. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP’15). 155–166.
[9]
Jin-yi Cai, Martin Fürer, and Neil Immerman. 1992. An optimal lower bound on the number of variables for graph identifications. Combinatorica 12, 4 (1992), 389–410.
[10]
Paolo Codenotti, Grant Schoenebeck, and Aaron Snook. 2014. Graph isomorphism and the Lasserre hierarchy. arxiv:1401.0758. Retrieved from https://arxiv.org/abs/1401.0758.
[11]
Stephen A. Cook and Robert A. Reckhow. 1979. The relative efficiency of propositional proof systems. J. Symbol. Logic 44, 1 (1979), 36–50.
[12]
Anuj Dawar and Kashif Khan. 2019. Constructing hard examples for graph isomorphism. J. Graph Algor. Appl. 23, 2 (2019), 293–316.
[13]
Andrzej Ehrenfeucht. 1961. An application of games to the completeness problem for formalized theories. Fundam. Math. 49 (1961), 129–141.
[14]
Paul Erdös and Alfrëd Rényi. 1959. On random graphs I. Publ. Math. 6 (1959), 290–297.
[15]
Juan Luis Esteban, Nicola Galesi, and Jochen Messner. 2004. On the complexity of resolution with bounded conjunctions. Theor. Comput. Sci. 321, 2-3 (2004), 347–370. Earlier conference version in ICALP’02.
[16]
Juan Luis Esteban and Jacobo Torán. 2001. Space bounds for resolution. Inf. Comput. 171, 1 (2001), 84–97. Preliminary versions in STACS’99 and CSL’99.
[17]
Roland Fraïssé. 1950. Sur une nouvelle classification des systémes de relations. Compt. Rend. 230 (1950), 1022–1024.
[18]
Frank Fuhlbrück, Johannes Köbler, Ilia Ponomarenko, and Oleg Verbitsky. 2021. The Weisfeiler–Leman algorithm and recognition of graph properties. Theor. Comput. Sci. 895 (2021), 96–114.
[19]
Merrick L. Furst, John E. Hopcroft, and Eugene M. Luks. 1980. In Proceedings of the 21st Annual Symposium on Foundations of Computer Science (FOCS’80). 36–41.
[20]
Nicola Galesi and Neil Thapen. 2005. Resolution and pebbling games. In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT’05). 76–90.
[21]
Zvi Galil. 1977. On resolution with clauses of bounded size. SIAM J. Comput. 6, 3 (1977), 444–459.
[22]
Edgar Nelson Gilbert. 1959. Random graphs. Ann. Math. Stat. 30, 4 (1959), 1141–1144.
[23]
Martin Grohe and Martin Otto. 2015. Pebble games and linear equations. J. Symbol. Logic 80, 3 (2015), 797–844. Earlier conference version in CSL’12.
[24]
Yuri Gurevich and Saharon Shelah. 1996. On finite rigid structures. J. Symbol. Logic 61, 2 (1996), 549–562.
[25]
Armin Haken. 1985. The intractability of resolution. Theor. Comput. Sci. 39 (1985), 297–308.
[26]
Neil Immerman. 1982. Upper and lower bounds for first order expressibility. J. Comput. Syst. Sci. 25, 1 (1982), 76–98. Earlier conference version in FOCS’80.
[27]
Neil Immerman. 1999. Descriptive Complexity. Springer.
[28]
Sandra Kiefer. 2020. Power and Limits of the Weisfeiler–Leman Algorithm. Dissertation. RWTH Aachen University.
[29]
Sandra Kiefer. 2020. The Weisfeiler–Leman algorithm: An exploration of its power. ACM SIGLOG News 7, 3 (2020), 5–27.
[30]
Jeong Han Kim, Oleg Pikhurko, Joel H. Spencer, and Oleg Verbitsky. 2005. How complex are random graphs in first order logic? Rand. Struct. Algor. 26, 1-2 (2005), 119–145.
[31]
Pavel Klavík, Dusan Knop, and Peter Zeman. 2021. Graph isomorphism restricted by lists. Theor. Comput. Sci. 860 (2021), 51–71. Earlier conference version in WG’20.
[32]
Johannes Köbler, Uwe Schöning, and Jacobo Torán. 1993. The Graph Isomorphism Problem: Its Structural Complexity. Birkhäuser/Springer.
[33]
Balakrishnan Krishnamurthy. 1985. Short proofs for tricky formulas. Acta Inf. 22, 3 (1985), 253–275.
[34]
Anna Lubiw. 1981. Some NP-complete problems similar to graph isomorphism. SIAM J. Comput. 10, 1 (1981), 11–21.
[35]
Peter N. Malkin. 2014. Sherali–Adams relaxations of graph isomorphism polytopes. Discr. Optim. 12 (2014), 73–97.
[36]
Daniel Neuen and Pascal Schweitzer. 2018. An exponential lower bound for individualization-refinement algorithms for graph isomorphism. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing (STOC’18). ACM, 138–150.
[37]
Ryan O’Donnell, John Wright, Chenggang Wu, and Yuan Zhou. 2014. Hardness of robust graph isomorphism, lasserre gaps, and asymmetry of random graphs. In Proceedings of the 25th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA’14). 1659–1677.
[38]
Oleg Pikhurko, Helmut Veith, and Oleg Verbitsky. 2006. The first order definability of graphs: Upper bounds for quantifier depth. Discr. Appl. Math. 154, 17 (2006), 2511–2529.
[39]
Alexander A. Razborov. 2001. Proof complexity of pigeonhole principles. In Proceedings of the 5th International Conference on Developments in Language Theory (DLT’01), Revised Papers. 100–116.
[40]
Pascal Schweitzer and Constantin Seebach. 2021. Resolution with symmetry rule applied to linear equations. In Proceedings of the 38th International Symposium on Theoretical Aspects of Computer Science (STACS’21). 58:1–58:16.
[41]
Hanif D. Sherali and Warren P. Adams. 1990. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Discr. Math. 3, 3 (1990), 411–430.
[42]
Stefan Szeider. 2005. The complexity of resolution with generalized symmetry rules. Theory Comput. Syst. 38, 2 (2005), 171–188. Earlier conference version in STACS’03.
[43]
Jacobo Torán. 2013. On the Resolution complexity of graph non-isomorphism. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT’13). 52–66.
[44]
Jacobo Torán and Florian Wörz. 2022. Number of variables for graph differentiation and the resolution of GI formulas. In Proceedings of the 30th EACSL Annual Conference on Computer Science Logic (CSL’22),LIPIcs, Vol. 216. 36:1–36:18.
[45]
Grigori S. Tseitin. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2. Seminars in Mathematics, Vol. 8. Consultants Bureau, 115–125.
[46]
Alasdair Urquhart. 1999. The symmetry rule in propositional logic. Discr. Appl. Math. 96-97 (1999), 177–193.
[47]
Boris Weisfeiler. 1976. On Construction and Identification of Graphs. Lecture Notes in Mathematics, Vol. 558. Springer.
[48]
Boris Weisfeiler and Andrei Leman. 1968. The reduction of a graph to canonical form and the algebra which appears therein. Nauch.-Technichesk. Inf. Ser. 2 9 (1968).
Index Terms
- Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas
Recommendations
The resolution complexity of random graph k-colorability
We consider the resolution proof complexity of propositional formulas which encode random instances of graph k-colorability. We obtain a tradeoff between the graph density and the resolution proof complexity. For random graphs with linearly many edges ...
Planar Graph Isomorphism is in Log-Space
CCC '09: Proceedings of the 2009 24th Annual IEEE Conference on Computational ComplexityGraph Isomorphism is the prime example of a computational problem with a wide difference between the best known lower and upper bounds on its complexity. There is a significant gap between extant lower and upper bounds for planar graphs as well. We ...
Tight Lower Bounds on the Resolution Complexity of Perfect Matching Principles
Discrete Mathematics (RuFiDiM 14)The resolution complexity of the perfect matching principle was studied by Razborov [1], who developed a technique for proving its lower bounds for dense graphs. We construct a constant degree bipartite graph Gn such that the resolution complexity of the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2023
268 pages
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 07 April 2023
Online AM: 21 January 2023
Accepted: 04 January 2023
Revised: 12 October 2022
Received: 15 November 2021
Published in TOCL Volume 24, Issue 3
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- Deutsche Forschungsgemeinschaft (DFG)
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 814Total Downloads
- Downloads (Last 12 months)440
- Downloads (Last 6 weeks)52
Reflects downloads up to 10 Dec 2024
Other Metrics
Citations
Cited By
View all- Torán JWörz F(2024)Cutting Planes Width and the Complexity of Graph Isomorphism RefutationsACM Transactions on Computational Logic10.1145/367712125:4(1-25)Online publication date: 18-Jul-2024
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatLogin options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in