Proof sketch.. Let \((G_i,\lambda_i^*,\mu_i^*)\) be the restriction of \((G,\lambda \oplus \lambda',\mu \otimes \mu')\) to \(V_0 \cup (\bigcup_{j=1}^i V_j)\). Roughly speaking, the idea for computing \(\mathsf{sgn}_{S'}(G,\lambda \oplus \lambda',\mu \otimes \mu')\) is to keep applying Lemma 1 to iteratively compute \(\mathsf{sgn}_{S'}(G_i,\lambda_i^*,\mu_i^*)\) for \(i = 0,1,\dots,r'\). By construction, \((V(G_{i-1}),V_i)\) is a separation of \(G_i\). As such, Lemma 1 allows us to compute \(\mathsf{sgn}_{S'}(G_i,\lambda_i^*,\mu_i^*)\) from \(\mathsf{sgn}_{S'}(G_{i-1},\lambda_{i-1}^*,\mu_{i-1}^*)\) and the given signature \(\mathsf{sgn}_{S'}(G[V_i],\lambda_i,\mu_i \otimes \tau_i)\), together with some other information that is encoded in the given graph \((G[V_0],\lambda_0 \oplus \pi_1 \oplus \cdots \oplus \pi_{r'},\mu_0)\). Note that \((G_{r'},\lambda_{r'}^*,\mu_{r'}^*) = (G,\lambda \oplus \lambda',\mu \otimes \mu')\). So we end up with the desired signature \(\mathsf{sgn}_{S'}(G,\lambda \oplus \lambda',\mu \otimes \mu')\).

We remark that the actual proof of this lemma is more technical than our discussion above. In fact, applying Lemma 1 does not enable us to compute \(\mathsf{sgn}_{S'}(G_i,\lambda_i^*,\mu_i^*)\) from \(\mathsf{sgn}_{S'}(G_{i-1},\lambda_{i-1}^*,\mu_{i-1}^*)\) and \(\mathsf{sgn}_{S'}(G[V_i],\lambda_i,\mu_i \otimes \tau_i)\). Therefore, in the actual proof, we need to compute the \(S'\)-signature of a graph more complicated than \((G_i,\lambda_i^*,\mu_i^*)\) in each iteration, in order to make the induction work. For simplicity, we omit the details here. ◻

Proof. Consider a nice tree decomposition \((T,\beta)\) of \(G\) with width \(t\). For a subset \(X \subseteq V(T)\), we write \(\beta(X) = \bigcup_{x \in X} \beta(x)\) for convenience. For each vertex \(v \in R\), we pick an arbitrary node \(x_v \in V(T)\) such that \(v \in \beta(x_v)\). Let \(X \subseteq V(T)\) be the minimal subset such that \(x_v \in X\) for all \(v \in R\) and \(T[X]\) is connected, or equivalently, \(X\) consists of the nodes on the paths in \(T\) between vertices in \(\{x_v: v \in R\}\). By construction, \(T[X]\) is a tree whose leaves are in \(\{x_v: v \in R\}\). Define \(X^* \subseteq X\) as the subset consisting of the nodes in \(\{x_v: v \in R\}\) and all nodes with degree at least \(3\) in \(T[X]\). Since the number of leaves of \(T[X]\) is at most \(|R| \leq r\), we have \(|X^*| \leq 2r\). As \((T,\beta)\) is a nice tree decomposition, the maximum degree of \(T\) is \(3\) and thus \(T - X^*\) has at most \(3|X^*| \leq 6r\) connected components. Let \(C_1,\dots,C_m\) be the connected components of \(T - X^*\). We observe that each \(C_i\) is adjacent to at most two nodes in \(X^*\). Indeed, if \(C_i\) is adjacent to three nodes \(x_1,x_2,x_3 \in X^*\), then there exists \(x \in C_i\) such that \(x_1,x_2,x_3\) belong to different connected components of \(T-x\), which implies \(x \in X\). It also follows that \(x \in X^*\), as the degree of \(x\) in \(T[X]\) is at least \(3\) because of \(x_1,x_2,x_3\). This contradicts the fact that \(x \in C_i\). Thus, there are at most two nodes in \(X^*\) adjacent to \(C_i\) in \(T\).

Define \(V_0 = \beta(X^*)\), \(V_i = N_G[\beta(C_i) \backslash \beta(X^*)]\) for \(i \in [m]\), and \(V_i = \emptyset\) for \(i \in \{m+1,\dots,6r\}\). Clearly, \(R \subseteq V_0\) and we have \(|V_0| \leq t|X^*| = O(rt)\). The fact \(V(G) = \bigcup_{i=0}^{6r} V_i\) follows from that \(V(G) = \beta(X^*) \cup (\bigcup_{i=1}^m \beta(C_i))\). To see the other properties, consider an index \(i \in [6r]\). If \(i > m\), then \(N_G(V_i \backslash V_0) = \emptyset\) and \(V_0 \cap V_i = \emptyset\). Otherwise, \(V_i = N_G[\beta(C_i) \backslash \beta(X^*)]\). Let \(U_i = \beta(C_i) \backslash \beta(X^*)\). Also, let \(X_i^* \subseteq X^*\) consist of the (at most two) nodes in \(X^*\) adjacent to \(C_i\) in \(T\). We observe that \(N_G(U_i) \subseteq \beta(X_i^*) \subseteq V_0\). Consider a vertex \(v \in N_G(U_i)\) and let \(u \in U_i\) be a neighbor of \(v\). Then there exists a node \(x \in V(T)\) with \(u,v \in \beta(x)\). If \(x \in V(T) \backslash C_i\), then \(u \in \beta(X_i^*)\), because in this case \(u \in \beta(C_i) \cap \beta(V(T) \backslash C_i)\) and the property of a tree decomposition guarantees that the bag of some vertex in \(X_i^*\) contains \(u\). This contradicts the fact that \(u \in U_i\). Thus, \(x \in C_i\). Since \(v \notin U_i\), there exists a node \(y \in V(T) \backslash C_i\) with \(v \in \beta(y)\). Note that the path between \(x\) and \(y\) in \(T\) intersects \(X_i^*\). This implies \(v \in \beta(X_i^*)\), as \(v \in \beta(x)\) and \(v \in \beta(y)\). As such, \(N_G(U_i) \subseteq \beta(X_i^*) \subseteq V_0\). By construction, \(N_G(U_i) \subseteq V_i\) and hence \(N_G(U_i) \subseteq V_0 \cap V_i\). Furthermore, as \(V_0 \cap U_i = \emptyset\), we have \(V_0 \cap V_i = V_0 \cap N_G[U_i] = V_0 \cap N_G(U_i) = N_G(U_i)\), which implies \[|V_0 \cap V_i| = |N_G(U_i)| \leq |\beta(X_i^*)| \leq (t+1)\cdot |X_i^*| \leq 2(t+1) \leq 4t.\] To further have \(|V_0 \cap V_i| = 4t\), we can arbitrarily add some vertices in \(V_0\) to \(V_i\) (note that by doing this, the other properties preserve). ◻

Proof. If \(G\) is an \(n\)-vertex (unlabeled) graph of \(n\) vertices and treewidth at most \(t\), then \(|E(G)| \leq tn\). Thus, the number of \(n\)-vertex (unlabeled) graphs with treewidth at most \(t\) is bounded by \(n^{2tn}\) up to isomorphism. Furthermore, there can be \(n^c\) different \(c\)-labelings for an \(n\)-vertex graph. So there are at most \(n^{2tn} \cdot n^c = n^{2tn+c}\) different \(n\)-vertex \(c\)-labeled graphs with treewidth at most \(t\). Considering the graphs with \(i\) vertices for \(i = 1,\dots,n\), we finally obtain the desired bound \(n^{2tn+c+1}\). ◻

Proof. If \(\mathsf{core}(\sigma) \neq \sigma\), then there is no graph \((G,\lambda,\mu)\) satisfying the condition \(\mathsf{core}(G,\lambda_{|[p]},\mu) = \sigma\). As such, assume \(\mathsf{core}(\sigma) \neq \sigma\), which implies that \(\sigma\) contains at most \(p\) vertices. Let \(\sigma = (H,\gamma,\tau)\). A graph \((G,\lambda,\mu)\) under consideration can be obtained from \(\sigma\) by adding a set \(V'\) of (at most) \(r\) vertices, adding a set \(E\) of edges between the vertices in \(V(H)\) and the vertices in \(V'\), adding a set \(E'\) of edges among the vertices in \(V'\), and specifying two functions \(\lambda': [q] \rightarrow V(H) \cup V'\) and \(\mu': V' \rightarrow P\). Then we simply set \(V(G) = V(G) \cup V'\), \(E(G) = E(H) \cup E \cup E'\), \(\lambda = \gamma \oplus \lambda'\), and \[\mu(v) = \left\{ \begin{array}{ll} \tau(v) & \text{if } v \in V(H), \\ \mu'(v) & \text{if } v \in V'. \end{array} \right.\] As we need to guarantee that \(\mathbf{tw}(G) \le t\), we must have \(|E| \leq \min\{(pr,(p+r)t\} \leq \min\{r,t\} \cdot (p+r)\) and \(|E'| \leq \min\{r^2,rt\} \leq \min\{r,t\} \cdot (p+r)\). Therefore, the number of choices for \(E\) and \(E'\) is bounded by \((p+r)^{O(\min\{r,t\} \cdot (p+r))}\). The number of choices for \(\lambda'\) is \((p+r)^q\), and the number of choices for \(\mu'\) is at most \(|P|^r\). So the bound \((p+r)^{O(\min\{r,t\} \cdot (p+r)+q)} \cdot |P|^{O(r)}\) follows. ◻

Proof. Assume \(a_1 \geq \dots \geq a_m\) without loss of generality. We have \(b^{\sum_{i=1}^m b^{a_i}} = b^{m \cdot b^{a_1}} \leq \exp_{bm}^{(2)}(a_1)\). Thus, the inequality \(b^{\sum_{i=1}^m b^{a_i}} \leq \sum_{i=1}^m \exp_{bm}^{(2)}(a_i)\) follows. ◻

Proof. We first show that \(\exp_b^{(r)} (x) \leq \exp^{(r)} (b(x+1))\) for all \(x \in \mathbb{R}_{\geq 0}\). This can be done by induction on \(r\). When \(r = 0\), the inequality trivially holds. Suppose it holds for \(r-1\). Then \[\exp_b^{(r)} (x) = \exp_b^{(r-1)} (b^x) \leq \exp^{(r-1)} (b(b^x+1)) \leq \exp^{(r)} (\log b \cdot (x+1) + 1) \leq \exp^{(r)} (b(x+1)).\] Note that \(b(x+1) \leq \max\{x \log (x+1),8^{b}\}\), since if \(2b \leq \log (x+1)\) and \(x \geq 1\), then \(b(x+1) \leq 2bx \leq x \log (x+1)\), otherwise \(b(x+1) \leq b\cdot 2^{2b}+ 2b \leq 8^b\). Thus, by setting \(c = \exp^{(r)} (3b)\), we have \(\exp^{(r)} (b(x+1)) \leq c \cdot \exp^{(r)} (x \log (x+1))\). ◻

Proof. Define \(f(x) = 2^{\log x + (\log (2x+4)/ \log\log (2x+4))} + 100\) for all \(x \in \mathbb{R}_{\geq 0}\). Clearly, \(f\) is almost linear and well-behaved. We observe two basic properties of \(f\): for all \(x \in \mathbb{R}_{\geq 0}\),

(i) \(f(x) \geq 2 x \log x \geq 2 x \log_b x\),

(ii) \((f(x)-x) / \log(f(x)-x) > 2x+2\).

To see \(f\) satisfies the desired property, assume without loss of generality that \(a_1 \geq \cdots \geq a_r\). Then we have the inequality \[\left(\sum_{i=1}^r \exp_b^{(2)}(a_i)\right)^z \leq r^z (\exp_b^{(2)}(a_1))^z = r^z \cdot b^{b^{a_1}z}.\]

We claim that \(b^{b^{a_1}z} \leq b^{b^b}(b^{f(z)} + b^{b^{f(a_1)}})/z^z\). Note that if this is true, then we are done, because \(r^z \cdot b^{b^{a_1}z} \leq (\frac{r}{z})^z b^{b^b} \cdot (b^{f(z)} + b^{b^{f(a_1)}}) \leq r^r b^{b^b} \cdot (b^{f(z)} + b^{b^{f(a_1)}}) \leq r^r b^{b^b} \cdot (b^{f(z)} + \sum_{i=1}^r b^{b^{f(a_i)}})\), which implies the desired inequality. If \(b^{f(a_1)} \geq b^{a_1} z + z \log_b z\), then \(b^{b^{a_1}z} \leq b^{b^{f(a_1)}}/z^z \leq (b^{f(z)} + b^{b^{f(a_1)}})/z^z\). So we only need to consider the case \(b^{f(a_1)} < b^{a_1} z + z \log_b z\). We shall show \(f(z) + b^{2 \log b} - z \log_b z \geq b^{a_1}z\) and therefore \(b^{b^{a_1}z} \leq b^{b^{2 \log b}} (b^{f(z)}/z^z) \leq b^{b^{2 \log b}} (b^{f(z)} + b^{b^{f(a_1)}})/z^z\). Consider the following two cases.

• Case 1: \(\log_b z \geq b^{a_1}\). In this case, we have \(b^{a_1} z \leq z \log_b z\). Property (i) of \(f\) above then implies \(f(z) - z \log_b z \geq z \log_b z \geq b^{a_1}z\).

• Case 2: \(\log_b z < b^{a_1}\). In this case, we have \(b^{f(a_1)} < b^{a_1} z + z \log_b z < 2z \cdot b^{a_1}\), which implies \(\log_b (2z) > f(a_1)-a_1\) and therefore \[\frac{\log_b (2z+4)}{\log \log_b (2z+4)} \geq \frac{\log_b (2z)}{\log \log_b (2z)} > \frac{f(a_1)-a_1}{\log(f(a_1)-a_1)} > 2 a_1+2,\] where the last \(>\) follows from property (ii) of \(f\). If \(\log\log (2z+4) \geq 2 \log\log b\), then \(\frac{\log_b (2z+4)}{\log \log (2z+4)} \geq \frac{\log_b (2z+4)}{2 \log \log_b (2z+4)} > a_1+1\). It follows that \[f(z) - z \log_b z \geq f(z)/2 = (z/2) \cdot b^{\log_b (2z+4)/ \log\log (2z+4)} \geq (z/2) \cdot b^{a_1+1} \geq b^{a_1} z.\] On the other hand, if \(\log\log (2z+4) < 2 \log\log b\), then it holds that \(b^{2 \log b} \geq z^2\). The inequality \(b^{f(a_1)} < b^{a_1} z + z \log_b z\) implies \(z > b^{a_1}\) and thus \(b^{2 \log b} \geq b^{a_1} z\). As \(f(z) > z \log_b z\) by property (i) of \(f\), we have \(f(z) + b^{2 \log b} - z \log_b z \geq b^{a_1}z\).

In both cases, we have \(f(z) + b^{2 \log b} - z \log_b z \geq b^{a_1}z\). This completes the proof. ◻

Proof. The proof is by induction on \(|S|=d\). To prove item (iii), we will need to prove a more general item, termed (iii*), defined as follows:

Let \((A,B)\) be a separation of \(G\) with \(|A \cap B| = z\) and \(\mu':V(G) \rightarrow [z]_0\) be a function that maps all vertices in \(V(G) \backslash (A \cap B)\) to \(0\) and maps \(A \cap B\) bijectively to \([z]\). Let \(I_A,I_B\subseteq [p]\) such that \(I_A\cup I_B=[p]\) and \(|I_A|+|I_B|-|I_A\cap I_B|=p\). Additionally, let \(J_A,J_B\subseteq [p]\) such that \(|I_A|=|J_A|\) and \(|I_B|=|J_B|\). Let \(\lambda_A: [p_A]\rightarrow A\) and \(\lambda_B: [p_B]\rightarrow B\) be a \(p_A\)-labeling of \(G[A]\) and a \(p_B\)-labeling of \(G[B]\) whose domains contain \(J_A\) and \(J_B\), respectively.. Additionally, let \(\mu_A: A\rightarrow P\) and \(\mu_B: B\rightarrow P\) be two \(P\)-colorings of \(G[A]\) and \(G[B]\), respectively.

We say that a \(p\)-labeling \(\lambda^*\) of \(G\) is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible if \({\lambda^*}^{-1}(A)=I_A\), \({\lambda^*}^{-1}(B)=I_B\), \(\mathsf{sort}({\lambda_A}_{|J_A})=\mathsf{sort}(\lambda^*_{|I_A})\), \(\mathsf{sort}({\lambda_B}_{|J_B})=\mathsf{sort}(\lambda^*_{|I_B})\). Notice that if there exists a \(p\)-labeling that is \((I_A,I_B,\lambda_A,\lambda_B)\)-compatible, then it is unique.

Similarly, we say that \(P\)-coloring \(\mu^*\) of \(G\) is \((\mu_A,\mu_B)\)-compatible if \(\mu_A=\mu^*_{|A}\) and \(\mu_B=\mu^*_{|B}\). Notice that if there exists a \(P\)-coloring that is \((\mu_A,\mu_B)\)-compatible, then it is unique.

Then given only \(S\), \(I_A,I_B,J_A,J_B,\), \(\mathsf{sgn}_S(G[A],\lambda_A,\mu_A)\), and \(\mathsf{sgn}_S(G[B],\lambda_B,\mu_B)\), one can either:

1. Determine that there does not exist a \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible or there does not exist a \(P\)-coloring that is \((\mu_A,\mu_B)\)-compatible (or both).

2. For \(\lambda^*\) and \(\mu^*\) being the \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible and the \(P\)-coloring that is \((\mu_A,\mu_B)\)-compatible, compute the signature \(\mathsf{sgn}_S(G,\lambda^*,\mu^*)\).

Furthermore, this is to be done in time \[2^{\sum_{i=1}^dk_i}\cdot\left(\sum_{i=1}^d (k_i+s_i) + \lVert \mathsf{sgn}_S(G[A],\lambda_A,\mu_A) \rVert + \lVert \mathsf{sgn}_S(G[B],\lambda_B,\mu_B) \rVert\right)^{O(1)}.\]

Let us denote \((H,\alpha',\beta)=\mathsf{sgn}_S(G,\lambda',\mu)\). Define \(\alpha = \alpha'\circ f\). Then, \((H,\alpha,\beta)=\mathsf{sgn}_S(G,\lambda,\mu)\).

Let us denote \((H,\alpha,\beta')=\mathsf{sgn}_S(G,\lambda,\mu')\). Define \(\beta= f\circ \beta'\). Then, \((H,\alpha,\beta)=\mathsf{sgn}_S(G,\lambda,\mu)\).

Let us denote \((H_A,\alpha_A,\beta_A)=\mathsf{sgn}_S(G[A],\lambda_A,\mu_A)\), and \((H_B,\alpha_B,\beta_B)=\mathsf{sgn}_S(G[B],\lambda_B,\mu_B)\). First, notice that \(z=|\{i\in\mathbb{N}: \exists X\) s.t. \((X,i)\in\mathsf{image}(\beta_A)\}|\), and \(p=|I_A|+|I_B|-|I_A\cap I_B|\). Thus, we suppose to have \(z\) and \(p\) at hand. Due to the renaming of vertices, we must observe that two vertices \(u\) in \(H_A\) and \(v\) in \(H_B\) should be “treated” as the same vertex (i.e., they are different names of the same vertex in \(A\cap B\)) if and only if: there exist \(i\in [z],X\) for which \(\beta_A(u)=(X,i)\) and \(\beta_B(v)=(X,i)\). Accordingly, we define a function \(\mathsf{retrace}: V(H_B)\rightarrow V(H_A)\) as follows: for every \(u\in V(H_B)\), if \(\beta_B(u)=(X,i)\) for some (unique) \(i\in[z]\), then \(\mathsf{retrace}(u)=\beta_A(X,i)\), and otherwise \(\mathsf{retrace}(u)=u\). Moreover, let \(M_A\) be the set of vertices in the image of \(\mathsf{retrace}\) that do not belong to \(B\), and let \(M_B\) be the set of vertices in \(B\) that \(\mathsf{retrace}\) does not map to themselves.

With this in mind, we reconstruct a function \(\widetilde{\lambda}^*\) on \([p]\) that is equivalent to \(\lambda^*\) (if it exists) up to the renaming of the vertices as follows. For every \(i\in[p]\):

• If \(i\in I_A\cap I_B\), then verify that \(\mathsf{sort}({\alpha_A}_{|J_A})(j)=\mathsf{retrace}(\mathsf{sort}({\alpha_B}|_{|J_B})(\ell))\), where \(j\) is the number of integers in \(I_A\) that are smaller or equal to \(i\), and \(\ell\) is the number of integers in \(I_B\) that are smaller or equal to \(i\). If this is not true, then return that there does not exist a \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible. Else (when this is true), then \(\widetilde{\lambda}^*(i)=\mathsf{sort}({\alpha_A}_{|J_A})(j)\).

• Else if \(i\in I_A\setminus I_B\), then \(\widetilde{\lambda}^*(i)=\mathsf{sort}({\alpha_A}_{|J_A})(j)\), where \(j\) is the number of integers in \(I_A\) that are smaller or equal to \(i\). If \(\alpha_A(j)\in M_A\), then return that there does not exist a \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible.

• Else (i.e., \(i\in I_B\setminus I_A\)), \(\widetilde{\lambda}^*(i)=\mathsf{retrace}(\mathsf{sort}({\alpha_B}_{|J_B})(j))\), where \(j\) is the number of integers in \(I_B\) that are smaller or equal to \(i\). If \(\mathsf{sort}({\alpha_B}_{|J_B})(j)\in M_B\), then return that there does not exist a \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible.

So far, observe that if the above tests have passed, then there indeed exists a \(p\)-labeling that is \((I_A,I_B,J_A,J_B,\lambda_A,\lambda_B)\)-compatible, and we denote it by \(\lambda^*\).

Now, we compute \((H,\alpha,\beta)\) as follows:

• \(V(H)=\widetilde{\lambda}^*([p])\).

• \(E(H)=\{\{u,v\}\in E(H_A): u,v\in V(H_A)\}\cup\{\{\mathsf{retrace}(u),\mathsf{retrace}(v)\}: \{u,v\}\in E(H_B)\}\). Since \((A,B)\) is a separation, two vertices are adjacent in \(G\) if and only if they are adjacent in at least one of \(G[A]\) and \(G[B]\). Hence, by the definition of \(\mathsf{sgn}\), two vertices are adjacent in \(G[\lambda^*([p])]\) if and only if the corresponding vertices are adjacent in at least one of \(H_A\) and \(H_B\). Thus, we derive that \(E(H)\) that we defined satisfies \(E(H)=E(G[\widetilde{\lambda}^*([p]])\) up to the remaining of the vertices.

• \(\alpha=\widetilde{\lambda}^*\).

• We construct a function \(\beta\) on \(V(H)\) as follows. For every \(v\in V(H)\):

  • If \(v\in M_A\): Verify that \(\beta_A(v)=\beta_B(\mathsf{retrace}^{-1}(v))\). If this is not true, then return that there does not exist a \(P\)-coloring that is \((\mu_A,\mu_B)\)-compatible. Else, \(\beta(v)=X\) where \(X\) is the element such that \(\beta_A(v)=(X,i)\) for some \(i\).

  • Else if \(v\in V(H_A)\setminus M_A\): \(\beta(v)=X\) where \(X\) is the element such that \(\beta_A(v)=(X,i)\) for some \(i\).

  • Else (when \(v\in V(H)\setminus V(H_A)\)): \(\beta(v)=X\) where \(X\) is the element such that \(\beta_B(v)=(X,i)\) for some \(i\).

  Observe that if the above tests have passed, then there indeed exists a \(P\)-coloring that is \((\mu_A,\mu_B)\)-compatible, and we denote it by \(\mu^*\).

Overall, we have \((H,\alpha,\beta)\) is isomorphic to \(\mathsf{sgn}_\emptyset(G,\lambda^*,\mu^*)\). Clearly, the time complexity to perform the computation above can be naively bounded by a polynomial in \(\lVert \mathsf{sgn}_S(G[A],\lambda_A,\mu_A) \rVert + \lVert \mathsf{sgn}_S(G[B],\lambda_B,\mu_B) \rVert\). This completes the proof of the basis.

Next, we suppose correctness for all sequences of pairs of natural numbers whose length is at most \(d-1\). Let \(\widehat{S}=((k_1,s_1),\ldots,(k_{d-1},s_{d-1}))\).

We initialize \(\cal C\) to be empty, and insert elements as follows. For all \(X\in \mathsf{sgn}_S(G,\lambda',\mu)\): Insert into \(\cal C\) the element returned by the application of the algorithm from the inductive hypothesis on \(X\) and \(f\). Correctness follows directly from the definition of \(\mathsf{sgn}\), and the running time bound is immediate from the definition of recursive size.

We initialize \(\cal C\) to be empty, and insert elements as follows. For all \(X\in \mathsf{sgn}_S(G,\lambda,\mu')\): Insert into \(\cal C\) the element returned by the application of the algorithm from the inductive hypothesis on \(X\) and \(f\). Correctness follows directly from the definition of \(\mathsf{sgn}\), and the running time bound is immediate from the definition of recursive size.

We initialize \({\cal C}\) to be empty, and insert elements as follows:

• For all \(X\in \mathsf{sgn}_S(G[A],\lambda_A,\mu_A)\) and \(Y\in \mathsf{sgn}_S(G[B],\lambda_B,\mu_B)\):

  • For all \(\widehat{I}_A,\widehat{I}_B\subseteq [k_d]\) such that \(\widehat{I}_A\cup \widehat{I}_B=[k_d]\) and \(|\widehat{I}_A|+ |\widehat{I}_B|-|\widehat{I}_A\cap \widehat{I}_B|=k_d\):

    • Denote \(I^*_A=I_A\cup \{p+i:i\in \widehat{I}_A\}\), \(I^*_B=I_B\cup \{p+i:i\in \widehat{I}_B\}\), \(J^*_A=J_A\cup\{|\mathsf{domain}(\lambda_A)|+i:i\in\widehat{I}_A\}\) and \(J^*_B=J_B\cup\{|\mathsf{domain}(\lambda_B)|+i:i\in\widehat{I}_B\}\).

    • Use the inductive hypothesis on \(\widehat{S},I^*_A, I^*_B,J^*_A,J^*_B,X,Y\) to compute \(Z\). If invalidity is determined, then continue to the next iteration (or stop, if all iterations have already been completed). Else, we have \(Z\) at hand, and insert it into \({\cal C}\).

If \(\cal C\) is empty, then this is the indication that \(\lambda^*\) or \(\mu^*\) (or both) does not exist; then, we return this information. Else, the proof proceeds as follows, showing that \({\cal C}=\mathsf{sgn}_S(G,\lambda^*,\mu^*)\).

First, we will argue that \({\cal C}\subseteq \mathsf{sgn}_S(G,\lambda^*,\mu^*)\). For this purpose, consider some iteration of the algorithm, corresponding to some \(\widehat{I}_A,\widehat{I}_B,X,Y\). Then, by the definition of \(\mathsf{sgn}\), \(X\) is equal to \(\mathsf{sgn}_{\widehat{S}}(G[A],\lambda_A\oplus \lambda'_A,\mu_A\otimes \mu'_A)\) for some (possibly several equivalent under isomorphism, but we pick one arbitrarily) \(\lambda'_A\in A_{G[A],k_d}\) and \(\mu'_A\in U_{G[A],\{0,1\}^{s_d}}\). (Notice that the knowledge of these \(\lambda'_A,\mu'_A\) is not available to the algorithm, but can only be used in the analysis.) Similarly, \(Y\) is equal to \(\mathsf{sgn}_{\widehat{S}}(G[B],\lambda_B\oplus \lambda'_B,\mu_B\otimes \mu'_B)\) for some \(\lambda'_B\in A_{G[B],k_d}\) and \(\mu'_B\in U_{G[B],\{0,1\}^{s_d}}\). Now, we define a function \(\widehat{\lambda}\in A_{G,k_d}\) as follows. For all \(i\in[k_d]\):

• If \(i\in \widehat{I}_A\): \(\widehat{\lambda}(i)=\lambda'_A(j)\).

• Otherwise (i.e., \(i\in \widehat{I}_B\setminus \widehat{I}_A\)): \(\widehat{\lambda}(i)=\lambda'_B(j)\).

Additionally, we define a function \(\widehat{\mu}\in U_{G,\{0,1\}^{s_d}}\) as follows. For all \(v\in V(G)\):

• If \(v\in A\): \(\widehat{\mu}(v)=\mu'_A(v)\).

• Otherwise (i.e., \(v\in B\setminus A\)): \(\widehat{\mu}(v)=\mu'_B(v)\).

The inductive hypothesis yields that \(Z=\mathsf{sgn}_{\widehat{S}}(G,\lambda^*\oplus \widehat{\lambda}, \mu^*\otimes \widehat{\mu})\). Since \(\widehat{\lambda}\in A_{G,k_d}\) and \(\widehat{\mu}\in U_{G,\{0,1\}^{s_d}}\), we conclude that \(Z\in \mathsf{sgn}_S(G,\lambda^*,\mu^*)\). This completes the proof that \({\cal C}\subseteq \mathsf{sgn}_S(G,\lambda^*,\mu^*)\).

Second, we will argue that \({\cal C}\supseteq \mathsf{sgn}_S(G,\lambda_D)\). For this purpose, consider some element in \(\mathsf{sgn}_S(G,\lambda^*,\mu^*)\). So, this element is of the form \(\mathsf{sgn}_{\widehat{S}}(G,\lambda^*\oplus\widehat{\lambda},\mu^*\otimes\widehat{\mu})\) for some (possibly several equivalent under isomorphism, but we pick one of each arbitrarily) \(\widehat{\lambda}\in A_{G,k_d}\) and \(\widehat{\mu}\in U_{G,\{0,1\}^{s_d}}\). Define:

• \(\widehat{I}_A=\{i-p+|\mathsf{domain}(\lambda_A)|:i\in\widehat{\lambda}^{-1}(A)\}\) and \(\widehat{I}_B=\{i-p+|\mathsf{domain}(\lambda_B)|:i\in\widehat{\lambda}^{-1}(B)\}\).

• \(\lambda'_A\in A_{G[A],k_d}\): For all \(i\in[k_d]\): If \(i\in\widehat{A}_I\), then \(\lambda'_A(i)=\widehat{\lambda}(i)\); Otherwise, let \(\lambda'_A(i)\) equal some arbitrary vertex in \(A\).

• \(\lambda'_B\in A_{G[B],k_d}\): For all \(i\in[k_d]\): If \(i\in\widehat{B}_I\), then \(\lambda'_B(i)=\widehat{\lambda}(i)\); Otherwise, let \(\lambda'_B(i)\) equal some arbitrary vertex in \(B\).

• \(\mu'_A=\mu^*_{|A}\) and \(\mu'_B=\mu^* \otimes_{|B}\). Then, \(\mu'_A\in U_{G[A,\{0,1\}^{s_d}}\) and \(\mu'_B\in U_{G[B],\{0,1\}^{s_d}}\).

Thus, the definition of \(\mathsf{sgn}\) directly yields that \(\mathsf{sgn}_{\widehat{S}}(G[A],\lambda_A\oplus\lambda'_A,\mu_A\otimes\mu'_A)\in\mathsf{sgn}_S(G[A],\lambda_A,\mu_A)\) and \(\mathsf{sgn}_{\widehat{S}}(G[B],\lambda_B\oplus\lambda'_B,\mu_B\otimes\mu'_B)\in\mathsf{sgn}_S(G[B],\lambda_B,\mu_B)\). Hence, the algorithm will perform an iteration with \(X=\mathsf{sgn}_{\widehat{S}}(G[A],\lambda_A\oplus\lambda'_A,\mu_A\otimes\mu'_A)\) and \(Y=\mathsf{sgn}_{\widehat{S}}(G[B],\lambda_B\oplus\lambda'_B,\mu_B\otimes\mu'_B)\), and an inner-iteration with \(\widehat{I}_A,\widehat{I}_B\). In particular, by the correctness of the inductive hypothesis, in this iteration we reconstruct \(Z=\mathsf{sgn}_{\widehat{S}}(G,\lambda^*\oplus \widehat{\lambda}, \mu^*\otimes \widehat{\mu})\). Thus, we conclude that \(\mathsf{sgn}_{\widehat{S}}(G,\lambda^*\oplus \widehat{\lambda}, \mu^*\otimes \widehat{\mu})\in{\cal C}\). This completes the proof of \({\cal C}\supseteq \mathsf{sgn}_S(G,\lambda^*,\mu^*)\).

Notice that we perform \(2^{O(k_d)}\cdot |\mathsf{sgn}_S(G[A],\lambda_A,\mu_A)|\cdot|\mathsf{sgn}_S(G[B],\lambda_B,\mu_B)|\) iterations (where \(|\mathsf{sgn}_S(G[A],\lambda_A,\mu_A)|\) and \(|\mathsf{sgn}_S(G[B],\lambda_B,\mu_B)|\) denote the sizes of the corresponding sets, not their recursive sizes). So, the bound on the time complexity of the algorithm follows from the inductive hypothesis and the definition of the recursive size of \(\mathsf{sgn}\). This completes the proof. ◻

Proof. Following the definition of signature, we compute it using brue-force as follows. For \(i=1,2,\ldots,d-1\): first, we consider all options to pick \(k_i\) vertices (with repetition) from \(V(G)\), thereby spending \(|V(G)|^{O(k_i)}\) time, and then consider all options to color all vertices using colors from \(\{0,1\}^{s_i}\), thereby spending \(2^{O(|V(G)|\cdot s_i)}\) time. The only difference is when \(i=d\). Then, again we consider all options to pick \(k_i\) vertices (with repetition) from \(V(G)\), thereby spending \(|V(G)|^{O(k_d)}\) time, and then, if \(\sum_{i=1}^dk_i<|V(G)|\), then since all vertices that were labeled are already known at this point (and unlabeled vertices do not appear in the signature), we can consider all colorings only of the labeled vertices rather than all vertices, thereby spending \(2^{O((\sum_{i=1}^dk_i)\cdot s_d)}\) time. Notice that by multiplying the entire formula by \(f(d)\), we can put the sum \(\sum_{i=1}^d\) before corresponding expressions rather than let it be in the exponents, e.g., \(2^{O((\sum_{i=1}^dk_i)\cdot s_d)}\leq g(d)\cdot \sum_{i=1}^d2^{O(s_d\cdot k_i)}\) for some computable function \(g\) of \(d\).

Notice that the order of \(\sum_{i=1}^d2^{O(k_i\log |V(G)|)}\cdot\sum_{i=1}^{d-1}2^{O(s_i\cdot |V(G)|)}\cdot\sum_{i=1}^d2^{O(s_d\cdot k_i)}\) is bounded by the dominant sum (since there is an \(O\)-notation in the exponent), and hence by \(\sum_{i=1}^d2^{O(k_i\log |V(G)|)}+\sum_{i=1}^{d-1}2^{O(s_i\cdot |V(G)|)}+ \sum_{i=1}^d2^{O(s_d\cdot k_i)}\); thus, the bound follows. ◻

Proof. Let \(<\) be an arbitrary order on \(V(G)\). For every \(x\in V(T)\), we will fix \(\mu_x:\beta(x)\rightarrow [|\beta(x)|]\) as the following bijective function: for all \(v\in\beta(x)\), \(\mu_x(v)\) equals the number of vertices smaller or equal to \(v\) among those in \(\beta(x)\) w.r.t. \(<\). Additionally, let \(\mu^*_x:\gamma(x)\rightarrow [|\beta(x)|]_0\) be the extension of \(\mu\) that assigns \(0\) to every vertex in \(\gamma(x)\setminus\beta(x)\). (We remind that \(\gamma(x)\) denotes the union of \(\beta(x')\) over every \(x'\) that is either \(x\) or a descendant of \(x\).) Let \(\mathsf{emp}=\{\cdots\{(-,-,-)\}\cdots\}\), where each pair \(\{,\}\) appears \(d=|S|\) times and \((-,-,-)\) is the empty graph with the empty labeling and the empty coloring.

Now, we describe the algorithm.

1. Initialize a dynamic programming table \(M\) with an entry \(M[x]\) for every \(x\in V(T)\). (The purpose of every entry \(M[x]\) will be to store \(\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)\).)

2. For every \(x\in V(T)\) in preorder, consider the following cases:

   1. \(x\) is a Leaf node: Assign \(M[x]=\mathsf{emp}\).

   2. \(x\) is an Introduce node: Let \(s\) be the child of \(x\). Let \(\{v\}=\beta(x)\setminus\beta(s)\). Let \(i_v\) be the number of vertices in \(\beta(x)\) that are smaller or equal to \(v\) w.r.t. \(<\). Compute \(X=\mathsf{sgn}_S(G[\beta(x)],-,\mu_x)\) using the algorithm from Lemma 12.

      Let \(f_X:[|\beta(x)|]_0\rightarrow [|\beta(x)|]_0\times [|\beta(s)|]_0\) be defined as follows. For all \(i\in [|\beta(x)|]_0\):

      • If \(i<i_v\), then \(f_X(i)=(i,i)\).

      • If \(i=i_v\), then \(f_X(i)=(i,0)\).

      • If \(i>i_v\), then \(f_X(i)=(i,i-1)\).

      Call the algorithm from item (ii) of Lemma 11 with \(X\) and \(f_X\), and let \(X'\) denote the result.

      Additionally, denote \(Y=M[s]\). Let \(f_Y:[|\beta(s)|]_0\rightarrow [|\beta(x)|]_0\times [|\beta(s)|]_0\) be defined as follows. For all \(i\in [|\beta(s)|]_0\):

      • If \(i<i_v\), then \(f_Y(i)=(i,i)\).

      • If \(i\geq i_v\), then \(f_Y(i)=(i+1,i)\).

      Call the algorithm from item (ii) of Lemma 11 with \(Y\) and \(f_Y\), and let \(Y'\) denote the result.

      Now, call the algorithm from item (iii) of Lemma 11 with \(I_A=I_B=J_A=J_B=\emptyset\), \(X'\) and \(Y'\), and let \(Z\) denote the result. Assign \(M[x]=Z\).

   3. \(x\) is a Forget node: Let \(s\) be the child of \(x\). Let \(\{v\}=\beta(s)\setminus\beta(x)\). Let \(i_v\) be the number of vertices in \(\beta(x)\) that are smaller or equal to \(v\) w.r.t. \(<\). Denote \(X=M[s]\).

      Let \(f_X:[|\beta(s)|]_0\rightarrow [|\beta(x)|]_0\) be defined as follows. For all \(i\in [|\beta(s)|]_0\):

      • If \(i<i_v\), then \(f_X(i)=i\).

      • If \(i=i_v\), then \(f_X(i)=0\).

      • If \(i>i_v\), then \(f_X(i)=i-1\).

      Call the algorithm from item (ii) of Lemma 11 with \(X\) and \(f_X\), and let \(X'\) denote the result. Assign \(M[x]=X'\).

   4. \(x\) is a Join node: Let \(h,s\) be the children of \(t\). Denote \(X=M[h]\) and \(Y=M[s]\). Let \(f:[|\beta(x)|]_0\rightarrow [|\beta(x)|]_0\times [|\beta(x)|]_0\) be defined as follows. For all \(i\in [|\beta(s)|]_0\): \((i)=(i,i)\).

      Call the algorithm from item (ii) of Lemma 11 with \(X\) and \(f\), and let \(X'\) denote the result. Additionally, call the algorithm from item (ii) of Lemma 11 with \(Y\) and \(f\), and let \(Y'\) denote the result.

      Now, call the algorithm from item (iii) of Lemma 11 with \(I_A=I_B=J_A=J_B=\emptyset\), \(X'\) and \(Y'\), and let \(Z\) denote the result. Assign \(M[x]=Z\).

3. Denote \(X=M[\mathsf{root}(T)]\). For every graph in the “innermost” sets of \(X\), every vertex is assigned a color that is a tuple that begins with \(0\) (since \(\mu^*_{\mathsf{root}(T)}\) is the function from \(V(G)\) to \(\{0\}\)). Remove these \(0\)’s. Let \(X'\) denote the result, and return \(X'\).

We use induction on the order of computation of \(M\) to show that for every \(x\in V(T)\), \(M[x]=\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)\). Recall that \(\gamma(\mathsf{root}(T))=V(G)\) and \(\beta(\mathsf{root}(T))=\emptyset\). Thus, since we remove the \(0\)’s assigned \(\mu^*_x\), proving the inductive claim will prove that the output of the algorithm is indeed \(\mathsf{sgn}_S(G)\).

In the basis, where \(x\) is a Leaf node and therefore \(\gamma(x)=\emptyset\), correctness follows directly from the definition of \(\mathsf{sgn}\).

Now, we prove correctness for some non-leaf \(x\in V(T)\), while we assume correctness for its child(ren). We have the following cases:

• \(x\) is an Introduce node: Consider the graph \((G[\gamma(x)],-,\mu^*_x)\) together with the separation \((\beta(x),\gamma(s))\). Note that \(\beta(x)\cap\gamma(s)=\{v\}\). From the inductive hypothesis, we have \(M[s]=\mathsf{sgn}_S(G[\gamma(s)],\lambda_s)\). Then, Lemma 11 directly implies that \(M[x]=\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)\). We remark that the application of this lemma is valid due to our definitions of \(f_X\) and \(f_Y\): particularly, we update the coloring corresponding to \(M[s]\) to be a restriction of \(\mu^*_x\) rather than \(\mu^*_s\), and we “append” \(\mu_s\), thereby enabling to pick \(\mu'=\mu_s\).

• \(x\) is a Forget node: From the inductive hypothesis, we have \(M[s]=\mathsf{sgn}_S(G[\gamma(s)],-,\mu^*_s)\). Thus, we only need to update the coloring from \(\mu^*_s\) to \(\mu_x\). This is done using \(f_X\) and the application Lemma 11, which directly implies that \(M[x]=\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)\).

• \(x\) is a Join node: Consider the graph \((G[\gamma(x)],\mu^*_x)\) together with the separation \((\gamma(h),\gamma(s))\). From the inductive hypothesis, we have that \(M[h]=\mathsf{sgn}_S(G[\gamma(h)],-,\mu^*_h)\) and \(M[s]=\mathsf{sgn}_S(G[\gamma(s)],-,\mu^*_s)\). Then, Lemma 11 directly implies that \(M[x]=\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)\). We remark that the application of this lemma is valid due to our definition of \(f\): particularly, we “append” \(\mu_x\), thereby enabling to pick \(\mu'=\mu_x\).

This completes the proof of the correctness of the algorithm.

For the time complexity analysis, we observe that for any node \(x\in V(T)\), each application of Lemma 11 is done in time \(2^{\sum_{i=0}^d k_i}\cdot (\sum_{i=1}^d(k_i+s_i))^{O(1)}\cdot(\sum_{s\in\mathsf{children}(x)}||\mathsf{sgn}_S(G[\gamma(s)],-,\mu^*_s)||)^{O(1)}\). In addition, if \(x\) is an Introduce node, we perform the additional computation of Lemma 12, whose time complexity is bounded by \(f(d)\cdot\left(\sum_{i=1}^d2^{O(k_i\cdot\log t)}+\sum_{i=1}^{d-1}2^{O(s_i\cdot t)}+ \sum_{i=1}^d2^{O(s_d\cdot k_i)}\right)\) for some computable function \(f\) of \(d\) (since it is applied on a graph with at most \(t+1\) vertices). Since \(||\mathsf{sgn}_S(G[\gamma(x)],-,\mu^*_x)||\leq \max_{\mu \in U_{G,[t+1]_0}} \lVert \mathsf{sgn}_S(G,-,\mu) \rVert\) for all nodes \(x \in V(T)\), the bound claimed in the lemma follows. ◻

Proof. To prove this lemma, we need to prove a more general claim: Let \(S=((k_1,s_1),\ldots,(k_d,s_d))\) be a sequence of pairs of natural numbers. Suppose that we are given the \(S\)-signature \(\mathsf{sgn}_S(G,\lambda,\mu)\) of a \(p\)-labeled \(\{0,1\}^q\)-colored graph \(G\). Now, let \(I=((a_1,b_1),\ldots,(a_r,b_r)), J=((\widetilde{a}_1,\widetilde{b}_1),\ldots,(\widetilde{a}_r,\widetilde{b}_r))\) be two other sequences of pairs of nonnegative integers so that \(\sum_{i=1}^r\widetilde{a}_i=p\) and \(\sum_{i=1}^r\widetilde{b}_i=q\), and for every \(i\in[r]\), \(a_i\leq\widetilde{a}_i\) and \(b_i\leq\widetilde{b}_i\).

Let \(\phi(v_1,\ldots,v_{p'},U_1,\ldots,U_{q'})\) be an \(S\)-formula with \(p'\) free vertex variables, \(v_1,\ldots,v_{p'}\), and \(q'\) free vertex set variables, \(U_1,\ldots,U_{q'}\), where \(\sum_{i=1}^ra_i=p'\) and \(\sum_{i=1}^rb_i=q'\). For all \(i\in[q]\), let \(A_i\) denote the set of vertices \(v\) in \(G\) such that the \(i\)-th coordinate of \(\mu(v)\) is \(1\). Now, we say that \((G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\) if \((G,V^*,U^*)\) satisfies \(\phi\), where:

• \(V^*=\lambda(1),\ldots,\lambda(a_1),\lambda(\widetilde{a}_1+1),\ldots,\lambda(\widetilde{a}_1+a_2),\cdots,\lambda(\sum_{i=1}^{r-1}\widetilde{a}_i+1),\ldots\lambda(\sum_{i=1}^{r-1}\widetilde{a}_i+a_r)\).

• \(U^*=A_1,\ldots,A_{b_1},A_{\widetilde{b}_1+1},\ldots,A_{\widetilde{b}_1+b_2},\cdots,A_{\sum_{i=1}^{r-1}\widetilde{b}_i+1},\ldots,A_{\sum_{i=1}^{r-1}\widetilde{b}_i+b_r}\).

Then, the claim is that we can check whether \((G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\) in \((||\mathsf{sgn}_S(G,\lambda,\mu)||+|\phi|)^{O(1)}\) time (given \(\mathsf{sgn}_S(G,\lambda,\mu)\)).

The proof is by induction on \(|S|=d\).

Denote \((H,\alpha,\beta)=\mathsf{sgn}_\emptyset(G,\lambda,\mu)\). By the definition of signature, \((H,\alpha,\beta)\) is the core of \((G,\lambda,\mu)\), which immediately yields that \((G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\) if and only if \((H,\alpha,\beta)\) satisfies \(\phi\) w.r.t. \(I,J\). So, we trivially check whether \((H,\alpha,\beta)\) satisfies \(\phi\) w.r.t. \(I,J\) in time \((||\mathsf{sgn}_S(G,\lambda,\mu)||+|\phi|)^{O(1)}\), and return the answer.

Here, we suppose correctness for all sequences of pairs of natural numbers whose length is at most \(d-1\). Denote \(S= (k_1,s_1)+\widehat{S}\), i.e., \(k=k_1\) and \(s=s_1\). Without loss of generality, we can suppose that \(\phi\) excludes occurrences of \(\forall\), since they can be replaced by occurrences of \(\exists\) and \(\neg\) (i.e., \(A (\forall x_1,\ldots\forall x_t\forall X_1,\ldots\forall X_s B\) is equivalent to \(A \neg(\exists x_1\ldots\exists x_t\exists X_1\ldots\exists X_s\neg B)\)). We will use induction on \(\ell\), being the number of occurrences of \(\neg,\wedge,\) and \(\vee\), in \(\phi\). But first, we consider the following case:

• \(\phi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'}) = \exists x_1 \cdots \exists x_i\exists Y_1 \cdots \exists Y_j \psi(v_1,\dots,v_{p'},x_1,\dots,x_i,U_1,\ldots,U_{q'},Y_1,\ldots,Y_j)\), where \(\psi\) is an \(\widehat{S}\)-formula with \(p'+i\) free vertex variables for some \(i\in[k]_0\) and \(q'+j\) free vertex set variables for some \(j\in[s]_0\) (and \(i+j\geq 1\)). Our algorithm works as follows. For every element \(X\in\mathsf{sgn}_S(G,\lambda,\mu)\), we use the algorithm guaranteed by the inductive hypothesis (w.r.t. \(d\)) on \(X\), \(\psi\), \(I'\) being \(I\) to which we append the pair \((i,j)\), and \(J'\) being \(J\) to which we append the pair \((k,s)\) and return its answer. The definition of the recursive size of a signature directly yields the required time bound.

  For the forward direction of correctness, suppose that \((G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\). So, there exist functions \(\lambda'\in A_{G,k}\) and \(\mu'\in U_{G,\{0,1\}^s}\) such that \((G,\lambda\oplus\lambda',\mu\otimes\mu')\) satisfies \(\psi\) w.r.t. \(I'\). Notice that \(\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\lambda',\mu\otimes\mu')\in\mathsf{sgn}_S(G,\lambda,\mu)\). So, there exists an iteration where the algorithm considers \(X=\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\lambda',\mu\otimes\mu')\). By the inductive hypothesis, the algorithm then returns yes.

  For the reverse direction of correctness, suppose that the algorithm returned yes. Let \(X\in\mathsf{sgn}_S(G,\lambda,\mu)\) correspond to the iteration where the algorithm returned yes. Then, \(X=\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\lambda',\mu\otimes\mu')\) for some \(\lambda'\in A_{G,k}\) and \(\mu'\in U_{G,\{0,1\}^s}\). By the inductive hypothesis, \((G,\lambda\oplus\lambda',\mu\otimes\mu')\) satisfies \(\psi\) w.r.t. \(I',J'\). Thus, by assigning \(x_1=\lambda'(1),\ldots,x_i=\lambda'(i)\) and \(Y_{j'}\), for all \(j'\in[j]\), to be the set of vertices such that the \(j'\)-th coordinate assigned to them by \(\mu'\) is \(1\), we see that \((G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\).

Now, we continue with the induction on \(\ell\). Since \(d\geq 1\), the base case where \(\ell=0\) is already covered by the above (since, when \(d\geq1\) and \(\ell=0\), the formula must begin with \(\exists\)).

Next, suppose \(\ell\geq 1\), and assume correctness when we have at most \(\ell-1\) occurrences of \(\neg,\wedge,\) and \(\vee\) (but the same number of free variables).

According to the definition of \(S\)-formulas and since \(\varphi\) excludes occurrences of \(\forall\), it remains to consider the following cases:

• \(\phi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'}) = \neg \psi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})\), where \(\psi\) is an \(S\)-formula with \(p'\) free vertex variables and \(q'\) free vertex set variables. Our algorithm simply calls the algorithm guaranteed by the inductive hypothesis (w.r.t. \(\ell\)) on \(\mathsf{sgn}_S(G,\lambda,\mu),\psi,I,J\), and returns the opposite answer. Correctness and time complexity requirements are immediate.

• Either \(\phi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})=\psi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'}) \wedge \varphi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})\) or \(\phi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})=\psi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'}) \vee \varphi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})\), where \(\psi\) and \(\varphi\) are both \(S\)-formulas with \(p'\) free vertex variables and \(q'\) free vertex set variables.

  Let us consider only the case where \(\phi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})=\psi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'}) \wedge \varphi(v_1,\dots,v_{p'},U_1,\ldots,U_{q'})\), since the proof for the other case is similar. Our algorithm simply calls the algorithm guaranteed by the inductive hypothesis (w.r.t. \(\ell\)) twice: one time w.r.t. \(\mathsf{sgn}_S(G,\lambda,\mu),\psi,I\), and another time w.r.t. \(\mathsf{sgn}_S(G,\lambda,\mu),\varphi,I,J\); the algorithm returns yes if and only if both calls returned yes. Again, correctness and time complexity requirements are immediate.

This completes the proof. ◻

Proof. The “if” direction directly follows from Lemma 13. Thus, it suffices to show the “only if” direction. Towards the proof of this direction, we reuse the definition of a \(p\)-labeled \(\{0,1\}^q\)-colored graph \((G,\lambda,\mu)\) satisfying \(\phi\) w.r.t. \(I,J\) from the proof of Lemma 13. Now, we say that two \(p\)-labeled \(\{0,1\}^q\)-colored graphs \((G,\lambda,\mu)\) and \((G',\lambda',\mu')\) are \(S\)-equivalent iff for every \(S\)-MSO \(\phi\) with \(p'\leq p\) free vertex variables and \(q'\leq q\) set variables, and every compatible \(I,J\), (\(G,\lambda,\mu)\) satisfies \(\phi\) w.r.t. \(I,J\) iff \((G',\lambda',\mu')\) does. Here, compatibility naturally means that \(I=((a_1,b_1),\ldots,(a_r,b_r)), J=((\widetilde{a}_1,\widetilde{b}_1),\ldots,(\widetilde{a}_r,\widetilde{b}_r))\) are two sequences of pairs of nonnegative integers, for some \(r\), so that \(\sum_{i=1}^r\widetilde{a}_i=p, \sum_{i=1}^ra_i=p'\), \(\sum_{i=1}^r\widetilde{b}_i=q\), \(\sum_{i=1}^rb_i=q'\), and for every \(i\in[r]\), \(a_i\leq\widetilde{a}_i\) and \(b_i\leq\widetilde{b}_i\). However, in what follows, we will only be use the supposition when \(I=J,p'=p\) and \(q'=q\), and then we do not need to mention \(I,J\) explicitly.

So, we aim to prove the more general claim: if \((G,\lambda,\mu)\) and \((G',\lambda',\mu')\) are \(S\)-equivalent, then then have the same \(S\)-signatures. Next, suppose that \((G,\lambda,\mu)\) and \((G',\lambda',\mu')\) are \(S\)-equivalent.

The proof is by induction on \(|S|=d\). For all \(i\in[q]\), let \(A_i\) denote the set of vertices \(v\) in \(G\) such that the \(i\)-th coordinate of \(\mu(v)\) is \(1\).

Denote \((H,\alpha,\beta)=\mathsf{sgn}_\emptyset(G,\lambda,\mu)\) and \((H',\alpha',\beta')=\mathsf{sgn}_\emptyset(G',\lambda',\mu')\).

Consider the following \(\emptyset\)-formula: \[\begin{array}{ll} \bigskip \phi(v_1,\dots,v_{p},U_1,\ldots,U_{q}) &= \left(\bigwedge_{(i,j): (\alpha(i),\alpha(j))\in E(H)} \mathbf{adj}(v_i,v_j)\right) \wedge \left(\bigwedge_{(i,j): (\alpha(i),\alpha(j))\notin E(H)} \neg\mathbf{adj}(v_i,v_j)\right)\\ \bigskip & \wedge\left(\bigwedge_{(i,j): \alpha(i)\neq\alpha(j)} v_i=v_j\right) \wedge \left(\bigwedge_{(i,j): \alpha(i)\neq\alpha(j)} v_i\neq v_j\right)\\ & \wedge \left(\bigwedge_{i,j: \alpha(i)\in A_j}v_i\in U_j\right)\wedge \left(\bigwedge_{i,j: \alpha(i)\notin A_j}v_i\notin U_j\right). \end{array}\]

In particular, the formula is defined so that \((H,\alpha,\beta)\) satisfies it, and any \(p\)-labeled \(\{0,1\}^q\)-colored graph that satisfies it must be isomorphic to \((H,\alpha)\). Now, by the definition of \(\mathsf{sgn}\), specifically the derivation of \((H,\alpha,\beta)\) from \((G,\lambda,\mu)\), it is immediate that \((G,\lambda,\mu)\) satisfies \(\phi\) as well. So, since \((G,\lambda,\mu)\) and \((G',\lambda',\mu')\) are \(\emptyset\)-equivalent, it follows that \((G',\lambda')\) satisfies \(\phi\). Then, again by the definition of \(\mathsf{sgn}\), it is immediate that \((H',\alpha',\beta')\) satisfies \(\phi\) as well. Hence, \((H',\alpha',\beta')\) is isomorphic to \((H,\alpha,\beta)\), that is, \(\mathsf{sgn}_\emptyset(G,\lambda,\mu) = \mathsf{sgn}_\emptyset(G',\lambda',\mu')\).

Here, we suppose correctness for all sequences of natural numbers whose length is at most \(r-1\). Denote \(S= (k,s)+\widehat{S}\).

We will only show the containment \(\mathsf{sgn}_S(G,\lambda,\mu)\subseteq \mathsf{sgn}_S(G',\lambda',\mu')\), since the proof of the other containment \(\mathsf{sgn}_S(G',\lambda',\mu')\subseteq \mathsf{sgn}_S(G,\lambda,\mu)\) is symmetric. For this purpose, consider some arbitrary \(X\in \mathsf{sgn}_S(G,\lambda,\mu)\). Thus, \(X=\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\) for some \(\widehat{\lambda}\in A_{G,k}\) and \(\widehat{\mu}\in U_{G,\{0,1\}^s}\). We define an \(S\)-formula \(\phi(v_1,\ldots,v_p,U_1,\ldots,U_q)\) as follows:

\[\phi(v_1,\ldots,v_p,U_1,\ldots,U_q)=\exists x_1\cdots\exists x_k\exists Y_1\cdots\exists Y_s \psi(v_1,\ldots,v_p,x_1,\ldots,x_k,U_1,\ldots,U_q,Y_1,\ldots,Y_s),\]

where \(\psi(v_1,\ldots,v_p,x_1,\ldots,x_k,U_1,\ldots,U_q,Y_1,\ldots,Y_s)\) is the \(\widehat{S}\)-formula defined as follows: \[\begin{array}{l} \medskip \psi(v_1,\ldots,v_p,x_1,\ldots,x_k,U_1,\ldots,U_q,Y_1,\ldots,Y_s)=\\ \medskip\left(\bigwedge_{\varphi\in UNSAT}\neg\varphi(v_1,\ldots,v_p,x_1,\ldots,x_k,U_1,\ldots,U_q,Y_1,\ldots,Y_s)\right)\wedge\\ \left(\bigwedge_{\varphi\in SAT}\varphi(v_1,\ldots,v_p,x_1,\ldots,x_k,U_1,\ldots,U_q,Y_1,\ldots,Y_s)\right), \end{array}\]

where \(UNSAT\) is the collection of all \(\widehat{S}\)-formulas with \(p+k\) free vertex variables and \(q+s\) vertex set variables that are not satisfied by \((G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\), and \(SAT\) is the collection of all such formulas that are satisfied by \((G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\).

Observe that, by the definition of \(\psi\), \((G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\) satisfies it. So, by assigning \(x_1=\widehat{\lambda}(1),x_2=\widehat{\lambda}(2),\ldots,x_k=\widehat{\lambda}(k)\), and \(Y_i\), for all \(i\in[s]\) be the set of vertices whose \(i\)-th coordinate in \(\widehat{\mu}\) is \(1\), we see that \((G,\lambda,\mu)\) satisfies \(\phi\). So, since \((G,\lambda,\mu)\) and \((G',\lambda',\mu')\) are \(S\)-equivalent, we get that \((G',\lambda',\mu')\) satisfies \(\phi\) as well. Thus, let \(w\) be an assignment of vertices and vertex sets of \(G'\) to the variables \(x_1,\ldots,x_k,Y_1,\ldots,Y_s\) that witnesses this. Accordingly, define \(\widehat{\lambda}': [k]\rightarrow V(G')\) so that for all \(i\in[k]\), \(\widehat{\lambda}'(i)=w(x_{i})\). Additionally, define \(\widehat{\mu}': V(G')\rightarrow \{0,1\}^s\) so that for all \(v\in V(G')\) and \(i\in[s]\), the \(i\)-th coordinate of \(\widehat{\mu}'(v)\) is \(1\) iff \(v\in w(Y_i)\). By the definition of \(\widehat{\lambda}'\) and \(\widehat{\mu}'\), it immediately follows that \((G',\lambda'\oplus\widehat{\lambda}',\mu'\otimes\widehat{\mu}')\) satisfies \(\psi\). However, by the definition of \(\psi\), this implies that \((G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\) and \((G',\lambda'\oplus\widehat{\lambda}',\mu'\otimes\widehat{\mu}')\) are \(\widehat{S}\)-equivalent. In turn, by the inductive hypothesis, which can be applied since \(|\widehat{S}|\leq d-1\), we derive that \(\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})=\mathsf{sgn}_{\widehat{S}}(G',\lambda'\oplus\widehat{\lambda}',\mu'\otimes\widehat{\mu}')\) (under isomorphism). By the definition of \(\mathsf{sgn}_S(G',\lambda',\mu')\), it includes \(\mathsf{sgn}_{\widehat{S}}(G',\lambda'\oplus\widehat{\lambda}',\mu'\otimes\widehat{\mu}')\), and therefore it includes \(\mathsf{sgn}_{\widehat{S}}(G,\lambda\oplus\widehat{\lambda},\mu\otimes\widehat{\mu})\). Since the choice of \(X\) was arbitrary, we conclude that \(\mathsf{sgn}_S(G,\lambda,\mu)\subseteq \mathsf{sgn}_S(G',\lambda',\mu')\). ◻

Proof sketch. To avoid copy-past of text, we will only describe the changes in the proof of Lemma 11. Again, we prove item (iii*) instead of (iii), where, now, the basic \((p',q',w)\)-evaluation maps of \((G[A],\lambda_A,\mu_A)\) and \((G[B],\lambda_B,\mu_B)\) are given, and we are to compute the simple \((p',q',w)\)-evaluation map of \((G,\lambda^*,\mu^*)\).

In the basis, to obtain \(g(H,\alpha,\beta)\), we compute \(g(H_A,\alpha_A,\beta_A)\cdot g(H_B,\alpha_B,\beta_B)\) and divide it by the multiplication of all of the following terms:

• For all \(i\in J_A\cap J_B\), \(w(\alpha_A(i))\) (since each of them is double-counted).

• For all \(i\in [p]\setminus J_A\), \(w(\alpha_A(i))\) (since each of them is irrelevant).

• For all \(i\in[p]\setminus J_B\), \(w(\alpha_B(i))\) (since each of them is irrelevant).

For the inductive step, where \(|S|\geq 1\), the only difference is that we use the inductive hypothesis of this lemma rather than of Lemma 11, and thereby obtain the simple evaluation map. Notice that the same signature \(Z\) might be computed multiple times, but in all of them, \(g(Z)\) is the same, and hence there is no conflict. ◻

Proof sketch. To avoid copy-past of text, we will only describe the changes in the proof of Lemma 11. Here, we do not use induction. In particular, we directly move to the arguments given in the step, where \(|S|\geq 1\). Then, to compute \(Z\), we apply the algorithm from Lemma 15 in order to obtain \(g(Z)\). Besides this, the critical difference is that when we insert \(Z\) into \(\cal C\), if it already exists, then we add \(g(Z)\) to the existing \(f(Z)\), and else we just assign \(f(Z)=g(Z)\). ◻

Proof sketch. To avoid copy-past of text, we will only describe the changes in the proof of Theorem 5. Now, the purpose of each table entry \(M[x]\), \(x\in V(T)\), will be to store the \((S,w)\)-evaluation map of \((G[\gamma(x)],-,\mu^*_x)\) rather than just its signature.

First, in case \(x\) is a leaf node, we assign the weight \(0\).

Second, in case \(x\) is an Introduce node, the first change is to apply a generalized version of Lemma 12, to compute the \((S,w)\)-evaluation map of \(X\) rather than just \(X\): the brute-force computation in the proof can be trivially modified to account for weights. Then, instead of applying item (iii) of Lemma 11, we apply Lemma 16, and store the result in \(M[x]\).

In case \(x\) is a Forget node, the proof remains the same (keeping the same evaluation map).

Lastly, in case \(x\) is a Join node, the only difference is that instead of applying item (iii) of Lemma 11, we apply Lemma 16, and store the result in \(M[x]\). ◻

Proof sketch. Let \(S=(k,s)+S'\). Recall that by definition, for an assignment \(\alpha = (v_1,\dots,v_k,V_1,\dots,V_s)\), we write \(w(\alpha) = (\prod_{i=1}^k w(v_1)) \cdot (\prod_{i=1}^s \prod_{v \in V_i} w(v))\), and that \(\mathsf{scr}(G,w,\phi) = \sum_{\alpha \in \mathcal{A}_\phi(G)} w(\alpha)\), where \(\mathcal{A}_\phi(G)\) denotes the set of all satisfying assignments of \(\phi\) on \(G\).

Also recall that for every \(x\in\mathsf{sgn}_S(G)\), \(f(x) = \displaystyle{\sum_{(\lambda,\mu) \in \varGamma_x} \left(\prod_{i=1}^k w(\lambda(i)) \cdot \prod_{i=1}^s \prod_{v \in V(G)} (w(v))^{\mu_i(v)}\right)}\), where \(\varGamma_x\) be the set consisting of all pairs \((\lambda,\mu) \in \varLambda_{G,k} \times U_{G,\{0,1\}^s}\) satisfying \(\mathsf{sgn}_{S'}(G, \lambda,\mu) = x\).

Now, notice that the proof of Lemma 13 implies that, in time \((||\mathsf{sgn}_S(G)||+|\phi|)^{O(1)}\), we can obtain all the answers for the following for all \(x\in\mathsf{sgn}_S(G)\): Does there exist \((\lambda,\mu) \in \varGamma_x\) so that \((G,\lambda,\mu)\) satisfies \(\phi\)? Furthermore, the proof shows that if there exists such \((\lambda,\mu) \in \varGamma_x\), then, in fact, all \((\lambda',\mu') \in \varGamma_x\) are such that \((G,\lambda',\mu')\) satisfies \(\phi\). Let \(X_{\mathsf{yes}}\) denote the set of \(x\in\mathsf{sgn}_S(G)\) such that the above answer is positive.

For all \(x\in X_{\mathsf{yes}}\), let \(M_x\) denote the set of all assignments \(\alpha = (v_1,\dots,v_k,V_1,\dots,V_s)\in \mathcal{A}_\phi(G)\) such that for all \(i\in[k]\), \(v_i=\lambda(i)\), and for all \(i\in[s]\), \(V_i\) is the set of all vertices whose \(i\)-coordinate in \(\mu\) is \(1\), for some \((\lambda,\mu) \in \varGamma_x\). Then, by the definitions of the weight of an assignment and of \(f\), we get that \(f(x)=\sum_{\alpha\in M_x}w(\alpha)\). Notice that for distinct \(x,y\in X_{\mathsf{yes}}\), \(M_x\cap M_y=\emptyset\), and that \(\bigcup_{x\in X_{\mathsf{yes}}}M_x=\mathcal{A}_\phi(G)\).

Thus, algorithmically, we derive that it suffices to compute \(f(G)\) (using Theorem 6) and then \(X_{\mathsf{yes}}\) by iterating through every signature in \(\mathsf{sign}_S(G)\) and using the arguments for Lemma 13, eventually returning \(\sum_{x\in X_{\mathsf{yes}}}f(x)\) as \(\mathsf{scr}(G,w,\phi)\). Due to the running times stated in Theorem 6 and (the proof of) Lemma 13, the proof is complete. ◻

Proof. Recall that how we constructed \(\varGamma_S(G,\lambda,\mu)\). Let \(V_0,V_1,\dots,V_{6p}\), \(\pi_1,\dots,\pi_{6p}\), \(\mu_1,\dots,\mu_{6p}\), \(X_1,\dots,X_{6p}\), \(\gamma_1,\dots,\gamma_{6p}\), and \(\lambda_1,\dots,\lambda_{6p}\) be as in the construction of \(\varGamma_S(G,\lambda,\mu)\). For \(i \in [6p]\), denote by \(\hat{\pi}_i:V(G) \rightarrow [4t]_0\) the function where \(\hat{\pi}_i(v) = \pi_i^{-1}(v)\) for all \(v \in V_0 \cap V_i\) and \(\pi_i'(v) = 0\) otherwise. Also, write \(G_i = G[V_0 \cup (\bigcup_{j=1}^i V_j)]\) for \(i \in [6p]\).

We show how to compute \(\mathsf{sgn}_S(G,\lambda,\mu)\) if we are only given \(\varGamma_S(G,\lambda,\mu)\). Specifically, we are going to prove that, for all \(i \in [6p]_0\), \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_{i+1})_{|V(G_i)})\) can be computed using \(\varGamma_S(G,\lambda,\mu)\). We apply induction on \(i\). Consider the base case \(i = 0\). As \(G_0 = G[V_0]\), what we want to compute is \(\mathsf{sgn}_S(G[V_0],\lambda^{|V_0},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_1)_{|V_0})\). By construction, the first element of \(\varGamma_S(G,\lambda,\mu)\) is \((G[V_0],\lambda^{|V_0} \oplus \pi_1 \oplus \cdots \oplus \pi_{6p},\mu_{|V_0})\), from which we can obtain the functions \(\mu_{|V_0},\pi_1,\dots,\pi_{6p}\). Knowing \(\mu_{|V_0},\pi_1,\dots,\pi_{6p}\), we can further compute the function \((\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_1)_{|V_0}\). Therefore, from the first element of \(\varGamma_S(G,\lambda,\mu)\), we can obtain the graph \((G[V_0],\lambda^{|V_0},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_1)_{|V_0})\) itself and thus its \(S\)-signature. Now suppose we have \(\mathsf{sgn}_S(G_{i-1},\lambda^{|V(G_{i-1})},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_i)_{|V(G_{i-1})})\), and we show how to use it to compute \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_{i+1})_{|V(G_i)})\).

For convenience, write \(\tau = \mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_{i+1}\). Then what we want to compute is just \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},\tau_{|V(G_i)})\). We can obtain \(V_0 \cap V_1,\dots,V_0 \cap V_{6p}\) from \(\varGamma_S(G,\lambda,\mu)\), as they are just \(\text{Im}(\pi_1),\dots,\text{Im}(\pi_{6p})\). For each \(j \in [i]\), construct a function \(f_j: [4t]_0 \rightarrow [4t]_0\) as \[f_j(a) = \left\{ \begin{array}{ll} \pi_j^{-1}(\pi_i(a)) & \text{if } a \neq 0 \text{ and } \pi_i(a) \in V_0 \cap V_j, \\ 0 & \text{otherwise}. \end{array} \right.\] Then define \(f: P \times [4t]_0 \rightarrow P \times [4t]_0^{i}\) as \(f(a,x) = (a,f_1(x),\dots,f_i(x))\). Now it is easy to verify that \((\tau \otimes \hat{\pi}_i)_{|V_i} = f \circ \mu_i\). Thus, by (ii) of Lemma 11, we can compute \(\mathsf{sgn}_S(G[V_i],\lambda_i,(\tau \otimes \hat{\pi}_i)_{|V_i})\) using only \(f\) and \(\mathsf{sgn}_S(G[V_i],\lambda_i,\mu_i)\). Next, we show how to further compute \(\mathsf{sgn}_S(G[V_i],\mathsf{sort}(\lambda^{|V_i}),(\tau \otimes \hat{\pi}_i)_{|V_i})\). It suffices to construct a function \(f\) (from what we know) satisfying that \(\mathsf{sort}(\lambda^{|V_i}) = \lambda_i \circ f\), and then applies (i) of Lemma 11. The domain of \(\lambda^{|V_i}\) is \(\lambda^{-1}(V_i) = \lambda^{-1}(V_0 \cap V_i) \subseteq [p]\), which can be known from \(\varGamma_S(G,\lambda,\mu)\) as it just consists of the numbers \(a \in [p]\) such that \(\lambda(a) \in V_0 \cap V_i\). Thus, we can construct the bijection \(f': [|\lambda^{-1}(V_i)|] \rightarrow \lambda^{-1}(V_i)\) such that \(\mathsf{sort}(\lambda^{|V_i}) = \lambda^{|V_i} \circ f'\). Recall that the domain of \(\gamma_i\) is \(\pi_i^{-1}(X_i)\) and \(\lambda_i = \mathsf{sort}(\gamma_i)\). Note that \(X_i\) can be known from \(\varGamma_S(G,\lambda,\mu)\), since it is just \(\text{Im}(\lambda^{|V_0}) \cap (V_0 \cap V_i)\). Thus, we can construct the bijection \(f'': [|X_i|] \rightarrow \pi_i^{-1}(X_i)\) such that \(\gamma_i = \mathsf{sort}(\gamma_i) \circ f'' = \lambda_i \circ f''\). Furthermore, it is easy to verify that \(\lambda^{|V_i} = \gamma_i \circ (\hat{\pi}_i \circ \lambda^{|V_0})^{| \pi_i^{-1}(X_i)}\), and \((\hat{\pi}_i \circ \lambda^{|V_0})^{| \pi_i^{-1}(X_i)}\) can also be known from \(\varGamma_S(G,\lambda,\mu)\) simply because \(\hat{\pi}_i \circ \lambda^{|V_0} =(\hat{\pi}_i)_{|V_0} \circ \lambda^{|V_0}\). Setting \(f = f'' \circ (\hat{\pi}_i \circ \lambda^{|V_0})^{| \pi_i^{-1}(X_i)} \circ f'\), we have \(\mathsf{sort}(\lambda^{|V_i}) = \lambda_i \circ f\). Applying (i) of Lemma 11, we can then compute \(\mathsf{sgn}_S(G[V_i],\mathsf{sort}(\lambda^{|V_i}),(\tau \otimes \hat{\pi}_i)_{|V_i})\) using only \(f\) and \(\mathsf{sgn}_S(G[V_i],\lambda_i,(\tau \otimes \hat{\pi}_i)_{|V_i})\). Finally, using \(\mathsf{sgn}_S(G[V_i],\lambda_i,(\tau \otimes \hat{\pi}_i)_{|V_i})\), we compute \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},\tau_{|V(G_i)})\) as follows. By our induction hypothesis, we already have \(\mathsf{sgn}_S(G_{i-1},\lambda^{|V(G_{i-1})},(\tau \otimes \hat{\pi}_i)_{|V(G_{i-1})})\) in hand. For convenience, let us write \(A = V(G_{i-1}) = V_0 \cup (\bigcup_{j=1}^{i-1} V_j)\) and \(B = V_i\). Then \((A,B)\) is a separation of \(G_i\) by (iii) of Lemma 5. Observe that \((\lambda^{|V(G_i)})^{-1}(A) = [p]\) and \((\lambda^{|V(G_i)})^{-1}(B) = \lambda^{-1}(V_0 \cap V_i)\). Furthermore, \(\mathsf{sort}((\lambda^{|V(G_i)})^{|A}) = \lambda^{|V(G_{i-1})}\) and \(\mathsf{sort}((\lambda^{|V(G_i)})^{|B}) = \mathsf{sort}(\lambda^{|V_i})\). Therefore, by (iii) of Lemma 11, given \([p]\), \(\lambda^{-1}(V_0 \cap V_i)\), \(\mathsf{sgn}_S(G_{i-1},\lambda^{|V(G_{i-1})},(\tau \otimes \hat{\pi}_i)_{|V(G_{i-1})})\) and \(\mathsf{sgn}_S(G[V_i],\mathsf{sort}(\lambda^{|V_i}),(\tau \otimes \hat{\pi}_i)_{|V_i})\), we can compute \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},\tau_{|V(G_i)})\). This completes our induction argument.

Now we see \(\mathsf{sgn}_S(G_i,\lambda^{|V(G_i)},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_{i+1})_{|V(G_i)})\) can be computed using only \(\varGamma_S(G,\lambda,\mu)\), for all \(i \in [6p]\). Note that \((G,\lambda,\mu) = (G_i,\lambda^{|V(G_i)},(\mu \otimes \hat{\pi}_{6p} \otimes \hat{\pi}_{6p-1} \otimes \cdots \otimes \hat{\pi}_{i+1})_{|V(G_i)})\) for \(i = 6p\). Thus, we can compute \(\mathsf{sgn}_S(G,\lambda,\mu)\) given only \(\varGamma_S(G,\lambda,\mu)\). ◻

Proof. Define a set \(K = \{\mathsf{sgn}_{S'}(G',\lambda',\mu'): (G',\lambda',\mu') \in \mathcal{G}_{p+k,P\times \{0,1\}^s,t}\}\). By construction, we have \(\mathsf{sgn}_S(G,\lambda,\mu) \subseteq K\) for all \((G,\lambda,\mu) \in \mathcal{G}_{p,P,t}\). Thus, \(\{\mathsf{sgn}_S(G,\lambda,\mu): (G,\lambda,\mu) \in \mathcal{G}_{p,P,t}\} \subseteq 2^K\). It then follows that \(\delta_S(\mathcal{G}_{p,P,t}) \leq |K|\) and \(\Delta_S(\mathcal{G}_{p,P,t}) \leq |\{\mathsf{sgn}_S(G,\lambda,\mu): (G,\lambda,\mu) \in \mathcal{G}_{p,P,t}\}| \leq 2^{|K|}\). So it suffices to bound \(|K|\). By Lemma 18, \(|K|\) is bounded by the number of different \(S'\)-characterization sequences the graphs in \(\mathcal{G}_{p+k,P\times \{0,1\}^s,t}\) have.

In the \(S'\)-characterization sequence of a graph in \(\mathcal{G}_{p+k,P\times \{0,1\}^s,t}\), the first element is a \(((p+k)+24(p+k)t)\)-labeled and \((P\times \{0,1\}^s)\)-colored graph, which has \(O((p+k)t)\) vertices and treewidth at most \(t\). By Fact 6, the number of such graphs is bounded by \(((p+k)t)^{O((p+k)t^2)} \cdot (2^s|P|)^{O((p+k)t)}\). Fixing such a graph \((H,\sigma,\tau) \in \mathcal{G}_{(p+k)+24(p+k)t,P\times \{0,1\}^s,t}\), we count the number of different \(S'\)-characterization sequences starting with \((H,\sigma,\tau)\) the graphs in \(\mathcal{G}_{p+k,P\times \{0,1\}^s,t}\) have. Consider an \(S'\)-characterization sequence whose first element is \((H,\eta,\tau)\). Denote by \(e_1,\dots,e_{6(p+k)}\) be the remaining elements in the sequence. By construction, each of \(e_i\) is the \(S'\)-signature of some \(q_i\)-labeled and \(P'\)-colored graph \((H_i,\eta_i,\tau_i)\) where \(q_i \leq \min\{p+k,4t\} = p'\). As observed before, both \(q_i\) and \(\mathsf{core}(H_i,\eta_i,\tau_i)\) are determined by \((H,\eta,\tau)\); we use \(\sigma_i\) to denote this core. Therefore, the number of possible choices for \(e_i\) is bounded by \[|\{\mathsf{sgn}_{S'}(H',\eta',\tau'): (H',\eta',\tau') \in \mathcal{G}_{q_i,P',t} \text{ and } \mathsf{core}(H',\eta',\tau') = \sigma_i\}| \leq \Delta_{S'}(\mathcal{G}_{q_i,P',t}) \leq \Delta_{S'}(\mathcal{G}_{p',P',t}).\] So the total number of choices for \(e_1,\dots,e_{6(p+k)}\) is at most \((\Delta_{S'}(\mathcal{G}_{p',P',t}))^{6(p+k)}\). It follows that \[|K| \leq ((p+k)t)^{O((p+k)t^2)} \cdot (2^s|P|)^{O((p+k)t)} \cdot (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{6(p+k)}.\] As such, the bounds for \(\delta_S(\mathcal{G}_{p,P,t})\) and \(\Delta_S(\mathcal{G}_{p,P,t})\) follows. ◻

Proof. We modify the bounds in Lemma 19 as follows. Observe that \[\begin{align} & ((p+k)t)^{O((p+k)t^2)} \cdot (2^s|P|)^{O((p+k)t)} \cdot (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{6(p+k)} \\ =\;& ((p+k)t)^{O((p+k)t^2)} + (2^s|P|)^{O((p+k)t)} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ =\;& 2^{O((p+k)t^3 \log (p+k))} + 2^{O((s+\log |P|) \cdot (p+k)t)} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ =\;& 2^{O((p+k)t^3 \log (p+k))} + 2^{2^{O(s + \log |P|)}} + 2^{O((p+k)t^2 \log(p+k))} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)}, \end{align}\] where the last \(=\) follows from the fact \((s+\log |P|) \cdot (p+k)t \leq \max\{2^{s+\log|P|},(p+k)t^2 \log(p+k)\}\). Fact 10 implies \(2^{O((p+k)t^3 \log (p+k))} = 2^{\hat{O}(p+k)} + 2^{2^{\hat{O}(\log t)}} = 2^{\hat{O}(p)} + 2^{\hat{O}(k)} + 2^{2^{\hat{O}(\log t)}}\). Therefore, \[\begin{align} & 2^{O((p+k)t^3 \log (p+k))} + 2^{2^{O(s + \log |P|)}} + 2^{O((p+k)t^2 \log(p+k))} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ =\;& 2^{O((p+k)t^3 \log (p+k))} + 2^{2^{O(s + \log |P|)}} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ =\;& 2^{\hat{O}(p+k)} + 2^{2^{\hat{O}(\log t)}} + 2^{2^{\hat{O}(s)}} + 2^{2^{\hat{O}(\log |P|)}} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)}. \end{align}\] As such, the desired function \(f\) exists. ◻

Proof. Let \(\mathcal{H}'= \{(G[\text{Im}(\lambda\oplus \lambda')],\lambda\oplus \lambda',\mu_{|\text{Im}(\lambda\oplus \lambda')}): \lambda' \in \varLambda_{G,k}\}\). Clearly, \(\mathcal{H}' \subseteq \mathcal{H}_{\sigma,k}\). We prove that \(\mathcal{H}'\) satisfies the desired condition. By definition, \[\begin{align} \mathsf{sgn}_S(G,\lambda,\mu) &= \left\{G[\text{Im}(\lambda\oplus \lambda')],\lambda\oplus \lambda',(\mu \otimes \mu')_{|\text{Im}(\lambda\oplus \lambda')}): \lambda' \in \varLambda_{G,k} \text{ and } \mu' \in U_{G,\{0,1\}^s}\right\} \\ &= \{(G[\text{Im}(\lambda\oplus \lambda')],\lambda\oplus \lambda',\mu_{|\text{Im}(\lambda\oplus \lambda')} \otimes \tau'): \lambda' \in \varLambda_{G,k} \text{ and } \tau' \in U_{G[\text{Im}(\lambda\oplus \lambda')],\{0,1\}^s}\} \\ &= \{(H,\gamma,\tau \otimes \tau'): (H,\gamma,\tau) \in \mathcal{H}' \text{ and } \tau' \in U_{H,\{0,1\}^s}\}, \end{align}\] which completes the proof. ◻

Proof. Lemma 20 implies that \(|\mathsf{sgn}_{((k,s))}(G,\lambda,\mu)| \leq |\mathcal{H}_{\sigma,k}| \cdot |U_{H,\{0,1\}^s}|\) for all \((G,\lambda,\mu) \in \mathcal{G}_{p,P,t}\). Therefore, we have \(\delta_{((k,s))}(\mathcal{G}_{p,P,t}) \leq |\mathcal{H}_{\sigma,k}| \cdot |U_{H,\{0,1\}^s}| = (p+k)^{O(\min\{k,t\} \cdot (p+k))} \cdot |P|^{O(k)} \cdot 2^{s(p+k)}\), because the graphs in \(\mathcal{H}_{\sigma,k}\) have at most \(p+k\) vertices and thus \(|U_{H,\{0,1\}^s}| \leq 2^{s(p+k)}\). As such, \(\delta_{((k,s))}(\mathcal{G}_{p,P,t})\) is bounded by \[8^{sk} + 8^{sp} + 2^{O(k \log |P|)} + 2^{\hat{O}(\min\{k,t\} \cdot k)} + 2^{\hat{O}(\min\{k,t\} \cdot p)}.\] Lemma 20 also implies that the \(S\)-signature of every graph in \(\mathcal{G}_{p,P,t}\) with core \(\sigma\) is uniquely determined by a subset \(\mathcal{H}' \subseteq \mathcal{H}_{\sigma,k}\). Therefore, the number of different \(S\)-signatures such graphs can have is bounded by the number of different subsets of \(\mathcal{H}_{\sigma,k}\), i.e., \(2^{|\mathcal{H}_{\sigma,k}|}\). Since \(|\mathcal{H}_{\sigma,k}| = (p+k)^{O(\min\{k,t\} \cdot (p+k))} \cdot |P|^{O(k)}\), we have \[2^{|\mathcal{H}_{\sigma,k}|} = \exp^{(2)}(O(k\log|P|)) + \exp^{(2)}(\hat{O}(\min\{k,t\} \cdot k)) + \exp^{(2)}(\hat{O}(\min\{k,t\} \cdot p)).\] As such, the desired function \(f\) exists. ◻

Proof. Let \(S = ((k_1,s_1),\dots,(k_r,s_r))\) and \(S' = ((k_2,s_2),\dots,(k_r,s_r))\). Also, let \(p,t \in \mathbb{N}\) and \(P\) be a set. To establish \(\delta\)-Bound\(_r\) and \(\Delta\)-Bound\(_r\), we need to bound \(\delta_S(\mathcal{G}_{p,P,t})\) and \(\Delta_S(\mathcal{G}_{p,P,t})\), both of which are related to \((\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k_1)}\), where \(p' = \min\{p+k_1,4t\}\) and \(P' = P \times \{0,1\}^{s_1} \times [4t]_0\), by our recurrences. So we first need to bound \((\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k_1)}\).

By assumption, we have \(\Delta\)-Bound\(_{r-1}\), which implies that \(\Delta_{S'}(\mathcal{G}_{p',P',t}) \leq \varPsi_{S',p',P',t,b_{r-1}}\). Thus, \((\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k_1)} \leq \varPsi_{S',p',P',t,b_{r-1}}^{7(p+k_1)}\). By definition, \(\varPsi_{S',p',P',t,b_{r-1}}\) is the sum of \(m = (r-1)(r+2)+1\) towers of exponentials with base \(b_{r-1}\) each of which has height at least 2. That is, \(\varPsi_{S',p',P',t,b_{r-1}}\) can be written in the form of \(\sum_{i=1}^m \exp_{b_{r-1}}^{(2)} (a_i)\). This allows us to apply Fact 10 to deduce \[\varPsi_{S',p',P',t,b_{r-1}}^{7(p+k_1)} \leq m^{m} \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1}) \cdot \left(b_{r-1}^{f(7(p+k_1))} + \sum_{i=1}^{r(r-1)} \exp_{b_{r-1}}^{(2)} (f(a_i)) \right).\] For convenience, write \(X = \sum_{i=1}^m \exp_{b_{r-1}}^{(2)} (f(a_i))\). Let \(b = (b_{r-1}^c)^{8^{c^2}}\). The terms in \(X\) one-to-one correspond to the terms in \(\varPsi_{S',p',P',t,b_{r-1}}\). Next, we consider these terms one by one and bound each of them by one or multiple terms in \(\psi_{S,p,P,t,b}\).

• For \(i \in \{3,\dots,d\}\) and \(j \in \{2,\dots,i-1\}\), \(\varPsi_{S',p',P',t,b_{r-1}}\) contains a term \[\exp_{b_{r-1}}^{(i)}(f_{i-1}(s_j k_i)) = \exp_{b_{r-1}}^{(i)}(f_i(s_j k_i))).\] This term corresponds to \(\exp_{b_{r-1}}^{(2)}(f(\exp_{b_{r-1}}^{(i-2)} (f_i(s_j k_i))))\) in \(X\), which is then bounded by \(\exp_{b_{r-1}^c}^{(i)}(f_i(s_j k_i))\) and hence bounded by \(\exp_b^{(i)}(f_i(s_j k_i))\).

• For \(i \in \{3,\dots,d\}\), \(\varPsi_{S',p',P',t,b_{r-1}}\) contains a term \[\exp_{b_{r-1}}^{(i)}(f_{i-1}(k_i \log|P'|)) = \exp_{b_{r-1}}^{(i)}(f_i(k_i\log|P|+s_1 k_i+ k_i\log (4t+1))).\] This term corresponds to \(\exp_{b_{r-1}}^{(2)}(f(\exp_{b_{r-1}}^{(i-2)} (f_i(k_i \log|P|+s_1 k_i+ k_i\log (4t+1)))))\) in \(X\), which is bounded by \(\exp_{b_{r-1}^c}^{(i)}(f_i(k_i\log|P|+s_1 k_i+ k_i\log (4t+1)))\). As \(f_i = f \circ f\), we have \[\begin{align} & f_i(k_i\log|P|+s_1 k_i+ k_i\log (4t+1)) \\ \leq\;& f_i(k_i\log|P|+2s_1 k_i+ 3k_i\log (4t+1)) \\ \leq\;& 6^c \cdot \max\{f_i(k_i\log|P|),f_i(s_1k_i),f_i(k_i \log t)\}. \end{align}\] Therefore, it follows that \[\begin{align} & \exp_{b_{r-1}^c}^{(i)}(f_i(k_i\log|P|+s_1 k_i+ k_i\log (4t+1))) \\ \leq\;& \exp_{b_{r-1}^c}^{(i)}(6^c \cdot f_i(k_i\log|P|)) + \exp_{b_{r-1}^c}^{(i)}(6^c \cdot f_i(s_1 k_i)) + \exp_{b_{r-1}^c}^{(i)}(6^c \cdot f_i(k_i \log t)) \\ \leq\;& \exp_b^{(i)}(f_i(k_i\log|P|)) + \exp_b^{(i)}(f_i(s_1 k_i)) + \exp_b^{(i)}(f_i(k_i \log t)). \end{align}\] Furthermore, \(\varPsi_{S',p',P',t,b_{r-1}}\) also contains the term \(\exp_{b_{r-1}}^{(2)}(f_1(k_2 \log|P'|))\). It corresponds to \(\exp_{b_{r-1}}^{(2)}(f(f_1(k_2 \log|P'|))) = \exp_{b_{r-1}}^{(2)}(f_2(k_2 \log|P'|)))\) in \(X\). By the argument above, we have \[\begin{align} & \exp_{b_{r-1}}^{(2)}(f_2(k_2 \log|P'|))) \\ =\;& \exp_{b_{r-1}}^{(2)}(f_2(k_2\log|P|+s_1 k_2+ k_2\log (4t+1))) \\ \leq\;& \exp_b^{(2)}(f_2(k_2\log|P|)) + \exp_b^{(2)}(f_2(s_1 k_2)) + \exp_b^{(2)}(f_2(k_2 \log t)). \end{align}\]

• For \(i,j \in \{3,\dots,d\}\) with \(j \leq i\), \(\varPsi_{S',p',P',t,b_{r-1}}\) contains a term \[\exp_{b_{r-1}}^{(i)}(f_{i-1}(\min\{k_j,t\} \cdot k_i)) = \exp_{b_{r-1}}^{(i)}(f_i(\min\{k_j,t\} \cdot k_i))).\] This term corresponds to \(\exp_{b_{r-1}}^{(2)}(f(\exp_{b_{r-1}}^{(i-2)} (f_i(\min\{k_j,t\} \cdot k_i))))\) in \(X\), which is then bounded by \(\exp_{b_{r-1}^c}^{(i)}(f_i(\min\{k_j,t\} \cdot k_i))\) and hence bounded by \(\exp_{b}^{(i)}(f_i(\min\{k_j,t\} \cdot k_i))\). Also, \(\varPsi_{S',p',P',t,b_{r-1}}\) contains the terms \(\exp_{b_{r-1}}^{(2)}(f_1(\min\{k_2,t\} \cdot k_2))\) and \(\exp_{b_{r-1}}^{(2)}(f_1(\min\{p',t\} \cdot k_2))\). These two terms correspond respectively to \(\exp_{b_{r-1}}^{(2)}(f(f_1(\min\{p',t\} \cdot k_2))) = \exp_{b_{r-1}}^{(2)}(f_2(\min\{p',t\} \cdot k_2)))\) and \(\exp_{b_{r-1}}^{(2)}(f(f_1(\min\{k_2,t\} \cdot k_2))) = \exp_{b_{r-1}}^{(2)}(f_2(\min\{k_2,t\} \cdot k_2)))\) in \(X\). We have \[\begin{align} & \exp_{b_{r-1}}^{(2)}(f_2(\min\{p',t\} \cdot k_2)) \\ =\;& \exp_{b_{r-1}}^{(2)}(f_2(\min\{p+k,t\} \cdot k_2)) \\ \leq\;& \exp_{b_{r-1}}^{(2)}(f_2(\min\{p,t\} \cdot k_2+\min\{k,t\} \cdot k_2)) \\ \leq\;& \exp_b^{(2)}(f_2(\min\{p,t\} \cdot k_2))+\exp_b^{(2)}(f_2(\min\{k,t\} \cdot k_2)), \end{align}\] where the last \(\leq\) follows from the fact that \(f_2(x+y) \leq 2^{c^2} \cdot \max\{f_2(x),f_2(y)\}\). The other term \(\exp_{b_{r-1}}^{(2)}(f_2(\min\{k_2,t\} \cdot k_2)))\) is clearly bounded by \(\exp_b^{(2)}(f_2(\min\{k_2,t\} \cdot k_2)))\).

• For \(i \in \{3,\dots,d\}\), \(\varPsi_{S',p',P',t,b_{r-1}}\) contains a term \(\exp_{b_{r-1}}^{(i)}(f_{i-1}(k_i \log t)) = \exp_{b_{r-1}}^{(i)}(f_i(k_i \log t)))\). This term corresponds to \(\exp_{b_{r-1}}^{(2)}(f(\exp_{b_{r-1}}^{(i-2)} (f_i(k_i \log t))))\) in \(X\), which is then bounded by \(\exp_{b_{r-1}^c}^{(i)}(f_i(k_i \log t))\) and hence bounded by \(\exp_{b}^{(i)}(f_i(k_i \log t))\). Also, \(\varPsi_{S',p',P',t,b_{r-1}}\) contains the term \(\exp_{b_{r-1}}^{(2)}(f_1(k_2 \log t))\). It corresponds to \(\exp_{b_{r-1}}^{(2)}(f(f_1(k_2 \log t))) = \exp_{b_{r-1}}^{(2)}(f_2(k_2 \log t))\) in \(X\), which is bounded by \(\exp_b^{(2)}(f_2(k_2 \log t))\).

• Finally, \(\varPsi_{S',p',P',t,b_{r-1}}\) contains the term \[\exp_{b_{r-1}}^{(2)}(f_1(\min\{k_2,t\} \cdot p')) = \exp_{b_{r-1}}^{(2)}(f_1(\min\{k_2,t\} \cdot \min\{p+k_1,4t\})).\] It corresponds to \(\exp_{b_{r-1}}^{(2)}(f(f_1(\min\{k_2,t\} \cdot \min\{p+k_1,4t\})))\) in \(X\). We have \[\begin{align} & \exp_{b_{r-1}}^{(2)}(f(f_1(\min\{k_2,t\} \cdot \min\{p+k_1,4t\}))) \\ =\;& \exp_{b_{r-1}}^{(2)}(f_2(\min\{k_2,t\} \cdot \min\{p+k_1,4t\})) \\ \leq\;& \exp_{b_{r-1}}^{(2)}(f_2(\min\{p+k_1,4t\} \cdot k_2)) \\ \leq\;& \exp_{b_{r-1}}^{(2)}(f_2(4 \cdot \min\{p,t\} \cdot k_2 + 4 \cdot \min\{k_1,t\} \cdot k_2)) \end{align}\] Using the fact that \(f_2(4x+4y) = 8^{c^2} \cdot \max\{f_2(x),f_2(y)\}\), we further have \[\begin{align} & \exp_{b_{r-1}}^{(2)}(f_2(4 \cdot \min\{p,t\} \cdot k_2 + 4 \cdot \min\{k_1,t\} \cdot k_2)) \\ \leq\;& \exp_b^{(2)}(f_2(\min\{p,t\} \cdot k_2)) + \exp_b^{(2)}(f_2(\min\{k_1,t\} \cdot k_2)). \end{align}\]

Now we see that each term in \(X\) is bounded by one or multiple terms in \(\varPsi_{S,p,P,t,b}\), and is thus at most \(\varPsi_{S,p,P,t,b}\). It follows that \(X \leq m \cdot \psi_{S,p,P,t,b} \leq r^2 \cdot \psi_{S,p,P,t,b}\). Since \[b_{r-1}^{f(7(p+k_1))} \leq b_{r-1}^{7cf(p)+7cf(k_1)} \leq b_{r-1}^{14cf(p)}+b_{r-1}^{14cf(k_1)} \leq b^{f_1(p)}+b^{f_1(k_1)} \leq \psi_{S,p,P,t,b},\] we have \(\varPsi_{S',p',P',t,b_{r-1}}^{7(p+k_1)} \leq (m^m \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1})+1) \cdot \psi_{S,p,P,t,b}\), which implies \[\begin{align} & 2^{f(p)} + 2^{f(k)} + \exp^{(2)}(f(\log t)) + \exp^{(2)}(f(s)) + \exp^{(2)}(f(\log|P|)) + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ \leq\;& \psi_{S,p,P,t,2} + (\Delta_{S'}(\mathcal{G}_{p',P',t}))^{7(p+k)} \\ \leq\;&\psi_{S,p,P,t,2} + (m^m \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1})+1) \cdot \psi_{S,p,P,t,b} \\ \leq\;& (m^m \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1})+2) \cdot \psi_{S,p,P,t,b} \\ \leq\;&\psi_{S,p,P,t,b'}, \end{align}\] where \(b' = (m^m \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1})+2) b\). Then Corollary 2 directly implies \(\delta_S(\mathcal{G}_{p,P,t}) \leq \psi_{S,p,P,t,b'}\) and \(\Delta_S(\mathcal{G}_{p,P,t}) \leq 2^{\psi_{S,p,P,t,b'}}\). Recall that \(\psi_{S,p,P,t,b'}\) consists of \(r(r+2)+1\) terms each of which is a tower of exponentials with base \(b'\). Thus, \(2^{\psi_{S,p,P,t,b'}} \leq \varPsi_{S,p,P,t,(r(r+2)+1)b'}\) by Fact 8. Note that \[\begin{align} b_r &= (r+1)^{2(r+1)} \cdot \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1} + 10c^3) \\ &\geq (r+1)^{2(r+1)} \cdot \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1}) \cdot (b_{r-1}^c)^{8^{c^2}} \\ &\geq (r(r+2)+1)\cdot ((r-1)(r+3)+1)^{(r-1)(r+3)+1} \cdot \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1}) \cdot b \\ &= (r(r+2)+1)\cdot m^m \exp_{b_{r-1}}^{(2)}(2 \log b_{r-1}) \cdot b \\ &\geq (r(r+2)+1)\cdot b'. \end{align}\] Therefore, we directly have \(\delta_S(\mathcal{G}_{p,P,t}) \leq \psi_{S,p,P,t,b_r}\) and \(\Delta_S(\mathcal{G}_{p,P,t}) \leq \varPsi_{S,p,P,t,b_r}\), which gives us the desired \(\delta\)-Bound\(_r\) and \(\Delta\)-Bound\(_r\). ◻

Proof. When \(z = 0\), the inequality trivially holds. So assume \(z \geq 1\). Observe that for most of the exponential towers in \(\psi_{S_z,p_z,P_z,t,b_{d-z}}\), there is a corresponding tower in \(\psi_{S,p,P,t,b_{d-z}}\) with larger height and base, except the terms

(i) \(b_{d-z}^{f_1((\log|P|+s_1+\cdots+s_z) \cdot k_i)}\) for \(i \in \{z+1,\dots,d\}\),

(ii) \(b_{d-z}^{f_1(\min\{p+k_1+\cdots+k_z,t\} \cdot k_i)}\) for \(i \in \{z+1,\dots,d\}\),

(iii) \(b_{d-z}^{f_1(\min\{k_{z+1},t\} \cdot (p+k_1+\cdots+k_z))}\).

Recall that \(f_1 = f\) and we have the number \(c\) such that \(f(ax) \leq a^c f(x)\) for all \(a,x \in \mathbb{N}\). Therefore, \(f_1((\log|P|+s_1+\cdots+s_z) \cdot k_i) \leq (z+1)^c \cdot \max\{f_1(k_i \log|P|),f_1(s_1k_i),\dots,f_1(s_zk_i)\}\), which implies \[\begin{align} \sum_{i=z+1}^d b_{d-z}^{f_1((|P|+s_1+\cdots+s_z) \cdot k_i)} &\leq (z+1)^c \cdot \left(\sum_{i=z+1}^d b_{d-j}^{f_1(k_i \log|P|)} + \sum_{i=z+1}^d \sum_{j=1}^z b_{d-j}^{f_1(s_jk_i)} \right) \\ & \leq (z+1)^c \cdot \psi_{S,p,P,t,b_{d-z}} \leq \psi_{S,p,P,t,(z+1)^c b_{d-z}}. \end{align}\] Similarly, we can show \(\sum_{i=z+1}^d b_{d-z}^{f_1(\min\{p+k_1+\cdots+k_z,t\} \cdot k_i)} \leq \psi_{S,p,P,t,(z+1)^c b_{d-z}}\) as well. Finally, we consider \(b_{d-z}^{f_1(\min\{k_{z+1},t\} \cdot (p+k_1+\cdots+k_z))}\). Because \(\min\{k_{z+1},t\} \cdot x \leq \min\{k_{z+1},t\} \cdot k_{z+1} + \min\{x,t\} \cdot x\), \[\begin{align} & f_1(\min\{k_{z+1},t\} \cdot (p+k_1+\cdots+k_z)) \\ \leq\;& f_1\left(\min\{p,t\} \cdot p+ \sum_{j=1}^z \min\{k_j,t\} \cdot k_j + (z+1) \cdot \min\{k_{z+1},t\} \cdot k_{z+1} \right) \\ \leq\;& (2z+2)^c \cdot \max\{f_1(\min\{p,t\} \cdot p),f_1(\min\{k_1,t\} \cdot k_1),\dots,f_1(\min\{k_{z+1},t\} \cdot k_{z+1})\}, \end{align}\] which implies \(b_{d-z}^{f_1(\min\{k_{z+1},t\} \cdot (p+k_1+\cdots+k_z))} \leq (2z+2)^c \cdot \sum_{i=1}^{z+1} b_{d-z}^{f_1(\min\{k_i,t\} \cdot k_i)} \leq \psi_{S,p,P,t,(2z+2)^c b_{d-z}}\).

To summarize, the sum of the terms in (i), (ii), and (iii) above is bounded by \(3 \psi_{S,p,P,t,(2z+2)^c b_{d-z}}\), and the sum of the other terms in \(\psi_{S_z,p_z,P_z,t,b_{d-z}}\) is bounded by \(\psi_{S,p,P,t,b_{d-z}}\). Therefore, we have \(\psi_{S_z,p_z,P_z,t,b_{d-z}} \leq 4 \psi_{S,p,P,t,(2z+2)^c b_{d-z}}\). Since \(b_d \geq 4(2z+2)^c b_{d-z}\) for all \(z \geq 1\) by our construction, we eventually have \(\psi_{S_z,p_z,P_z,t,b_{d-z}} \leq \psi_{S,p,P,t,b_d}\). ◻

Proof. Let \((G,t,S,\phi)\) be an instance of MSO Testing where \(S = ((k_1,s_1),\dots,(k_d,s_d))\). We first compute a nice tree decomposition of \(G\) with width \(t' = t^{O(1)}\) in \(T_\mathsf{td}(G,t)\) time. Then we apply Theorem 5 to compute \(\mathsf{sgn}(G)\) and further apply Lemma 13 to test whether \(G\) satisfies \(\phi\) or not. By Theorem 7, for any \(\mu \in U_{G,[t'+1]_0}\), \(\lVert \mathsf{sgn}_S(G,-,\mu) \rVert^{O(1)}\) is bounded by \[f(d) \cdot \left(\sum_{i=1}^d \sum_{j=1}^{i-1} \exp^{(i)}(\hat{O}(s_j k_i)) + \sum_{i=1}^d \sum_{j=1}^i \exp^{(i)}(\hat{O}(t_j k_i)) + \sum_{i=1}^d \exp^{(i)}(\hat{O}(k_i \log t)) + \sum_{i=1}^d 2^{O(s_d k_i)} \right)\]for some computable function \(f\), where \(t_j = \min\{k_j,t\}\). This also bounds the part \(\sum_{i=1}^d 2^{O(k_i\log t)}+\sum_{i=1}^{d-1} 2^{O(s_i t)}+ \sum_{i=1}^d 2^{O(s_d k_i)}\) in Theorem 5, simply because \(2^{O(s_it)} = 2^{\hat{O}(s_i)} + 2^{2^{\hat{O}(\log t)}}\) by Fact 10. Therefore, the total running time of the algorithm follows the bound in the theorem. ◻

Proof. The proof is the same as that of Theorem [thm-MSO], with Theorem 5 and Lemma 13 replaced with Theorem 6 and Lemma 17, respectively. ◻

Proof. The graph \(G'\) is obtained by modifying \(G\) as follows. For each edge \(e = (u,v) \in E(G)\), we add a new vertex \(v_e'\) together with two edges two edges \((u,v_e')\) and \((v,v_e')\). Also, we add a self-loop on \(v_e'\). Let \(G'\) be the resulting graph. Clearly, \(|V(G')| = |V(G)|+|E(G)| = O(tn)\) and \(\mathbf{tw}(G') \leq \mathbf{tw}(G)+1\). Let \(V_1(G') \subseteq V(G')\) consists of the vertices that are originally in \(G\) and \(V_2(G') \subseteq V(G')\) consists of the new vertices \(v_e'\). Let \(\pi:V(G) \cup E(G) \rightarrow V(G')\) be the bijective function that maps each vertex \(v \in V(G)\) to its corresponding vertex in \(V_1(G')\) and maps each edge \(e \in E(G)\) to \(v_e' \in V_2(G')\).

The construction of \(\phi'\) is more complicated. We need to apply induction on \(|S|\). For \(d \in \mathbb{N}_0\), we show that for every sequence \(S\) of \(d\) pairs of natural numbers and every \(S\)-MSO\(_2\) formula \(\phi\) (with free variables), one can construct an \(S\)-MSO formula \(\phi'\) satisfying the following conditions.

(i) The free variables of \(\phi\) one-to-one correspond to the free variables of \(\phi'\). If \(x\) is a free vertex/edge variable of \(\phi\), then it corresponds to a free vertex variable of \(\phi'\). If \(X\) is a free vertex/edge set variable of \(\phi\), then it corresponds to a free (vertex) set variable of \(\phi'\). Let \(\mathcal{X}_v'\), \(\mathcal{X}_e'\), \(\mathcal{X}_V'\), \(\mathcal{X}_E'\) denote the sets of free variables of \(\phi'\) corresponding to vertex variables, edge variables, vertex set variables, and edge set variables of \(\phi\), respectively.

(ii) For convenience, for an assignment \(A\) of a formula and a free variable \(x\) of the formula, we denote by \(A(x)\) the value of \(x\) in \(A\). We say an assignment \(A'\) of \(\phi'\) in \(G'\) is valid if for every \(x' \in \mathcal{X}_v'\) (resp., \(x' \in \mathcal{X}_e'\)), \(A'(x') \in V_1(G')\) (resp., \(A'(x') \in V_2(G')\)). If \(A'\) is a valid assignment of \(\phi'\) in \(G'\), then it naturally corresponds to an assignment \(A\) of \(\phi\) in \(G\):

 - if $x$ is a free vertex/edge variable of $\phi$ corresponding to
   $x' \in \mathcal{X}_v'$, let $A(x) = \pi^{-1}(A'(x'))$;

 - if $X$ is a free vertex set (resp., edge set) variable of $\phi$
   corresponding to $X' \in \mathcal{X}_V'$, let
   $A(X) = \pi^{-1}(A'(X') \cap V_1(G'))$ (resp.,
   $A(X) = \pi^{-1}(A'(X') \cap V_2(G'))$).

 We require $\phi'$ to satisfy the following condition: for every
 valid assignment $A'$ of $\phi'$ in $G'$ and its corresponding
 assignment $A$ of $\phi$ in $G$, $\phi'(A') = \phi(A)$.

When \(d = 0\), \(\phi\) is quantifier-free and the construction of \(\phi'\) is the following. The free variables of \(\phi'\) is one-to-one corresponding to those of \(\phi\) as required in condition (i). We replace each variable in \(\phi\) with its corresponding variable of \(\phi'\), and change each atomic formula \(\mathsf{inc}(\cdot,\cdot)\) in \(\phi\) to \(\mathsf{adj}(\cdot,\cdot)\). Let \(\phi'\) be the resulting formula. By checking the atomic formula, it is easy to verify that condition (ii) holds for \(\phi'\). Suppose that for every \(S\) of length \(d-1\) and every \(S\)-MSO\(_2\) formula \(\phi\) (with free variables), we can construct the corresponding \(S\)-MSO formula \(\phi'\) satisfying the two conditions. Consider a sequence \(S = ((k,s))+S'\) with \(|S| = d\) and an \(S\)-MSO\(_2\) formula \(\phi\). Without loss of generality, we can assume \(\phi(F) = \mathsf{Q} x_1\dots \mathsf{Q} x_k \mathsf{Q} X_1,\dots,\mathsf{Q} X_s\;\phi_0(F,x_1,\dots,x_k,X_1,\dots,X_s)\) where \(F\) denotes the free variables of \(\phi\), \(\mathsf{Q} \in \{\exists,\forall\}\), \(x_1,\dots,x_k\) are vertex/edge variables, \(X_1,\dots,X_s\) are vertex/edge set variables, and \(\phi_0\) is an \(S'\)-MSO\(_2\) formula. As \(|S'| = d-1\), \(\phi_0\) has a corresponding \(S'\)-MSO formula \(\phi_0'\) satisfying the two conditions. Let \(I = \{i \in [k]: x_i \text{ is a vertex variable}\}\) and \(J = \{j \in [s]: X_j \text{ is a vertex set variable}\}\). If \(\mathsf{Q}=\exists\), then we define \[\phi'(F') = \exists x_1'\dots \exists x_k' \exists X_1',\dots,\exists X_s'\;\left(\bigwedge_{i \in I} \neg\mathsf{adj}(x_i',x_i')\right)\wedge\left(\bigwedge_{i \in [k] \backslash I} \mathsf{adj}(x_i',x_i')\right)\wedge \phi_0'(F',x_1',\dots,x_k',X_1',\dots,X_s'),\]where \(x_1',\dots,x_k'\) are vertex variables and \(X_1',\dots,X_s'\) are (vertex) set variables. Here the variables in \(F'\) one-to-one correspond to the variables in \(F\) as in condition (i), and the argument \(x_i'\) (resp., \(X_j'\)) of \(\phi_0'\) corresponds to the argument \(x_i\) (resp., \(X_j\)) of \(\phi_0\). Clearly, \(\phi'\) is an \(S\)-MSO formula. We claim that \(\phi'\) satisfies condition (ii). Let \(A'\) be an assignment of \(\phi'\) and \(A\) be its corresponding assignment of \(\phi\). Assume \(\phi'(A') = \mathsf{True}\). There there should exist \(x_1',\dots,x_k' \in V(G')\) and \(X_1',\dots,X_s' \subseteq V(G')\) that makes the part of \(\phi'(A')\) after the sequence of quantifiers true. The fact that \((\bigwedge_{i \in I} \neg\mathsf{adj}(x_i',x_i')) \wedge (\bigwedge_{i \in [k] \backslash I} \mathsf{adj}(x_i',x_i')) = \mathsf{True}\) and the construction of \(G'\) guarantees that \(x_i' \in V_1(G)\) if \(i \in I\) and \(x_i' \in V_2(G)\) if \(i \notin I\). Set \(x_i = \pi^{-1}(x_i')\) for \(i \in [k]\), \(X_j = \pi^{-1}(X_j' \cap V_1(G'))\) for \(j \in J\), and \(X_j = \pi^{-1}(X_j' \cap V_2(G'))\) for \(j \in [s] \backslash J\). We have \(x_i \in V(G)\) if \(i \in I\) and \(x_i \in E(G)\) if \(i \in I\). Furthermore, since \(\phi_0'(A',x_1',\dots,x_k',X_1',\dots,X_s') = \mathsf{True}\), we have \(\phi_0(A,x_1,\dots,x_k,X_1,\dots,X_s) = \mathsf{True}\) by our induction hypothesis. It follows that \(\phi(A) = \mathsf{True}\). Next, assume \(\phi(A) = \mathsf{True}\). Then there should exist \(x_i \in V(G)\) for \(i \in I\), \(x_i \in E(G)\) for \(i \in [k] \backslash I\), \(X_j \subseteq V(G)\) for \(j \in J\), and \(X_j \subseteq E(G)\) for \(j \in [s] \backslash J\) such that \(\phi_0(A,x_1,\dots,x_k,X_1,\dots,X_s) = \mathsf{True}\). Set \(x_i' = \pi(x_i)\) for \(i \in [k]\) and \(X_i' = \pi(X_i)\) for \(j \in [s]\). Clearly, \(\neg\mathsf{adj}(x_i',x_i')\) for all \(i \in I\) and \(\mathsf{adj}(x_i',x_i')\) for all \(i \in [k] \backslash I\). Furthermore, the construction of \(X_1',\dots,X_s'\) satisfies that \(X_j = \pi^{-1}(X_j' \cap V_1(G'))\) for \(j \in J\) and \(X_j = \pi^{-1}(X_j' \cap V_2(G'))\) for \(j \in [s] \backslash J\). Therefore, \(\phi_0'(A',x_1',\dots,x_k',X_1',\dots,X_s') = \mathsf{True}\) by our induction hypothesis, which further implies that \(\phi'(A') = \mathsf{True}\). So \(\phi'\) satisfies condition (ii). On the other hand, if \(\mathsf{Q} = \forall\), then we define \[\phi'(F') = \forall x_1'\dots \forall x_k' \forall X_1',\dots,\forall X_s'\;\left(\bigwedge_{i \in I} \neg\mathsf{adj}(x_i',x_i')\right)\wedge\left(\bigwedge_{i \in [k] \backslash I} \mathsf{adj}(x_i',x_i')\right) \rightarrow \phi_0'(F',x_1',\dots,x_k',X_1',\dots,X_s').\]A similar argument as above shows that in this case, \(\phi'\) satisfies condition (ii) as well. Therefore, our induction works. This completes the construction of \(\phi'\). One can easily verify that the time for the construction is \(|\phi|^{O(1)}\). ◻

Proof. Let \(G\) be the given \(n\)-vertex graph. Let \(V(G)=\{1,2,\ldots,n\}\) and \(E(G)=\{e_1,\ldots,e_m\}\). Now we partition \(V(G)\) into \(\alpha\) groups \(V_1,\ldots,V_{\alpha}\) such that for each \(i\in [\alpha]\), \(|V_i|\leq \lceil \frac{n}{\alpha}\rceil\). Let \(\ell=3^{\lceil \frac{n}{\alpha}\rceil}\). For each \(i\in [\alpha]\), there are at most \(\ell\) proper \(3\)-colorings of \(G[V_i]\). Let us call these \(3\)-colorings \(c_{i,1},\ldots c_{i,{\ell}_i}\).

Construction. Now we construct a tree \(T\) rooted at a node \(rt\) as follows. The root \(rt\) has \(\alpha+m\) children and we name them \(U_1,\ldots,U_{\alpha}\) and \(f_1,\ldots, f_m\). That is, each node \(U_i\) corresponds to the vertex subset \(V_i\) of \(G\) and each node \(f_i\) corresponds to the edge \(e_i\) of \(G\). Each node \(f_i\) has two children corresponding to the endpoints of \(e_i\). Let us name these nodes with \(f_{i,a}\) and \(f_{i,b}\), where \(a\) and \(b\) are the endpoints of \(e_i\). Now, we explain the children of each \(U_i\). Recall that \(\{c_{i,1},\ldots,c_{i,\ell_i}\}\) is the set of all proper \(3\)-colorings of \(G[V_i]\). The node \(U_i\) has \(\ell_i\) children, and they are named \(C_{i,1},\ldots,C_{i,\ell_i}\). Each \(C_{i,j}\) has \(|V_i|\) children, and each of them corresponds to a vertex in \(V_i\). That is, each \(a\in V_i\), \(C_{i,j}\) has a child node named \(v_{i,j,a}\). Now, each \(v_{i,j,a}\) has two children \(id_{i,j,a}\) and \(c_{i,j,a}\). See Figure 4 for an illustration.

Next, we define \(9\) unary label predicates on \(T\).

• \({\sf R}=\{rt\}\).

• \({\sf EN}=\{f_1,\ldots,f_m\}\)

• \({\sf EP}\) is the set of children of nodes in \({\sf EN}\).

• \({\sf P}\) is the union of the set of children of \(U_i\) over all \(i\). That is, \({\sf P}=\{C_{i,j}~:~i\in [\alpha], j\in [\ell_i]\}\).

• \({\sf N}=\{v_{i,j,a}~:~i\in [\alpha],j\in [\ell_i],a\in V_i\}\)

• \({\sf I}=\{id_{i,j,a}~:~i\in [\alpha], j\in [\ell_i],a\in V_i\}\)

• For each \(q\in [3]\), \({\sf Q}_q=\{c_{i,j,a} ~:~a \textit{ is colored with q in the proper coloring c_{i,j} of G[V_i]}\}\).

Next we define the function \({\sf id}\) on \({\sf EP\cup I}\).

\[{\sf id}(x) = \left\{ \begin{array}{rcl} b & if & x=f_{s,b}\in {\sf EP} \\ a & if & x=id_{i,j,a}\in {\sf I} \end{array}\right.\]

Now we define an FO+\({\sf id}\) formula. We want to encode the statement that “there exist nodes \(x_1, x_2,\ldots, x_{\alpha}\) that correspond to proper \(3\)-colorings of \(G[V_1],\ldots G[V_{\alpha}]\), respectively, such that for any node \(z \in {\sf EN}\), the endpoints of the edge corresponding to \(z\) should get different colors according to the selected colorings of \(G[V_1],\ldots G[V_{\alpha}]\)”. This can be encoded as follows.

\[\begin{align} \psi \equiv&& \exists r \in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \exists p_1 \ldots \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3\nonumber\\ && \psi_{{\sf evalid}} \wedge( \psi_{{\sf uvalid}} \Rightarrow ( \psi_{{\sf id}}\Rightarrow \psi_{{\sf color}} ))\nonumber\\ &\equiv& \exists r \in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \exists p_1 \ldots \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \psi_{{\sf evalid}} \wedge ( \neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf id}}\vee \psi_{{\sf color}}) \label{eqn:psi1} \end{align}\tag{9}\]

Here, \(\psi_{\sf evalid}\) and \(\psi_{\sf uvalid}\) ensure that the selected vertices are valid. Before explaining it, let us define \(\psi_{{\sf id}}\) and \(\psi_{{\sf color}}\). The formula \(\psi_{{\sf id}}\) is the formula \({\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2)\). Next, we explain the formula \(\psi_{{\sf color}}\).

\[\psi_{{\sf color}}\equiv \neg (\bigvee_{i\in [3]} (c_1\in {\sf Q}_i \wedge c_2\in {\sf Q}_i) )\]

That is, \(\psi_{{\sf color}}\) is true if and only if \(c_1\) and \(c_2\) are two different colors. To define \(\psi_{\sf uvalid}\), let us first define \({\sf con}(X,Y)\) for two sets of variables \(X\) and \(Y\). \({\sf con}(X,Y)\) is true if and only if every vertex \(x\in X\) is adjacent to at least one vertex in \(Y\). Formally, \[{\sf con}(X,Y)=\bigwedge_{x\in X}\left(\bigvee_{y\in Y} {\sf adj(x,y)}\right).\]

Now, \(\psi_{{\sf uvalid}}\) is defined below.

\[\psi_{{\sf uvalid}}\equiv {\sf con}(\{z_1,z_2\},\{z\})\wedge {\sf con}(\{v_1,v_2\},\{x_1,\ldots,x_{\alpha}\}) \wedge {\sf con}(\{y_1,c_1\},\{v_1\})\wedge {\sf con}(\{y_2,c_2\},\{v_2\}).\]

We also need \(x_1, x_2,\ldots, x_{\alpha}\) to correspond to appropriate \(3\)-colorings, one for each \(G[V_i]\), where \(i\in [\alpha]\). We encode it using a formula \(\psi_{\sf evalid}\) as follows.

\[\psi_{\sf evalid} \equiv \left(\bigwedge_{1\leq i < j \leq [\alpha]} p_i\neq p_j \right) \wedge \left( \bigwedge_{i\in \alpha} {\sf adj}(x_i,p_i)\wedge {\sf adj}(p_i,r)\right)\]

It is easy to see that \(\psi\) is an \((2\alpha+1,9)\)-FO+id formula and \(|\psi|=O(\alpha^2)\). Notice that the size of \(T\) is \(O(3^{n/\alpha}+m)\) and it can be constructed in time \(O(3^{n/\alpha}+m)\). Now prove the correctness of the reduction.

 ◻

Proof. We need an FO formula to represent \({\sf id}(z)={\sf id}(y)\) for two variables \(z\) and \(y\). First, we create two label predicates \({\boldsymbol{1}}\) and \({\boldsymbol{0}}\). Let \(k\) be the smallest integer such that \(k\geq \log n\). For any node \(t\) in \(T\) such that \({\sf id}(t)\) is defined, we do the following. We know that \({\sf id}(t)\in [n]\). Thus, \({\sf id}(t)\) can be represented in binary using \(k\) bits. Let \(\pi_t\) be a path \(a_1,\ldots,a_{k},t\) on \(k+1\) vertices. Now, we replace node \(t\) with path \(\pi_t\). Let \(b_1,\ldots,b_{k}\) be the binary representation of the number \({\sf id}(t)\). For each \(i\in [k]\), \(a_i\in {\boldsymbol{0}}\) if \(b_i=0\) and \(a_i\in {\boldsymbol{1}}\) otherwise. The tree constructed as explained above is \(T'\). Clearly, \(|V(T')|=O(|V(T)|\cdot \log n)\). Now, for two leaf nodes \(z\) and \(y\) in \(T\), \({\sf id}(z)={\sf id}(y)\) can be encoded as

\[\begin{align} \exists a_1,a_1'\in {\boldsymbol{O}}\cup {\boldsymbol{1}} \ldots \exists a_{k},a_{k}' \in {\boldsymbol{O}}\cup {\boldsymbol{1}}&& \left(\bigwedge_{i\in [k] } (a_i \in {\boldsymbol{0}} \Leftrightarrow a'_i \in {\boldsymbol{0}})\right) \\ && \wedge {\sf path}(a_1,\ldots,a_{k},z) \wedge {\sf path}(a'_1,\ldots,a'_{k},y) \end{align}\]

where, \({\sf path}(w_1,\ldots,w_q) \equiv (\bigwedge_{i\in [q-1]} {\sf adj}(w_i,w_{i+1}))\). Notice that the number of quantifiers in the above formula is \(2\log n\). ◻

Proof. Like in Lemma 26, we need an FO formula to represent \({\sf id}(z)={\sf id}(y)\) for two variables \(z\) and \(y\). First, we create four label predicates \({\boldsymbol{1}}\), \({\boldsymbol{0}}\), \({\sf L}_1\), and \({\sf L}_2\). Let \(k\) and \(k'\) be the smallest integers such that \(k\geq \log n\) and \(k'\geq \log \log n\). For any node \(t \in V(T)\) such that \({\sf id}(t)\) is defined, we do the following. We know that \({\sf id}(t)\in [n]\). Thus, \({\sf id}(t)\) can be represented in binary using \(k\) bits. Let \(b_1\ldots b_{k}\) be the binary representation of the number \({\sf id}(t)\). Now we replace \(t\) with a subtree as shown in Figure 5. That is, \(t\) has \(k\) children \(a_1,\ldots,a_k\) and each \(a_i\) has two children \(d_i\) and \(c_i\). Here, each \(a_i\) represents \(b_i\) in the following way. We set \({\sf id}(d_i)=i\), \(c_i\in {\boldsymbol{O}}\) if \(b_i=0\) and \(c_i\in {\boldsymbol{1}}\) if \(b_i=1\). In other words, \({\sf id}(d_i)\) represents the position of \(b_i\) in the binary representation \(b_1\ldots b_{k}\) and \(c_i\) denotes the value of the bit \(b_i\). The crucial observation is that for each \(i\in [k]\), \({\sf id}(d_i)\) is a positive integer less than or equal to \(\lceil \log n \rceil\). Now we add all \(a_i\) to \({\sf L}_1\) and all \(d_i\) to \({\sf L}_2\). Let us name the tree constructed as \(T_1\). It is easy to see that \(|V(T_1)|=O(|V(T)| \log n)\).

Informally, for two leaf nodes \(z\) and \(y\) in \(T\), \({\sf id}(z)={\sf id}(y)\) is true if and only if for any child \(a\) of \(z\) and any child \(a'\) of \(y\) if the id of the left child of \(a\) and the id of the left child of \(a'\) are equal, then the corresponding bits (encoded in the right child of \(a\) and \(a'\)) are same. This can be encoded as follows.

\[\begin{align} {\sf id}(z)={\sf id}(y) &\equiv& \forall a,a' \in {\sf L}_1, \forall d,d' \in {\sf L}_2 \forall c,c' \in {\boldsymbol{0}}\cup {\boldsymbol{1}} \;\; \phi_{{\sf valid}} \Rightarrow ( \phi_{{\sf id}}\Rightarrow \phi_{{\sf bit}} )\nonumber\\ &\equiv& \forall a,a' \in {\sf L}_1, \forall d,d' \in {\sf L}_2 \forall c,c' \in {\boldsymbol{0}}\cup {\boldsymbol{1}} \;\; (\neg \phi_{{\sf valid}} \vee \neg \phi_{{\sf id}}\vee \phi_{{\sf bit}} )\label{eqn:uniloglog} \end{align}\tag{10}\]

Here, \(\phi_{{\sf valid}}\), \(\phi_{{\sf id}}\) and \(\phi_{{\sf bit}}\) are defined below.

\[\begin{align} \phi_{\sf id} &\equiv& {\sf id}(d)={\sf id}(d')\\ \phi_{\sf bit} &\equiv& c \in {\boldsymbol{0}} \Leftrightarrow c'\in {\boldsymbol{0}} \\ \phi_{\sf valid} &\equiv& ({\sf con}(\{d,c\},\{a\})\wedge ({\sf con}(\{d',c'\},\{a'\}) \wedge {\sf adj}(a,z) \wedge {\sf adj}(a',y) \end{align}\]

The formula \(\phi_{\sf valid}\) is true if and only if \(a\) and \(a'\) are children of \(z\) and \(y\), respectively, \(d\) and \(c\) are children of \(a\), and \(d'\) and \(c'\) are children of \(a'\). The formula \(\phi_{\sf bit}\) is true if and only if they both encode the same bit. Clearly, the formula in (10 ) is not an FO formula, but an FO+\({\sf id}\) formula with the value of \({\sf id}(d)\) and \({\sf id}(d')\) are positive integers less than or equal to \(\lceil \log n \rceil\). So, we apply Lemma 26 on \(T_1\) where \(n\) is replaced with \(\log n\). Thus, we get a tree \(T'\) (which is super graph of \(T_1\)) and a \((\log\log n)\)-FO formula \(\phi_{\exists}\) on two free variables with the following specifications.

(a) For any two leaf nodes \(d\) and \(d'\) in \(T_1\), \(T'\models \phi_{\exists}(d,d')\) if and only if \({\sf id}(d)={\sf id}(d')\).

(b) All the quantifiers in \(\phi_{\exists}(d,d')\) are existential quantifiers and \(|\phi_{\exists}(d,d')|=O(\log \log n)\)

(c) The number of label predicates used in \(\phi_{\exists}(z,y)\) is two.

(d) \(V(T')=O(|V(T_1)|\cdot \log\log n)\)

Thus, we can replace \(\phi_{\sf id}\) in the formula in (10 ) with \(\phi_{\exists}(d,d')\). Notice that there is negation before \(\phi_{\sf id}\) in the formula in (10 ). The formula \(\neg \phi_{\exists}(d,d')\) is of the form \(\neg \exists a_1 \ldots \exists a_{k} \phi'\) where \(\phi'\) is quantifier free and \(k=2\log \log n\). This implies that \[\neg \phi_{\exists}(d,d') \equiv \forall a_1 \ldots \forall a_{k} \neg \phi'.\]

Thus, by replacing \(\phi_{\sf id}\) in the formula in (10 ) with \(\phi_{\exists}(d,d')\), we get \((6+2\log \log n)\)-FO formula \(\phi_{\forall}\) where all the quantifiers are universal quantifiers. By Lemma 26 and (10 ), we get that the length of \(\phi_{\forall}\) is \(O(\log \log n)\). Property (d) above and the fact that \(|V(T_1)|=O(|V(T)|\cdot \log n)\) implies that \(|V(T')|=O(|V(T)|\cdot \log n \cdot \log \log n)\). Initially, we created four label predicates and Lemma 26 introduced two label predicates. Thus total number of label predicates created is \(6\). This completes the proof of the lemma. ◻

Proof sketch. Follow the proof of Lemma 27 until the construction of formula in (10 ). The formula in the right hand side of the equation in (10 ) is the required formula where \(\phi_1(z,y)\) is \(\neg \phi_{\sf valid} \vee \phi_{\sf bit}\). ◻

Proof. When \(d=1\), Lemma 27 implies the lemma. Now cosnider the case when \(d>1\). Apply Lemma 29 and obtain a tree \(T_1\) and \((c_1,\ldots,c_d)\)-FO+id formula \(\phi\) with specifications mentioned in the lemma. Since \(d\) is an odd number, condition (b) in Lemma 29 implies that for any two leaf nodes \(z,y\) in \(T\), \(\phi(z,y)\) is of the form

\[\begin{align} \forall x_{1,1}, \ldots, \forall x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \vee \nonumber\\ (\exists x_{2,1}\ldots,\exists x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \wedge \nonumber\\ (\forall x_{3,1}, \ldots, \forall x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\vee \nonumber\\ \vdots && \nonumber\\ (\forall x_{d,1}, \ldots, \forall x_{d,6} && (\phi_d(x_{d-1,1},x_{d-1,2},x_{d,1},\ldots,x_{d,6})\vee \neg ({\sf id}(x_{d,1})={\sf id}(x_{d,2}))))))))) \label{eqn:oddD} \end{align}\tag{11}\] where \({\sf id}(x_{d,1}), {\sf id}(x_{d,2}) \in [\lceil \log^{(d)} n \rceil]\), and \(\phi_1,\ldots,\phi_d\) are quantifier free formulas.

Now we want to replace \(({\sf id}(x_{d,1})={\sf id}(x_{d,2}))\) with an FO formula. So, we apply Lemma 26, and obtain a tree \(T'\) and \((2\log^{(d+1)} n)\)-FO formula \(\phi_{\exists}\) on two free variables with the following specifications.

(i) For any two nodes \(x_1\) and \(x_2\) in \(T_1\), \(T'\models \phi_{\exists}(x_1,x_2)\) if and only if \({\sf id}(x_1)={\sf id}(x_2)\).

(ii) All the quantifiers in \(\phi_{\exists}(x_1,x_2)\) are existential quantifiers and \(|\phi_{\exists}(x_1,x_2)|=O(\log^{(d+1)} n)\).

(iii) The number of label predicates used in \(\phi_{\exists}(x_1,x_2)\) is two.

(iv) \(V(T')=O(|V(T_1)|\cdot \log^{(d+1)}n )\)

Thus, we can replace \(\neg ({\sf id}(x_{d,1})={\sf id}(x_{d,2})))\) in the formula in (11 ) with \(\neg \phi_{\exists}(x_{d,1},x_{d,2})\). The formula \(\neg \phi_{\exists}(x_{d,1},x_{d,2})\) is of the form \(\neg \exists a_1 \ldots \exists a_{k} \phi_2\) where \(\phi_2\) is quantifier free and \(k=2\log^{(d+1)} n\). This implies that \[\neg \phi_{\exists}(x_{d,1},x_{d,2}) \equiv \forall a_1 \ldots \forall a_{k} \neg \phi_2.\]

Thus, the new formula \(\phi\) obtained from (11 ), by replacing \(\neg ({\sf id}(x_{d,1})={\sf id}(x_{d,2})))\) with \(\neg \phi_{\exists}(x_{d,1},x_{d,2})\), has the form specified in property (b) of the Lemma, after converting to prenex normal form using Proposition 23 The property (b) of Lemma 29 and item (ii) above implies that \(|\phi|=O(d+\log^{(d+1)}n)\). Property (e) of Lemma 29 and item (iii) above implies that the number of label predicates in \(\phi\) is \(4d+2\). Property (f) of Lemma 29 and item (iv) above implies the condition (f) of the lemma. This completes the proof. ◻

Proof. To prove this lemma we apply Lemma 29 followed by Lemma 27. Recall that \(d\geq 2\) is an even number. Apply Lemma 29 and obtain a tree \(T_1\) and \((c_1,\ldots,c_d)\)-FO+id formula \(\phi\) with specifications mentioned in the lemma. Since \(d\) is an even number, condition (c) in Lemma 29 implies that for any two leaf nodes \(z,y\) in \(T\), \(\phi(z,y)\) is of the form

\[\begin{align} \forall x_{1,1}, \ldots, \forall x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \vee \nonumber \\ (\exists x_{2,1}\ldots,\exists x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \wedge \nonumber\\ (\forall x_{3,1}, \ldots, \forall x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\vee \nonumber\\ \vdots && \nonumber\\ (\exists x_{d,1}, \ldots, \exists x_{d,6} && (\phi_d(x_{d-1,1},x_{d-1,2},x_{d,1},\ldots,x_{d,6})\wedge ({\sf id}(x_{d,1})={\sf id}(x_{d,2}))))))))) \label{eqn:evenD} \end{align}\tag{12}\] where \({\sf id}(x_{d,1}), {\sf id}(x_{d,2}) \in [\lceil \log^{(d)} n \rceil]\) , and \(\phi_1,\ldots,\phi_d\) are quantifier free formulas.

Now we want to replace \(({\sf id}(x_{d,1})={\sf id}(x_{d,2}))\) with an FO formula. So, we apply Lemma 26, and obtain a tree \(T'\) and \((2\log^{(d+1)} n)\)-FO formula \(\phi_{\exists}\) on two free variables with the following specifications.

(i) For any two leaf nodes \(x_1\) and \(x_2\) in \(T_1\), \(T'\models \phi_{\exists}(x_1,x_2)\) if and only if \({\sf id}(x_1)={\sf id}(x_2)\).

(ii) All the quantifiers in \(\phi_{\exists}(x_1,x_2)\) are existential quantifiers and \(|\phi_{\exists}(x_1,x_2)|=O(\log^{(d+1)} n)\).

(iii) The number of label predicates used in \(\phi_{\exists}(x_1,x_2)\) is two.

(iv) \(V(T')=O(|V(T_1)|\cdot \log^{(d+1)}n )\)

Thus, we can replace \({\sf id}(x_{d,1})={\sf id}(x_{d,2})\) in the formula in (12 ) with \(\phi_{\exists}(x_{d,1},x_{d,2})\). This new formula will be of the form specified in item (b) of the lemma, after converting to the prenex normal form. The arguments for the proof of other properties in the lemma are similar to the arguments in the proof of Lemma 30. This completes the proof. ◻

Proof. Apply Lemma 24 and obtain a tree \(T\) and an \((2\alpha+1,9)\)-FO+\({\sf id}\) formula \(\psi\). Notice that Figure 4 is an illustration of \(T\). The FO+\({ \sf id }\) formula \(\psi\) is given below.

\[\begin{align} \psi &\equiv&\exists r\in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \; \exists p_1 \; \ldots \; \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \psi_{{\sf evalid}}\wedge (\neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf id}}\vee \psi_{{\sf color}}) \label{eqn:FO1} \end{align}\tag{13}\] All the label predicates in the formula is explained in the proof of Lemma 24. In the formula \(\psi\), the subformulas \(\psi_{{\sf evalid}}, \psi_{{\sf uvalid}}\), and \(\psi_{{\sf color}}\) are quantifier free FO formulas. But \(\psi_{{\sf id}}\) contains the function sysmbol \({\sf id }\). Recall that

\[\psi_{{\sf id}}\equiv {\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2).\]

Now we explain how to get rid of the function \({\sf id}\). We have two cases, one is when \(i=2\) and the other is when \(i>2\).

Case 1: \(i=2\). In order to replace \(\psi_{\sf id}\), we apply Lemma 26 and obtain a tree \(T'\) (which is super graph of \(T\)) and \((2\log n)\)-FO formula \(\phi_{\exists}\) on two free variables with the following specifications.

(a) For any two leaf nodes \(z\) and \(y\) in \(T\), \(T'\models \phi_{\exists}(z,y)\) if and only if \({\sf id}(z)={\sf id}(y)\).

(b) All the quantifiers in \(\phi_{\exists}(z,y)\) are existential quantifiers and \(|\phi_{\exists}(z,y)|=O(\log n)\).

(c) The number of label predicates used in \(\phi_{\exists}(z,y)\) is two.

(d) \(V(T')=O(|V(T)|\cdot \log n)\)

Now we substitute \({\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2)\) with \(\phi_{\exists}(z_1,y_1) \wedge \phi_{\exists}(z_2,y_2)\) and let \(\psi'\) be the resulting formula. Equation (13 ) and the definition of \(\phi_{\exists}\) implies that \(\psi'\) is a \((2\alpha+1,9+2\log n)\)-FO formula. Property (i) of Lemma 24 and item (a) above implies that

• \(G\) is a \(3\)-colorable if and only if \(T'\) satisfies \(\psi'\).

Property (ii) of Lemma 24 and condition (d) above implies that

• \(|V(T')|=O((3^{n/\alpha}+m)\log n)\) and \(|\psi'|=O(\alpha^2+\log n)\).

Property (iii) of Lemma 24 and condition (c) above implies that

• Number of label predicates used is \(11\).

So, \(T'\) and \(\psi'\) are the required output of the theorem in this case.

Case 2: \(i>2\). In this case, to replace \(\psi_{\sf id}\), we apply Lemma 31 when \(i\) is even and apply Lemma 30 when \(i\) is odd with \(d=i-2\), and obtain a tree \(T'\) (which is super graph of \(T\)) and a \((c_1,\ldots,c_{i-2})\)-FO formula \(\phi\) on two free variables with the following specifications.

(a) \(c_q=6\) for all \(q\in [i-3]\) and \(c_{i-2}= 6+2\log^{(i-1)}n\).

(b) \(\phi(z,y)\) is of the form \[\forall x_{1,1}, \ldots, \forall x_{1,6} \exists x_{2,1}\ldots,\exists x_{2,6}, \ldots, Q x_{i-2,1}\ldots, Q x_{i-2,c_{i-2}} \;\; \phi_1(z,y)\] where \(\phi_1\) is a quantifier free formula, and \(Q=\exists\) if \(i\) is odd and \(Q=\forall\) otherwise.

(c) \(|\phi|= O(i+\log^{(i-1)} n)\).

(d) For any two leaf nodes \(z\) and \(y\) in \(T\), \(T'\models \phi_{\forall}(z,y)\) if and only if \({\sf id}(z)={\sf id}(y)\).

(e) The number of label predicates used in \(\phi(z,y)\) is \(4i-6\).

(f) \(V(T')=O(|V(T)|\cdot {\sf ilog}(n,i))\).

Now we substitute \({\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2)\) with \(\phi(z_1,y_1) \wedge \phi(z_2,y_2)\) and let \(\psi'\) be the resulting formula. Equation (13 ) and the definition of \(\phi\) implies that \(\psi'\) is a \((2\alpha+1,9, k_3,\ldots,k_{i-1},6+2\log^{(i-1)} n)\)-FO formula. Property (i) of Lemma 24 and item (d) above implies that

• \(G\) is a \(3\)-colorable if and only if \(T'\) satisfies \(\psi'\).

Property (ii) of Lemma 24 and items (c) and (f) above implies that

• \(|V(T')|=O((3^{n/\alpha}+m){\sf ilog}(n,i))\) and \(|\psi'|=O(\alpha^2+i+\log^{(i-1)} n)\).

Property (iii) of Lemma 24 and item (e) above implies that

• Number of label predicates used in \(\psi'\) is \(4i+3\).

So, \(T'\) and \(\psi'\) are the required output of the theorem in this case. This completes the proof of the theorem. ◻

Proof. First we apply Lemma 24 and obtain a tree \(T_1\) and a \((2\alpha +1,9)\)-FO+\({\sf id}\) formula \(\psi\). Notice that Figure 4 is an illustration of \(T_1\). The FO+\({ \sf id }\) formula \(\psi\) is given below.

\[\begin{align} \psi &\equiv&\exists r\in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \; \exists p_1 \; \ldots \; \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \psi_{{\sf evalid}}\wedge (\neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf id}}\vee \psi_{{\sf color}}) \label{eqn:FO1:s620:i612} \end{align}\tag{14}\] All the label predicates in the formula is explained in the proof of Lemma 24. In the formula \(\psi\), the subformulas \(\psi_{{\sf evalid}}, \psi_{{\sf uvalid}}\), and \(\psi_{{\sf color}}\) are quantifier free FO formulas. But \(\psi_{{\sf id}}\) contains the function sysmbol \({\sf id }\). Recall that

\[\psi_{{\sf id}}\equiv {\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2).\]

Let \(k'=\frac{k-14}{4}\). Now we replace each leaf node \(t\in {\sf EP}\cup {\sf I}\) with a path as explained below. We create a path \(\pi_t= a_1,\ldots,a_{k'},t\) on \(k' +1\) vertices. Now, we replace node \(t\) with path \(\pi_t\). Let \(T_2\) be the tree obtained after this process. Let \(b_1,\ldots,b_{k'}\) be the base \(2^{s}\) representation of the number \({\sf id}(t)\). Now, let us define \({\sf id}(a_i)=b_i\) for all \(i\). Moreover, we create a unary label predicate \({\sf P}_1\) and add all the vertices \(a_1,\ldots,a_{k'}\) to \({\sf P}_1\). Since \(2^{k' \cdot s} \geq n\), each number in \([n]\) can be uniquely represented as above. Now, \({\sf id}(z)={\sf id}(y)\) can be written as

\[\begin{align} \phi_{\sf yes}(z,y)\equiv \exists a_1,a_1'\in {\sf P}_1 \ldots \exists a_{k},a_{k'}' \in {\sf P}_1&& \left( \bigwedge_{i\in [k] } {\sf id}(a_i) = {\sf id}(a'_i) \right) \nonumber \\ && \wedge {\sf path}(a_1,\ldots,a_{k'},z) \wedge {\sf path}(a'_1,\ldots,a'_{k'},y) \label{eqn:exuni1} \end{align}\tag{15}\]

where, \({\sf path}(w_1,\ldots,w_q) \equiv (\bigwedge_{i\in [q-1]} {\sf adj}(w_i,w_{i+1}))\). Now, \(\neg \psi_{{\sf id}}\) can be expressed as

\[\begin{align} \neg \psi_{\sf id}\equiv \forall a_1,a_1'\in {\sf P}_1 \ldots \forall a_{k'},a_{k'}' \in {\sf P}_1 && \left( \bigvee_{i\in [k'] } {\sf id}(a_i) \neq {\sf id}(a'_i) \right) \nonumber \\ && \vee \neg {\sf path}(a_1,\ldots,a_{k'},z_1) \vee \neg {\sf path}(a'_1,\ldots,a'_{k'},y_1) \vee \nonumber \\ \forall d_1,d_1'\in {\sf P}_1 \ldots \forall d_{k'},d_{k'}' \in {\sf P}_1 && \left( \bigvee_{i\in [k'] } {\sf id}(d_i) \neq {\sf id}(d'_i) \right) \nonumber \\ && \vee \neg {\sf path}(d_1,\ldots,d_{k'},z_2) \vee \neg {\sf path}(d'_1,\ldots,d'_{k'},y_2) \nonumber \end{align}\] The above formula can be rewritten as \[\begin{align} \neg \psi_{\sf id} &\equiv& \forall a_1,a_1'\in {\sf P}_1 \ldots \forall a_{k'},a_{k'}' \in {\sf P}_1 \forall d_1,d_1'\in {\sf P}_1 \ldots \forall d_{k'},d_{k'}' \in {\sf P}_1 \nonumber \\ && \psi_{\sf npath} \vee \bigvee_{i\in [k'] } {\sf id}(a_i) \neq {\sf id}(a'_i) \vee \bigvee_{i\in [k'] } {\sf id}(d_i) \neq {\sf id}(d'_i), \nonumber \end{align}\]

where \(\psi_{\sf npath}\) is the formula \[\neg {\sf path}(a_1,\ldots,a_{k'},z_1) \vee \neg {\sf path}(a'_1,\ldots,a'_{k'},y_1) \vee \neg {\sf path}(d_1,\ldots,d_{k'},z_2) \vee \neg {\sf path}(d'_1,\ldots,d'_{k'},y_2)\] Now, (14 ) can be written as

\[\begin{align} \psi &\equiv& \exists r\in {\sf R}\; \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P}\; \exists p_1 \ldots \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \forall a_1,a_1'\in {\sf P}_1 \ldots \forall a_{k'},a_{k'}' \in {\sf P}_1 \forall d_1,d_1'\in {\sf P}_1 \ldots \forall d_{k'},d_{k'}' \in {\sf P}_1 \nonumber\\ && \psi_{{\sf evalid}} \wedge \left( (\neg \psi_{{\sf uvalid}} \vee \psi_{{\sf npath}}\vee \psi_{{\sf color}}) \vee \bigvee_{i\in [k'] } {\sf id}(a_i) \neq {\sf id}(a'_i) \vee \bigvee_{i\in [k'] } {\sf id}(d_i) \neq {\sf id}(d'_i)\right) \label{eqn:FO2:s620:i612} \end{align}\tag{16}\]

The length of formula in (16 ) is \(O(\alpha^2+k)\). In the above expression each \({\sf id}(a_i)\) is a number in \(\{0,\ldots,2^s-1\}\). Now we explain how to encode \({\sf id}(a_i) = {\sf id}(a'_i)\). Notice that we can use \(s\) set variables \(W_1,\ldots,W_s\) in the fomula. Also, we know the value of \({\sf id}(a_i)\) and \({\sf id}(a_{i'})\). Let \(b_1,\ldots,b_s\) be the binary representation of \({\sf id}(a_i)\) and \(b'_1,\ldots,b'_s\) be the binary representation of \({\sf id}(a'_i)\). Suppose we are able to force the set variables in such a way that for all \(j\in [s]\), \(a_i\in W_j\) if and only if \(b_j=1\) and \(a_i'\in W_j\) if and only if \(b'_j=1\). Under that condition, \({\sf id}(a_i) \neq {\sf id}(a'_i)\) can be encoded as

\[\label{eqn:setQIDcore} \neg \bigwedge_{j\in [s]} (a_i\in W_j) \Leftrightarrow (a'_i\in W_j)\tag{17}\]

Now to satisfy the condition mentioned above, we create a formula \(\psi_{\sf set}(W_1,\ldots W_s)\) such that \(\psi_{\sf set}(W_1,\ldots W_s)\) is true if and only if the following is true. For any vertex \(a\in {\sf P}_1\), let \(b_1,\ldots,b_s\) be the binary representation of \({\sf id}(a)\). Then, the formula \(\psi_{\sf set}(W_1,\ldots W_s)\) is true if and only if for all \(a\in P_1\) and \(j\in [s]\), \(a\in W_j\) only when \(b_j=1\). Once we have such a formula \(\psi_{\sf set}(W_1,\ldots W_s)\), we can rewrite (16 ) as follows.

\[\begin{align} \psi &\equiv& \exists W_1\ldots \exists W_s \exists r\in {\sf R} \exists x_1\in {\sf P}\; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \; \exists p_1 \ldots \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \forall a_1,a_1'\in {\sf P}_1 \ldots \forall a_{k'},a_{k'}' \in {\sf P}_1 \forall d_1,d_1'\in {\sf P}_1 \ldots \forall d_{k'},d_{k'}' \in {\sf P}_1 \nonumber\\ && \psi_{\sf set}(W_1,\ldots, W_s) \wedge \psi_{{\sf evalid}} \wedge \Big( (\neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf npath}}\vee \psi_{{\sf color}}) \vee \nonumber\\ && \bigvee_{i\in [k'] } \left(\neg \bigwedge_{j\in [s]} (a_i\in W_j) \Leftrightarrow (a'_i\in W_j)\right) \vee \bigvee_{i\in [k'] } \left( \neg \bigwedge_{j\in [s]} (d_i\in W_j) \Leftrightarrow (d'_i\in W_j) \right)\Big) \label{eqn:FO3:s620:i612} \end{align}\tag{18}\]

Now, to define the formula \(\psi_{\sf set}(W_1,\ldots,W_k)\), we create two label predicates \({\sf SP}_1\) and \({\sf SP}_2\). For each \(a\in P_1\), we know that \({\sf id}(a)\in \{0,\ldots 2^s-1\}\). Let \(c'={\sf id}(a)\). We replace \(a\) with a path \(\sigma_a=q_0,q_1,\ldots,q_{c'},a\). Let \(T_3\) be the tree obtained after this process. We add \(q_0\) to \({\sf SP}_1\) and for all \(j\in [c']\), \(q_j\) to \({\sf SP}_2\). Now, let us define \({\sf id}\) for the newly introduced vertices \(q_0,q_1,\ldots,q_{c'}\). Let \({\sf id}(q_j)=j\) for all \(j\in [c']\). Notice that \({\sf id}\) values of \(q_0,\ldots,q_{c'},a\) are \(0,1,2,\ldots,c'-1,c',c'\). To encode this, we will encode that

• for all \(u\in {\sf SP}_1\), \({\sf id}(u)=0\),

• for all \(u\in {\sf SP}_1\cup {\sf SP}_2\) and for all \(v\in {\sf SP}_2\), \({\sf adj}(u,v)\) implies that for all \(c\in [2^{s}-2] ({\sf id}(u)=c \Rightarrow {\sf id}(v)=c+1) \vee ({\sf id}(v)=c \Rightarrow {\sf id}(u)=c+1)\)
  

• for all \(u\in {\sf SP}_1\cup {\sf SP}_2\) and for all \(v\in {\sf P}_1\), \({\sf adj}(u,v)\) implies that for all \(c\in [2^{s}-1] ({\sf id}(u)=c \Rightarrow {\sf id}(v)=c)\)

We encode (i) as follows.

\[\begin{align} \phi_{(i)}&\equiv& \forall u_1\in {\sf SP}_1, \bigwedge_{j\in [s]} \neg (u_1\in W_j) \end{align}\]

To encode condition (ii), we need to encode that for a number \(c\in [2^{s}-1]\), \({\sf id}(u)=c \Rightarrow {\sf id}(v)=c+1\). Fix \(u\), and \(c\). Let \(d_1,\ldots,d_s\) be the binary representation of \(c\). Let \(D\subseteq [s]\) such that \(i\in D\) if and only if \(d_i=1\). Let

\[\begin{align} \phi_{\sf eq}(u,c)\equiv {\sf id}(u)=c &\equiv & \bigwedge_{i\in D} u\in W_i \wedge \bigwedge_{j\in [s]\setminus D} \neg (u\in W_j) \end{align}\] Now, we can encode condition (ii) as

\[\begin{align} \phi_{(ii)}\equiv && \forall u_2\in {\sf SP}_1\cup {\sf SP}_2, \forall v_2\in {\sf SP}_2 \\ && {\sf adj}(u_2,v_2) \Rightarrow \bigwedge_{c\in [2^s-1]} ((\phi_{\sf eq}(u_2,c)\Rightarrow \phi_{\sf eq}(v_2,c+1)) \vee (\phi_1(v_2,c)\Rightarrow \phi_1(u_2,c+1))) \end{align}\]

Similarly, we can encode (iii) as

\[\begin{align} \phi_{(iii)}\equiv \forall u_3\in {\sf SP}_1\cup {\sf SP}_2, \forall v_3\in {\sf P}_1 && {\sf adj}(u_3,v_3) \Rightarrow \bigwedge_{c\in [2^s-1]} (\phi_{\sf eq}(u_3,c)\Rightarrow \phi_{\sf eq}(v_3,c)) \end{align}\]

Thus, finally, we have \(\psi_{\sf set}(W_1,\ldots,W_k)= \phi_{(i)} \wedge \phi_{(ii)} \wedge \phi_{(iii)}\), and its length is \(O(2^s)\). Let \(\phi_{\sf set}\) be the formula obtained from \(\phi_{(i)} \wedge \phi_{(ii)} \wedge \phi_{(iii)}\) by removing the quantifiers. Then, \[\begin{align} \label{eqn:psiset} \psi_{\sf set}(W_1,\ldots,W_s) \equiv \forall u_1\in {\sf SP}_1 \forall u_2,u_3\in {\sf SP}_1\cup {\sf SP}_2 \forall v_2 \in {\sf SP}_2 \forall v_3\in {\sf P}_1 \;\; \phi_{\sf set} \end{align}\tag{19}\]

By substituting the above formula for \(\psi_{\sf set}(W_1,\ldots,W_s)\) in (18 ) we get an \(((2\alpha+1,s),(4k'+14,0))\)-MSO formula of length \(O(\alpha^2+k+2^s)\). By the construction of the tree and formula \(\psi\), property (i) of the theorem follows. Lemma 24 introduces \(9\) label predicates. We have also introduced \(3\) additional label predicates \({\sf P}_1\), \({\sf SP}_1\) and \({\sf SP}_2\). This implies that the number of label predicates in \(\psi\) is \(12\). The number of vertices in \(T_3\) is \(O(V(T_1)2^s \log k)= O((3^{n/\alpha}+m)2^s\log k)\). ◻

Proof. We apply Lemma 29 and we get a tree \(T_1\) which is a super graph of \(T\) and a \((c_1,\ldots,c_d)\)-FO+id formula \(\phi\) with the following properties.

(a) \(c_i=6\) for all \(i\in [d]\).

(b) If \(d\) is odd, then \(\phi(z,y)\) is of the form \[\begin{align} \forall x_{1,1}, \ldots, \forall x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \vee \\ (\exists x_{2,1}\ldots,\exists x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \wedge \\ (\forall x_{3,1}, \ldots, \forall x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\vee \\ \vdots && \\ (\forall x_{d,1}, \ldots, \forall x_{d,6} && (\phi_d(x_{d-1,1},x_{d-1,2},x_{d,1},\ldots,x_{d,6})\vee \neg ({\sf id}(x_{d,1})={\sf id}(x_{d,2}))))))))) \end{align}\] where \({\sf id}(x_{d,1}), {\sf id}(x_{d,2}) \in [\lceil \log^{(d)} n \rceil],\) and \(\phi_1,\ldots,\phi_{d}\) are quantifier free formulas.

(c) If \(d\) is even, then \(\phi(z,y)\) is of the form \[\begin{align} \forall x_{1,1}, \ldots, \forall x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \vee \\ (\exists x_{2,1}\ldots,\exists x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \wedge \\ (\forall x_{3,1}, \ldots, \forall x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\vee \\ \vdots && \\ (\exists x_{d,1}, \ldots, \exists x_{d,6} && (\phi_d(x_{d-1,1},x_{d-1,2},x_{d,1},\ldots,x_{d,6})\wedge ({\sf id}(x_{d,1})={\sf id}(x_{d,2}))))))))) \end{align}\] where \({\sf id}(x_{d,1}), {\sf id}(x_{d,2}) \in [\lceil \log^{(d)} n \rceil]\) , and \(\phi_1,\ldots,\phi_{d}\) are quantifier free formulas.

(d) For any two leaf nodes \(z\) and \(y\) in \(T\), \(T_1\models \phi(z,y)\) if and only if \({\sf id}(z)={\sf id}(y)\)

(e) The number of label predicates used in \(\phi(z,y)\) is \(4d\).

(f) \(V(T_1)=O(|V(T)|\cdot {\sf ilog}(n,d))\)

Now, to encode \({\sf id}(x_{d,1})={\sf id}(x_{d,2})\) we use set variables like in Theorem 15. Let \(k'=\frac{k-6}{2}\). Now we replace each leaf node \(t\) in \(T_1\) (where \({\sf id}(t)\) is defined) with a path as explained below. We create a path \(\pi_t= a_1,\ldots,a_{k'},t\) on \(k' +1\) vertices. Now, we replace node \(t\) with path \(\pi_t\). Let \(T_2\) be the tree obtained after this process. Let \(b_1,\ldots,b_{k'}\) be the base \(2^{s}\) representation of the number \({\sf id}(t)\). Now, let us define \({\sf id}(a_i)=b_i\) for all \(i\). Moreover, we create a unary label predicate \({\sf P}_1\) and add all the vertices \(a_1,\ldots,a_{k'}\) to \({\sf P}_1\). Since \(2^{k' \cdot s} \geq \log^{(d)} n\), each number in \([\log^{(d)} n]\) can be uniquely represented as above. Now, \({\sf id}(x_{d,1})={\sf id}(x_{d,2})\) can be written as

\[\begin{align} \exists a_1,a_1'\in {\sf P}_1 \ldots \exists a_{k},a_{k'}' \in {\sf P}_1\left( \bigwedge_{i\in [k] } {\sf id}(a_i) = {\sf id}(a'_i) \right) \wedge {\sf path}(a_1,\ldots,a_{k'},x_{d,1}) \wedge {\sf path}(a'_1,\ldots,a'_{k'},x_{d,2}) \nonumber \end{align}\]

where, \({\sf path}(w_1,\ldots,w_q) \equiv (\bigwedge_{i\in [q-1]} {\sf adj}(w_i,w_{i+1}))\). As before, we want to encode the identifiers using these set variables. Now, we introduce \(s\) set variables \(W_1,\ldots,W_s\). Let \(b_1,\ldots,b_s\) be the binary representation of \({\sf id}(a_i)\) and \(b'_1,\ldots,b'_s\) be the binary representation of \({\sf id}(a_i')\). Suppose we are able to force the set variables in such a way that for all \(j\in [s]\), \(a_i\in W_j\) if and only if \(b_j=1\) and \(x_{d,2}\in W_j\) if and only if \(b'_j=1\). Under that condition, \({\sf id}(x_{a_i}) = {\sf id}({a_i'})\) can be encoded as

\[\bigwedge_{j\in [s]} (a_i\in W_j) \Leftrightarrow (a'_i\in W_j)\]

In other words, we define a formula \(\phi_{\sf yes}(x_{d,1},x_{d,2},W_1,\ldots,W_s)\) on two free vertex variables and \(s\) free set variables as follows.

\[\begin{align} \phi_{\sf yes}(x_{d,1},x_{d,2},W_1,\ldots,W_s)&\equiv& \exists a_1,a_1'\in {\sf P}_1 \ldots \exists a_{k},a_{k'}' \in {\sf P}_1 \nonumber \\ && {\sf path}(a_1,\ldots,a_{k'},x_{d,1}) \wedge {\sf path}(a'_1,\ldots,a'_{k'},x_{d,2}) \wedge \nonumber\\ && \left( \bigwedge_{i\in [k] } \bigwedge_{j\in [s]} (a_i\in W_j) \Leftrightarrow (a'_i\in W_j) \right) \label{eqn:exuni1leveld2} \end{align}\tag{20}\]

Assuming the set variables are properly selected, \(\phi_{\sf yes}(x_{d,1},x_{d,2},W_1,\ldots,W_s)\) is true if and only if \({\sf id}(x_{d,1})={\sf id}(x_{d,2})\). Now substitute (20 ) in the formula \(\phi(z,y)\) (see items (b) and (c)) and let the resulting formula be \(\psi_1(z,y,W_1,\ldots,W_s)\). Notice that \(\psi_1(z,y,W_1,\ldots,W_s)\) is a \((c_1,\ldots,c_{d-1},c_d+2k')\)-MSO formula with \(s\) free set variables and \(2\) free vertex variables, where \(c_i=6\) for all \(i\in [d]\). Then, like in the case of Theorem 15, we add long paths to vertices for which id is defined and define \(\psi_{set}\) on free variables \(W_1,\ldots,W_s\) and it looks like

\[\begin{align} \label{eqn:psiset:aux} \psi_{\sf set}(W_1,\ldots,W_s) \equiv \forall u_1\in {\sf SP}_1 \forall u_2,u_3\in {\sf SP}_1\cup {\sf SP}_2 \forall v_2 \in {\sf SP}_2 \forall v_3\in {\sf P}_1 \;\; \phi_{\sf set} \end{align}\tag{21}\]

Let \(T'\) be the tree obtained after this process. Here, \(\phi_{\sf set}\) is quantifier free formula and the only free variables in \(\phi_{\sf set}\) are \(W_1,\ldots,W_s,u_1,u_2,u_3\). Moreover, \(\psi_{\sf set}(W_1,\ldots,W_s)\) is true if and only if for each vertex, its inclusion in these sets is according to the id of the vertex. Notice that \(\psi_{\sf set}(W_1,\ldots,W_s)\) is a \((5)\)-MSO formula.

Now, the required formula \(\psi(z,y)\) is defined as \[\exists W_1,\ldots,\exists W_s \; \psi_{\sf set}(W_1,\ldots,W_s) \wedge \psi_1(z,y,W_1,\ldots,W_s)\]

Similarly, the required formula \(\psi'\) is

\[\forall W_1,\ldots, \forall W_s \;\; \psi_{\sf set}(W_1,\ldots,W_s) \Rightarrow \psi_1(z,y,W_1,\ldots,W_s)\] The definitions of \(\psi_1, \psi_{\sf set}\) and \(\phi\) implies that \(\psi\) and \(\psi'\) are \(((c_0,s_0),\ldots,(c_d,s_d))\)-MSO formulas. The size of the formula \(\phi\) is \(O(d)\). This and (20 ) implies that \(|\psi_1|=O(d+k)\). The length of \(\psi_{\sf set}\) is \(O(2^s)\). Therefore \(|\psi|\) and \(|\psi'|\) are upper bounded by \(O(2^s+k+d)\). The fact that \(V(T_1)=O(|V(T)|\cdot {\sf ilog}(n,d))\), and the construction of the tree implies that \(V(T')=O(|V(T)|\cdot 2^s k \cdot {\sf ilog}(n,d))\) This completes the proof of the lemma. ◻

Proof. Like before, we start applying Lemma 24 and obtain a tree \(T_1\) and an \((2\alpha+1,9)\)-FO+\({\sf id}\) formula \(\psi\). The FO+\({\sf id }\) formula \(\psi\) is given below.

\[\begin{align} \psi &\equiv&\exists r\in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \; \exists p_1 \; \ldots \; \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \psi_{{\sf evalid}}\wedge (\neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf id}}\vee \psi_{{\sf color}}) \label{eqn:FO1:s620:i622} \end{align}\tag{22}\] All the label predicates in the formula is explained in the proof of Lemma 24. In the formula \(\psi\), the subformulas \(\psi_{{\sf evalid}}, \psi_{{\sf uvalid}}\), and \(\psi_{{\sf color}}\) are quantifier free FO formulas. But \(\psi_{{\sf id}}\) contains the function sysmbol \({\sf id }\). Recall that

\[\psi_{{\sf id}}\equiv {\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2).\]

We know that \(i>2\) and \({\sf id}(z_1),{\sf id}(y_1), {\sf id}(z_2), {\sf id}(y_2) \in [n]\).

Case 1: \(j>1\). We apply Lemma 29 where \(d=j-2\) and we get a tree \(T_2\) which is a super graph of \(T_1\), and \((c_3,\ldots,c_j)\)-FO+id formula \(\phi\) with the following properties. Since we want to substitute for \(\neg\psi_{\sf id}\) in (22 ), we negated the formulas in (b) and (c).

(a) \(c_q=6\) for all \(q\in \{3,\ldots,j\}\).

(b) If \(j-2\) is odd, then \(\neg \phi(z,y)\) is of the form \[\begin{align} \exists x_{1,1}, \ldots, \exists x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \wedge \\ (\forall x_{2,1}\ldots,\forall x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \vee \\ (\exists x_{3,1}, \ldots, \exists x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\wedge \\ \vdots && \\ (\exists x_{j-2,1}, \ldots, \exists x_{j-2,6} && (\phi_{j-2}(x_{j-3,1},x_{j-3,2},x_{j-2,1},\ldots,x_{j-2,6})\wedge ({\sf id}(x_{j-2,1})={\sf id}(x_{j-2,2}))))))))) \end{align}\] where \({\sf id}(x_{j-2,1}), {\sf id}(x_{j-2,2}) \in [\lceil \log^{(j-2)} n \rceil],\) and \(\phi_1,\ldots,\phi_{j-2}\) are quantifier free formulas.

(c) If \(j-2\) is even, then \(\neg \phi(z,y)\) is of the form \[\begin{align} \exists x_{1,1}, \ldots, \exists x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \wedge \\ (\forall x_{2,1}\ldots,\forall x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \vee \\ (\exists x_{3,1}, \ldots, \exists x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\wedge \\ \vdots && \\ (\forall x_{j-2,1}, \ldots, \forall x_{j-2,6} && (\phi_{j-2}(x_{j-3,1},x_{j-3,2},x_{j-2,1},\ldots,x_{j-2,6})\vee ({\sf id}(x_{j-2,1})\neq {\sf id}(x_{j-2,2}))))))))) \end{align}\] where \({\sf id}(x_{j-2,1}), {\sf id}(x_{j-2,2}) \in [\lceil \log^{(j-2)} n \rceil]\), and \(\phi_1,\ldots,\phi_{j-2}\) are quantifier free formulas.

(d) For any two f nodes \(z\) and \(y\) in \(T_1\), \(T_2\models \neg \phi(z,y)\) if and only if \({\sf id}(z)\neq {\sf id}(y)\).

(e) The number of label predicates used in \(\phi(z,y)\) is \(4j-8\).

(f) \(V(T_2)=O(|V(T_1)|\cdot {\sf ilog}(n,j-2))\)

The formula \(\neg \phi (z,y)\) contains exactly one subformula that uses the function sysmbol \({\sf id}\) and it is of the form \({\sf id}(x_{j-2,1})\neq {\sf id}(x_{j-2,2})\) when \(j\) is even and \({\sf id}(x_{j-2,1})= {\sf id}(x_{j-2,2})\) when \(j\) is odd. Notice that in the base case when \(j=2\), \(\neg \phi (z,y)\equiv {\sf id}(z)\neq {\sf id}(y)\). Each id is a non-negative integer which is at most \(\lceil \log^{(j-2)} n \rceil\). Since, \(n \leq \exp^{(i-1)}(\frac{k-6}{2}\cdot s)\), we have

\[\log^{j-2} n \leq \exp^{((i-1)-(j-2))}(\frac{k-6}{2}\cdot s) =\exp^{(i-j+1)}(\frac{k-6}{2}\cdot s)\]

Now to replace \({\sf id}(x_{j-2,1})= {\sf id}(x_{j-2,2})\), we apply Lemma 32 with \(d=i-j\) and the id values are at most \(\lceil \log^{(j-2)} n \rceil\). Thus, by Lemma 32, we get a tree \(T_3\) (which is a super graph of \(T_2\)) and \(((c'_j,s'_j),\ldots,(c'_{i},s'_i))\)-MSO formulas \(\psi_{\sf sec}\) on two free variables with the following specifications.

(i) \(c_q= 6\) for all \(q\in \{j,\ldots,i-1\}\), \(c_{i}=k\), \(s'_j=s\) and \(s'_q=0\) for all \(q\in \{j+1,\ldots,i\}\).

(ii) All the set variables are quantified with existential quantifier in \(\psi_{\sf sec}\).

(iii) For any two nodes \(a\) and \(b\) in \(T_2\), \(T_3\models \psi_{\sf sec}(a,b)\) if and only if \({\sf id}(a)={\sf id}(b)\).

(iv) \(|\psi_{\sf sec}|\in O(i-j+k+2^s)\)

(v) The number of label predicates used in \(\psi_{\sf sec}\) and \(\psi'_{\sf sec}\) are \(4(i-j)+2\).

(vi) \(V(T_3)=O(|V(T_2)|\cdot 2^s k \cdot {\sf ilog}(\log^{j-2} n,i-j+1))\).

We substitute \(\psi_{\sf sec}(x_{j-2,1}, x_{j-2,2})\) for \({\sf id}(x_{j-2,1})= {\sf id}(x_{j-2,2}\) in \(\neg \phi(z,y)\). In either case (i.e., when \(j\) is odd or even), the resulting formula (let us call it \(\neg \phi_{\sf sub}(z,y)\)) is a \(((c_3,s_3),\ldots,(c_{j-1},s_{j-1}),(c_j+c_j',s_j'),(c_{j+1}',s_{j+1'}))\)-MSO formula. Finally, we substitute \(\neg \psi_{\sf id}\) in (22 ) with \(\neg \phi_{\sf sub}(z_1,y_1)\vee \neg \phi_{\sf sub}(z_2,y_2)\) to obtain the required formula \(\psi\). The required tree in the theorem is \(T_3\).

By Lemma 24, we know that \(|V(T_1)| = O(3^{n/\alpha}+m)\). Since \(V(T_2)=O(|V(T_1)|\cdot {\sf ilog}(n,j-2))\) (see item (f) above), \(V(T_2)=O((3^{n/\alpha}+m)\cdot {\sf ilog}(n,j-2))\). So, by item (vi) above, \(V(T_3)=O((3^{n/\alpha}+m)\cdot 2^sk \cdot {\sf ilog}(n,i-1))\). This proved property (ii) of the theorem.

The length of the formula is (22 ) is \(O(\alpha^2)\). The size of the formulas mentioned in items (b) and (c) above, are \(O(j)\). The length of the formula \(\psi_{\sf sec}\) is \(O(i-j+k+2^s)\). Thus, the length of the final formula \(\psi\) is \(O(\alpha^2+i+k+2^s)=O(\alpha^2+k+2^s)\).

The number of label predicates used in (22 ) is \(9\). This, along with items \((e)\) and (v) implies that the total number of label predicates used in the final formula is \(4i+3\).

Case 2: \(j=1\). In this case we apply Lemma 29 where \(d=i-2\). Then, use set variables to encode id. This part of the proof follows arguments similar to Theorem 15. This completes the proof of the theorem. ◻

Proof sketch of Theorem 12. Let \(s=\min\{k,t\}\). We apply Theorem 11 with \(k=k'\) and get a tree \(T_1\) and an \(S\)-MSO formula \(\phi\) for \(S = ((k_1,s_1),\dots,(k_d,s_d))\) in time \(O(3^{n/\alpha})\), with the following properties.

(1) \(G\) is a \(3\)-colorable if and only if \(T\) satisfies \(\phi\).

(2) \(|V(T)| = O(3^{n/\alpha})\) and \(|\phi| = O(2^{s}+k+\alpha^2)\).

(3) \(k_i = k\), \(k_1 = O(\alpha)\), \(k_{i'} = O(1)\) for all \(i' \in \{2,\dots,i-1\}\), and \(k_{i'} = 0\) for all \(i' \in [d] \backslash [i]\).

(4) \(s_j = s\) and \(s_{j'} = 0\) for all \(j' \in [d] \backslash \{j\}\).

(5) The number of label predicates used in \(\phi\) is \(O(1)\)

Recall that, in the proof of Theorem 11, the set variables \(W_1,\ldots,W_s\) are used to encode id of nodes where each id is an integer in \(\{0,\ldots,2^s-1\}\). Now instead of using set variables, we add \(s\) new nodes \(\{t_1,\ldots,t_s\}\) to \(T\) and all those verices are labeled with \({\sf L}\). Recall the role of set variables in \(\phi\). For two node \(u\) and \(v\) in \(T\), \({\sf id}(u)={\sf id}(v)\) is encoded by

\[\bigwedge_{i'\in [s]} (u\in W_{i'}) \Leftrightarrow (v\in W_{i'}).\]

Now, to get rid of set variables, we add edges between \(\{t_1,\ldots,t_s\}\) and nodes in \(T\) for which \({\sf id}\) is defined as follows. Let \(x\) be a node in \(T\) and \(b_1,\ldots,b_s\) be the binary representation of \({\sf id}(x)\). Then, \(x\) is adjacent to \(t_r\) if and only if \(b_r=1\). This completes the construction of the tree \(T\). Clearly, the treewidth of \(T\) is at most \(s\).

Now we explain the change in the formula. Let \(u\) and \(v\) be two nodes in \(T\). Let \(a_1,\ldots,a_s\) be the binary representation of \({\sf id}(u)\) and \(b_1,\ldots,b_s\) be the binary representation of \({\sf id}(v)\). Then \({\sf id}(u)={\sf id}(v)\) is encoded by

\[\bigwedge_{i'\in [s]} ({\sf adj}(u,t_{i'})) \Leftrightarrow ({\sf adj}(v,t_{i'}).\]

Now to covert the formula \(\phi\) to an FO formula, we replace the set variable \(W_r\) with vertex variable \(w_r\in {\sf L}\) and subformulas of the form \((u\in W_{i'}) \Leftrightarrow (v\in W_{i'})\) with \(({\sf adj}(u,t_{i'}) \Leftrightarrow ({\sf adj}(v,t_{i'})\). The resulting formula satisfies the properties mentioned in Theorem 12. Notice that we have introduced one new label predicate and hence the number of label predicates used in the new formula is \(O(1)\) only. ◻

Proof of Theorem 13. Apply Lemma 24 and obtain a tree \(T\) and an \((2\alpha+1,9)\)-FO+\({\sf id}\) formula \(\psi\). Notice that Figure 4 is an illustration of \(T\). The FO+\({ \sf id }\) formula \(\psi\) is given below.

\[\begin{align} \psi &\equiv&\exists r\in {\sf R} \exists x_1\in {\sf P} \; \exists x_2 \in {\sf P}\; \ldots \; \exists x_{\alpha}\in {\sf P} \; \exists p_1 \; \ldots \; \exists p_{\alpha} \nonumber\\ && \forall z \in {\sf EN}\; \forall z_1, z_2 \in {\sf EP}\; \forall v_1, v_2 \in {\sf N} \; \forall y_1, y_2 \in {\sf I} \; \forall c_1,c_2 \in {\sf Q} _1\cup {\sf Q}_2 \cup {\sf Q}_3 \nonumber\\ && \psi_{{\sf evalid}}\wedge (\neg \psi_{{\sf uvalid}} \vee \neg\psi_{{\sf id}}\vee \psi_{{\sf color}}) \label{eqn:MSO-TW22-1} \end{align}\tag{23}\]

All the label predicates in the formula is explained in the proof of Lemma 24. In the formula \(\psi\), the subformulas \(\psi_{{\sf evalid}}, \psi_{{\sf uvalid}}\), and \(\psi_{{\sf color}}\) are quantifier free FO formulas. But \(\psi_{{\sf id}}\) contains the function sysmbol \({\sf id }\). Recall that

\[\psi_{{\sf id}}\equiv {\sf id}(z_1)={\sf id}(y_1)\wedge {\sf id}(z_2)={\sf id}(y_2).\]

Now we explain how to get rid of the function \({\sf id}\). Notice that \({\sf id}(y)\in [n]\) for any node \(y\) and \(i\geq 2\). We apply Lemma 29 where \(d=i-2\) and we get a tree \(T_1\) which is a super graph of \(T\), and \((c_3,\ldots,c_i)\)-FO+id formula \(\phi\) with the following properties. Since we want to substitute for \(\neg\psi_{\sf id}\) in (23 ), we negated the formulas in (b) and (c).

(a) \(c_q=6\) for all \(q\in \{3,\ldots,i\}\).

(b) If \(i-2\) is odd, then \(\neg \phi(z,y)\) is of the form \[\begin{align} \exists x_{1,1}, \ldots, \exists x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \wedge \\ (\forall x_{2,1}\ldots,\forall x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \vee \\ (\exists x_{3,1}, \ldots, \exists x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\wedge \\ \vdots && \\ (\exists x_{i-2,1}, \ldots, \exists x_{i-2,6} && (\phi_{i-2}(x_{i-3,1},x_{i-3,2},x_{i-2,1},\ldots,x_{i-2,6})\wedge ({\sf id}(x_{i-2,1})={\sf id}(x_{i-2,2}))))))))) \end{align}\] where \({\sf id}(x_{i-2,1}), {\sf id}(x_{i-2,2}) \in [\lceil \log^{(i-2)} n \rceil],\) and \(\phi_1,\ldots,\phi_{j-2}\) are quantifier free formulas.

(c) If \(i-2\) is even, then \(\neg \phi(z,y)\) is of the form \[\begin{align} \exists x_{1,1}, \ldots, \exists x_{1,6} && ( \phi_1(z,y, x_{1,1},\ldots,x_{1,6}) \wedge \\ (\forall x_{2,1}\ldots,\forall x_{2,6} && ( \phi_2(x_{1,1},x_{1,2},x_{2,1},\ldots,x_{2,6}) \vee \\ (\exists x_{3,1}, \ldots, \exists x_{3,6} && (\phi_3(x_{2,1},x_{2,2},x_{3,1},\ldots,x_{3,6})\wedge \\ \vdots && \\ (\forall x_{i-2,1}, \ldots, \forall x_{i-2,6} && (\phi_{i-2}(x_{i-3,1},x_{i-3,2},x_{i-2,1},\ldots,x_{i-2,6})\vee ({\sf id}(x_{i-2,1})\neq {\sf id}(x_{i-2,2}))))))))) \end{align}\] where \({\sf id}(x_{i-2,1}), {\sf id}(x_{i-2,2}) \in [\lceil \log^{(i-2)} n \rceil]\), and \(\phi_1,\ldots,\phi_{j-2}\) are quantifier free formulas.

(d) For any two nodes \(z\) and \(y\) in \(T\), \(T_1\models \neg \phi(z,y)\) if and only if \({\sf id}(z)\neq {\sf id}(y)\).

(e) The number of label predicates used in \(\phi(z,y)\) is \(4i-8\).

(f) \(V(T_1)=O(|V(T)|\cdot {\sf ilog}(n,i-2))\)

The formula \(\neg \phi (z,y)\) contains exactly one subformula that uses the function sysmbol \({\sf id}\) and it is of the form \({\sf id}(x_{i-2,1})\neq {\sf id}(x_{i-2,2})\) when \(i\) is even and \({\sf id}(x_{i-2,1})= {\sf id}(x_{i-2,2})\) when \(j\) is odd. Notice that in the base case when \(i=2\), \(T_1=T\) and \(\neg \phi (z,y)\equiv {\sf id}(z)\neq {\sf id}(y)\). That is, when \(i=2\), we do not apply Lemma 29. Each id is a non-negative integer which is at most \(\lceil \log^{(i-2)} n \rceil\). Since, \(n \leq \exp^{(i-1)}(\frac{k-6}{3}\cdot \log t)\), we have

\[\log^{i-2} n \leq 2^{(\frac{k-6}{3}\cdot \log t)} =t^{\frac{k-6}{2}}.\]

Now, we want to encode \({\sf id}(x_{i-2,1})={\sf id}(x_{i-2,2})\) where these id values are at most \(\lceil \log^{(i-2)} n \rceil\). Let \(k'=\frac{k-6}{3}\). Now we replace each node \(w\) in \(T_1\) (where \({\sf id}(w)\) is defined) with a path as explained below. We create a path \(\pi_w= a_1,\ldots,a_{k'},w\) on \(k' +1\) vertices. Now, we replace node \(w\) with path \(\pi_w\). Let \(T_2\) be the tree obtained after this process. Let \(b_1,\ldots,b_{k'}\) be the base \(t\) representation of the number \({\sf id}(w)\). Now, let us define \({\sf id}(a_j)=b_j \in \{0,\ldots,t-1\}\) for all \(j\in [k']\). Moreover, we create a unary label predicate \({\sf P}_1\) and add all the vertices \(a_1,\ldots,a_{k'}\) to \({\sf P}_1\). Since \(t^{k'} \geq \log^{(i-2)} n\), each number in \([\log^{(i-1)} n]\) can be uniquely represented as above. Now, \({\sf id}(x_{i-2,1})={\sf id}(x_{i-2,2})\) can be written as

\[\begin{align} \exists a_1,a_1'\in {\sf P}_1 \ldots \exists a_{k'},a_{k'}' \in {\sf P}_1 && {\sf path}(a_1,\ldots,a_{k'},x_{i-2,1}) \wedge {\sf path}(a'_1,\ldots,a'_{k'},x_{i-2,2}) \wedge \nonumber \\ && \left( \bigwedge_{j\in [k'] } {\sf id}(a_j) = {\sf id}(a'_j) \right) \label{eqn:tlogkid} \end{align}\tag{24}\]

where, \({\sf path}(w_1,\ldots,w_q) \equiv (\bigwedge_{i\in [q-1]} {\sf adj}(w_i,w_{i+1}))\) and for all \(j\in [k']\), \({\sf id}(a_j)\in \{0,1,\ldots,k'\}\). Now to encode \({\sf id}(a_j)\) we add \(t\) nodes \(h_1,\ldots,h_t\) to \(T_2\) and we add the following edges. For each node \(a\) in \(T_2\) such that \({\sf id}(a_j)\in \{0,1,\ldots,k'\}\), we add an edge between \(a\) and \(h_{b+1}\) where \(b={\sf id}(a)\). Let \(G'\) be the graph constructed after this process. Since \(T_2\) is a tree \(\mathbf{tw}(G')=t\). We also a create a label predicate \({\sf P}_2\) and add \(h_1,\ldots,h_t\) to \({\sf P}_2\). Now \({\sf id}(a_j) = {\sf id}(a'_j)\) if and only if both \(a_j\) and \(a'_j\) are adjacent to the same vertex in \({\sf P}_2\). So we can modify (24 ) and get an encoding for \({\sf id}(x_{i-2,1})={\sf id}(x_{i-2,2})\) as follows.

\[\begin{align} \exists a_1,a_1'\in {\sf P}_1 \ldots \exists a_{k'},a_{k'}' \in {\sf P}_1\; \exists q_1\in {\sf P}_2\; \ldots \; q_{k'}\in {\sf P}_2 && {\sf path}(a_1,\ldots,a_{k'},x_{i-2,1}) \wedge \nonumber \\ && {\sf path}(a'_1,\ldots,a'_{k'},x_{i-2,2}) \wedge \nonumber \\ && \left( \bigwedge_{j\in [k'] } {\sf adj}(a_j,q_j) \wedge {\sf adj}(a'_j,q_j) \right) \label{eqn:tlogkid2} \end{align}\tag{25}\]

Thus, after substituting (25 ) in \(\neg \phi (z,y)\), we get a \((c_3,\ldots,c_{i-1},k)\)-FO formula. Let us call this formula \(\neg \phi_{\sf sub} (z,y)\). Finally, we substitute \(\neg \psi_{\sf id}\) in (23 ) with \(\neg \phi_{\sf sub}(z_1,y_1)\vee \neg \phi_{\sf sub}(z_2,y_2)\) to obtain the required formula \(\psi\). The required graph in the theorem is \(G'\). By Lemma 24, we know that \(|V(T)| = O(3^{n/\alpha}+m)\). Since \(V(T_1)=O(|V(T)|\cdot {\sf ilog}(n,i-2))\) (see item (f) above), \(V(G')=O((3^{n/\alpha}+m)\cdot {\sf ilog}(n,i-2) \cdot k \cdot t)\).

The length of the formula is (23 ) is \(O(\alpha^2)\). The size of the formulas mentioned in items (b) and (c) above, are \(O(i)\). The length of the formula in (25 ) is \(O(k)\). Thus, the length of the final formula \(\psi\) is \(O(\alpha^2+i+k)=O(\alpha^2+k)\). This proved property (ii) of the theorem. The number of label predicates used in (23 ) is \(9\). Item (e) above implies that the number of label predicates in \(\phi(z,y)\) is \(4i-8\). We have also introduced two more predicates \({\sf P}_1\) and \({\sf P}_2\). This implies that the number of label predicates in \(\psi\) is \(4i+3=O(1)\). This completes the proof of the theorem. ◻

Proof. Let \(x_1,x_2,\ldots,x_n\) be the variables in \(\phi\). We construct an MSO \(\psi\) formula with \(k\) vertex variables \(v_1,\ldots,v_k\) and \(s\) set variables \(W_1,\ldots,W_s\). Notice that the number of atomic formulas of the form \(v_i\in W_j\) for all \(i\in [k]\) and \(j\in [s]\) is \(k\cdot s \geq n\). Let \(\psi_1\) be the MSO formula on \(k+s\) free variables obtained from \(\phi\) by replacing each \(x_{i,j}\) with \(v_i\in W_j\). Then, we define

Since \(k\cdot s \geq n\), each variable in \(\phi\) can be encoded as \(v_i\in W_j\) for some \(i\) and \(j\), and \(v_i\in W_j\) is true can be interpreted as the corresponding variable in \(\phi\) is set to true. For ease of presentation, we assume that \(\phi\) contains \(k\cdot s\) variables and the variable set is \(\{x_{i,j}~:~i\in [k], j\in [s]\}\).

\[\psi\equiv \exists v_1 \exists v_2 \ldots \exists v_k \exists W_1\ldots \exists W_s\;\; \psi_1\]

Notice that \(|\psi|\leq |\psi_1|+k^2+s= O(|\phi|+k^2+s)\). Next, we prove the correctness of the reduction. Let \(G\) be a graph on at least \(k\) vertices. Suppose \(\phi\) is satisfiable and let \(\beta\) be a satisfying assignment. Let \(u_1,\ldots,u_k\) be arbitrarily chosen \(k\) distinct vertices in \(G\). Now we define \(Z_1,\ldots,Z_k\) as follows. For each \(i\in [k]\) and \(j\in [s]\), \(u_i\in Z_j\) if and only if \(\beta(x_{i,j})\) is true. This implies that \(\psi_1(u_1,\ldots,u_k,Z_1,\ldots,Z_s)\) is true. Since \(u_1,\ldots,u_k\) are distinct vertices, \(\bigwedge_{i,i'\in [k], \; i\neq i'} u_i \neq u_{i'}\) is true. Therefore, \(G\models \psi\).

Now we prove the reverse direction. Let \(G\) be a graph on at least \(k\) vertices and \(G\models \psi\). Then, there exists an assignment to the variables \(v_1,\ldots,v_k, W_1,\ldots,W_s\) such that \(G\models \psi\). Let \(u_1,\ldots,u_k, Z_1,\ldots, Z_s\) be an assignment to \(v_1,\ldots,v_k, W_1,\ldots,W_s\) such that \(\psi\) is true for this assignment. Now we construct a satisfying assignment \(\beta\) for \(\phi\) as follows. For each \(i\in [k]\) and \(j\in [s]\), \(\beta(x_{i,j})\) is true if and only if \(u_i\in Z_j\). Since \(\psi_1(u_1,\ldots,u_k,Z_1,\ldots,Z_s)\) is true, \(\beta\) is a satisfying assignment of \(\phi\). ◻

Proof. Let \(s\leq \min \{k,t\}\) such that \(n\geq s\cdot k\). This implies that \(s\leq \sqrt{n}\). First, we explain the construction of \(G\). \(G\) is a bipartite graph with bipartition \(A\uplus B\). The set \(A\) has \(s\) vertices. Let \(A=\{a_1,\ldots,a_s\}\). The set \(B\) has \(2^s\) vertices. For each subset \(A'\subseteq A\), there is exactly one vertex \(b_{A'}\) in \(B\) which is adjacent to all the vertices in \(A'\) and not adjacent to any vertex in \(A\setminus A'\). This completes the construction of \(G\). Notice that \(\mathbf{tw}(G)\leq s \leq t\) and \(V(G)=2^{s}+s\). Next, we explain the construction of \(\psi\). Let \(s=\min\{k,t\}\). We create two label predicates \({\sf A}\) and \({\sf B}\), where \({\sf A}\) and \({\sf B}\) contain all the vertices in \(A\) and \(B\), respectively. The formula \(\psi\) contains \(s+k\) variables \(w_1,\ldots,w_s, v_1,\ldots,v_k\) such that \(w_1,\ldots,w_s\in {\sf A}\) and \(v_1,\ldots,v_k\in {\sf B}\). Since \(k\cdot s \geq n\), each variable in \(\phi\) can be encoded as \({\sf adj}(v_i,w_j)\) for some \(i\) and \(j\), and \({\sf adj}(v_i,w_j)\) is true can be interpreted as the corresponding variable in \(\phi\) is set to true. For the ease of presentation, we assume that \(\phi\) contains \(k\cdot s\) variables and the variable set is \(\{x_{i,j}~:~i\in [k], j\in [s]\}\). Let \(\psi_1\) be the FO formula on \(k+s\) free variables obtained from \(\phi\) by replacing each \(x_{i,j}\) with \({\sf adj}(v_i,w_j)\). Then, we define \[\psi\equiv \exists v_1\in {\sf B} \exists v_2\in {\sf B} \ldots \exists v_k\in {\sf B} \exists w_1 \in {\sf A}\ldots \exists w_s \in {\sf A}\;\; \psi_1\]

Notice that \(|\psi|=O(|\phi|+k+s)=O(|\phi|+k+t)\). Now we prove the correctness of the reduction. Suppose \(\phi\) is satisfiable and let \(\beta\) be a satisfying assignment. Now we need an assignments to \(v_1,\ldots,v_k\) and \(w_1,\ldots,w_s\) such that \(\psi\) is true under the assignment. Let us assign \(a_j\) to \(w_j\) for all \(j\in [s]\). For each \(i\in [k]\), let \(u_i\) be the vertex in \(B\) such that the following holds. For each \(j\in [s]\), \((u_i,a_j)\in E(G)\) if and only if \(\beta(x_{i,j})\) is true. Now, for all \(i\in [k]\), assign \(u_i\) to \(v_i\). Then, since \(\beta\) is a satifying assignment to \(\phi\), \(\psi_1(u_1,\ldots,u_k,a_1,\ldots,a_s)\) is true. This implies that \(G\models \psi\).

Now we prove the reverse direction. Let \(G\) be a graph on at least \(k\) vertices and \(G\models \psi\). Then, there exists an assignment to the variables \(v_1,\ldots,v_k, w_1,\ldots,w_s\) such that \(\psi_1\) is true under this assignment. Let \(u_1,\ldots,u_k, c_1,\ldots, c_s\) be an assignment to \(v_1,\ldots,v_k, w_1,\ldots,w_s\) such that \(\psi_1\) is true for this assignment. Now we construct a satisfying assignment \(\beta\) for \(\phi\) as follows. For each \(i\in [k]\) and \(j\in [s]\), \(\beta(x_{i,j})\) is true if and only if \((u_i,c_j)\in E(G)\). Since \(\psi_1(u_1,\ldots,u_k,c_1,\ldots,c_s)\) is true, \(\beta\) is a satisfying assignment of \(\phi\). ◻

Proof of Theorem 1. Suppose there is an algorithm for MSO Testing on trees in \(f(k_1,s_1,\dots,k_d,s_d) \cdot \exp^{(i)}(T(s_j, k_i)) \cdot (n+|\phi|)^{O(1)}\) time for a function \(f(k_1,s_1,\dots,k_d,s_d)\) independent of \(s_j\) and \(k_i\). We want to prove that \(T(x,y)=\Omega(xy)\). For the sake of contradiction, assume that \(T(xy)=o(xy)\). Then, for any constant \(a>0\), there exist \(x_a,y_a>0\) such that \(T(x,y)< a x y\) for all \(x\geq x_a\) and \(y\geq y_a\). Let \(a<1/3\) and \(\alpha>1\) be two constants which we fix later.

Let \(G\) be an input instance of \(3\)-Coloring. Let \(n=|V(G)|\). Fix two integers \(s_j\) and \(k_i\) such that \(x_a\leq s_j=O(\log n)\), \(k_i\geq \{y_a,20\}\), and \(n \leq \exp^{(i-1)}(\frac{k_i-9}{2}\cdot s_j) \leq n+O(1)\). We apply Theorem 11, and compute in \(O(3^{n/\alpha})\) time a tree \(T\) and an \(S\)-MSO formula \(\phi\) for \(S = ((k_1,s_1),\dots,(k_d,s_d))\) satisfying the following.

(i) \(G\) is a \(3\)-colorable if and only if \(T\) satisfies \(\phi\).

(ii) \(|V(T)| = O(3^{n/\alpha})\) and \(|\phi| = O(2^{s_j}+k_i+\alpha^2)\).

(iii) \(k_1 = O(\alpha)\), \(k_{i'} = O(1)\) for all \(i'\in [d]\setminus \{1,i\}\).

(iv) \(s_{j'} = 0\) for all \(j' \in [d] \backslash \{j\}\).

Now, applying the algorithm for MSO Testing on trees, \(3\)-Coloringcan be solved in time

\[\begin{align} R(n)&=& O(3^{n/\alpha})+\exp^{(i)}(T(s_j, k_i)) \cdot (3^{n/\alpha}+2^{s_j}+k_i+\alpha^2)^{O(1)} \nonumber\\ &=& O(3^{n/\alpha})+\exp^{(i)}(a\cdot s_j\cdot k_i) \cdot (3^{n/\alpha}+2^{s_j}+k_i+\alpha^2)^{O(1)} \nonumber \end{align}\]

Notice that, for \(a<1/3\), \(\exp^{(i-1)}(a \cdot k_i \cdot s_j)\leq 3a \exp^{(i-1)}(\frac{k_i}{3} \cdot s_j)\). Since \(k_i\geq 20\), \[\exp^{(i-1)}(\frac{k_i}{3}\cdot s_j) \leq \exp^{(i-1)}(\frac{k_i-9}{2}\cdot s_j) \leq n+O(1).\]

Therefore, \[\begin{align} \exp^{(i-1)}(a \cdot k_i \cdot s_j)&\leq& 3a(n+O(1)) \\ \exp^{(i)}(a \cdot k_i \cdot s_j)&\leq& 2^{3a\cdot n+O(1)} \end{align}\]

Then,

\[\begin{align} R(n)&=& O(3^{n/\alpha})+2^{3a\cdot n + O(1)} \cdot (3^{n/\alpha}+2^{s_j}+k_i+\alpha^2)^{O(1)}\nonumber \end{align}\]

Let \(c\) be a constant mentioned in Proposition 33. Now, we choose \(a\) and \(\alpha\) in such a way that \(R(n)\) is at most \(2^{cn}\). Then, this is a contradiction to Proposition 33. ◻

Proof of Theorem 2. Suppose there is an algorithm that solves MSO Testing on trees in time \(f(k_1,s_1,\dots,k_d,s_d) \cdot 2^{T(s_d, k_i)} \cdot (n+|\phi|)^{O(1)}\) for a function \(f(k_1,s_1,\dots,k_d,s_d)\) independent of \(s_d\) and \(k_i\). We want to prove that \(T(x,y)=\Omega(xy)\). For the sake of contradiction, assume that \(T(xy)=o(xy)\). Then, for any constant \(a>0\), there exist \(x_a,y_a>0\) such that \(T(x,y)< a x y\) for all \(x\geq x_a\) and \(y\geq y_a\). Let \(a<1\) be a constant which we fix later.

Now, for any constant \(c\) we design an algorithm for \(3\)-CNF SAT that runs in time \(2^{cn}\) time, where \(n\) is the number of variables in the input \(3\)-CNF formula. This will contradicts ETH. Fix a constant \(c\). Let \(\phi\) be a \(3\)-CNF SAT formula on \(n\) variables. Choose two integers \(k_i\) and \(s_d\) such that \(n\leq k_i \cdot s_d \leq n+O(1)\). Now, we apply Theorem 17, and construct a \((k_i,s_d)\)-MSO formula \(\psi\) in polynomial time with the following specifications.

(i) For any graph \(G\) with \(|V(G)|\geq k_i\), \(G\models \psi\) if and only if \(\phi\) is satisfiable.

(ii) \(|\psi|=O(|\phi|+k_i^2+s_d)\).

We may assume that \(G\) is a tree on \(k_i\) vertices. Also, \(\psi\) is an \(S\)-MSO formula, for \(S=((k_1,s_1),\ldots,(k_d,s_d))\), where \(k_j=0\) for all \(j\neq i\) and \(s_j=0\) for all \(j\neq d\). Now, applying the algorithm for MSO Testing on trees, \(3\)-CNF SAT can be solved in time

\[\begin{align} R(n)&=& 2^{T(s_d, k_i)} \cdot (n+|\psi|)^{O(1)}\nonumber\\ &=&2^{a\cdot s_d\cdot k_i} (n+|\phi|)^{O(1)}\nonumber \\ &=&2^{a (n+O(1))} (n+|\psi|)^{O(1)} \nonumber \end{align}\] By fixing \(a=c\), we get an algorithm for \(3\)-CNF SAT that runs in time \(2^{cn}\) time, which contradicts ETH. ◻

Proof of Theorem 3. Let \(d,i,j \in \mathbb{N}\) such that \(j \leq i \leq d\). Suppose there is an algorithm that solves FO Testing in \(f(k_1,\dots,k_d,t) \cdot \exp^{(i)}(T(k_j,t,k_i)) \cdot (n+|\phi|)^{O(1)}\) time for any function \(f(k_1,\dots,k_d,t)\) that is independent of \(t\), \(k_j\), and \(k_i\). We want to prove that \(T(x,y,z) = \Omega(\min\{x,y\} \cdot z)\). For the sake of contradiction, assume that \(T(x,y)=o(\min\{x,y\}\cdot z)\). Then, for any constant \(a>0\), there exist \(x_a,y_a,z_a>0\) such that \(T(x,y)< a \min\{x,y\}\cdot z\) for all \(x\geq x_a\) and \(y\geq y_a\) and \(z\geq z_a\). Let \(a<1/3\) and and \(\alpha>1\) be two constants which we fix later. We have two cases.

Case 1: \(i>1\). Let \(G\) be an input instance of \(3\)-Coloring. Let \(n=|V(G)|\). Fix two integers \(k\) and \(t\) such that \(x_a<k\), \(y_a<t\), \(\max\{z_a,20\}<k'\), \(\min\{k,t\} =O(\log n)\), and \(n \leq \exp^{(i-1)}(\min\{k,t\}\frac{k'-9}{2}) \leq n+O(1)\). We apply Theorem 12 and compute in \(O(3^{n/\alpha})\) time a graph \(G'\) and an \(S\)-FO formula \(\phi\) for \(S = (k_1,\dots,k_d)\) satisfying the following.

(i) \(G\) is a \(3\)-colorable if and only if \(G'\) satisfies \(\phi\).

(ii) \(|V(G')| = O(3^{n/\alpha})\), \(\mathbf{tw}(G') \leq t\), and \(|\phi| = O(2^{\min\{k,t\}} +k'+\alpha^2)\).

(iii) \(k_{i'} = O(1)\) for all \(i'\in [d]\setminus \{1,j,i\}\)

  - if $1 = j < i$, then $k_1 = k_j = O(\alpha+k)$ and $k_i = k'$;

  - if $1 < j < i$, then $k_1 = O(\alpha)$, $k_j = k$, and
    $k_i = k'$;

  - if $1 < j = i$, then $k_1 = O(\alpha)$, $k_j = k_i = k+k'$.

Now applying the algorithm for FO Testing, we get a solution for \(3\)-Coloringin time

\[\begin{align} R(n)&=&O(3^{n/\alpha})+\exp^{(i)}(T(k,t,k')) \cdot (3^{n/\alpha}+2^{\min\{k,t\}} +k'+\alpha^2)^{O(1)}\\ &=&O(3^{n/\alpha})+\exp^{(i)}(a\min\{k,t\}\cdot k')) \cdot (3^{n/\alpha}+n)^{O(1)} \end{align}\]

Notice that, for \(a<1/3\), \(\exp^{(i-1)}(a \cdot \min\{k,t\} \cdot k)\leq 3a \exp^{(i-1)}(\frac{1}{3} \min\{k,t\} \cdot k')\). Since \(k\geq 20\), \[\exp^{(i-1)}(\frac{1}{3} \min\{k,t\} \cdot k') \leq \exp^{(i-1)}(\min\{k,t\} \cdot \frac{k'-9}{2})\leq n+O(1).\]

Then, \[R(n)= O(3^{n/\alpha})+2^{3a\cdot n + O(1)} \cdot (3^{n/\alpha}+n)^{O(1)}.\]

Let \(c\) be a constant mentioned in Proposition 33. Now, we choose \(a\) and \(\alpha\) in such a way that \(R(n)\) is at most \(2^{cn}\). Then, this is a contradiction to Proposition 33.

Case 2: \(i=1\). In this case, for any constant \(c\) we design an algorithm for \(3\)-CNF SAT that runs in time \(2^{cn}\) time, where \(n\) is the number of variables in the input \(3\)-CNF formula. This will contradicts ETH. Fix a constant \(c\). Let \(\phi\) be a \(3\)-CNF SAT formula on \(n\) variables. Choose two integers \(k\) and \(t\) such that \(n\leq \min\{k,t\} \cdot k \leq n+O(1)\). Now, we apply Theorem 18, and construct a graph \(G\) and a \((k+t)\)-FO formula \(\psi\) in time \(O(2^{\sqrt{n}}+|\phi|)\) with the following specifications.

(i) \(G\models \psi\) if and only if \(\phi\) is satisfiable.

(ii) \(V(G)=O(2^{\sqrt{n}})\) and \(\mathbf{tw}(G) \leq t\).

(iii) \(|\psi|=O(|\phi|+k+t)\).

Since \(t\leq k\), \(\psi\) is a \((2k)\)-FO formula. To solve \(\psi\), we run the algorithm for FO Testing and its running time will be

\[\begin{align} R(n)&=&2^{T(k,t,k)} (|V(G)|+|\psi|)^{O(1)}\\ &=& 2^{a\min\{k,t\}\cdot k} (2^{\sqrt{n}}+n)^{O(1)}\\ &=& 2^{an+O(1)} (2^{\sqrt{n}}+n)^{O(1)} \end{align}\] By fixing \(a=c\), we get an algorithm for \(3\)-CNF SAT that runs in time \(2^{cn}\) time, which contradicts ETH. ◻

Proof of Theorem 4. Let \(d,i \in \mathbb{N}\) such that \(i \leq d\). Suppose there is an algorithm solves FO Testing in \(f(k_1,\dots,k_d,t) \cdot \exp^{(i)}(T(k_i,t)) \cdot (n+|\phi|)^{O(1)}\) time for any function \(f(k_1,\dots,k_d,t)\) that is independent of \(t\) and \(k_i\). We need to prove that \(T(x,y) = \Omega(x \log y)\). We have two cases.

Case 1: \(i>1\). For the sake of contradiction, assume that \(T(x,y)=o(x\log y)\). Then, for any constant \(a>0\), there exist \(x_a,y_a>0\) such that \(T(x,y)< a x\log y\) for all \(x\geq x_a\) and \(y\geq y_a\). Let \(a<1/3\) and and \(\alpha>1\) be two constants which we fix later.

Let \(G\) be an input instance of \(3\)-Coloring. Let \(n=|V(G)|\). Fix two integers \(k_i\) and \(t\) such that \(\max\{x_a,20\}<k_i\), \(y_a<t\), and \(n \leq \exp^{(i-1)}(\frac{k_i-6}{2} \log t) \leq n+O(1)\). We apply Theorem 13 with \(k=k_i\) and compute in \(O(3^{n/\alpha})\) time a graph \(G'\) and an \(S\)-FO formula \(\phi\) for \(S = (k_1,\dots,k_d)\) satisfying the following.

(i) \(G\) is a \(3\)-colorable if and only if \(G'\) satisfies \(\phi\).

(ii) \(|V(G')| = O(3^{n/\alpha})\), \(\mathbf{tw}(G') \leq t\), and \(|\phi| = O(\alpha^{2}+k_i)\).

(iii) \(k_i = k\), \(k_1 = O(\alpha)\), \(k_{i'} = O(1)\) for all \(i' \in \{2,\dots,i-1\}\), and \(k_{i'} = 0\) for all \(i' \in [d] \backslash [i]\).

Now applying the algorithm for FO Testing, we solve \(3\)-Coloringin time

\[\begin{align} R(n)&=&O(3^{n/\alpha})+\exp^{(i)}(T(k_i,t) \cdot (3^{n/\alpha}+ k_i+\alpha^2)^{O(1)}\\ &=&O(3^{n/\alpha})+\exp^{(i)}(a\cdot k_i \log t)) \cdot (3^{n/\alpha})^{O(1)} \end{align}\]

Notice that, for \(a<1/3\), \(\exp^{(i-1)}(a \cdot k_i \log t)\leq 3a \exp^{(i-1)}(\frac{1}{3} k_i \log t)\). Since \(k_i\geq 20\), \[\exp^{(i-1)}(\frac{k_i-6}{2} \log t) \leq \exp^{(i-1)}(\frac{k_i}{3} \log t)\leq n+O(1).\]

Then, \[R(n)= O(3^{n/\alpha})+2^{3a\cdot n + O(1)} \cdot (3^{n/\alpha}+n)^{O(1)}.\]

Let \(c\) be a constant mentioned in Proposition 33. Now, we choose \(a\) and \(\alpha\) in such a way that \(R(n)\) is at most \(2^{cn}\). Then, this is a contradiction to Proposition 33.

Case 2: \(i=1\). We know that the Clique problem (finding a clique of size \(k\) on an \(n\) vertex graph) can not be solved in time \(n^{o(k)}\) unless ETH fails. Let \(G'\) be a graph on \(n\) vertices. We can encode the existence of a clique of size \(k\) using the following FO formula.

\[\exists v_1 \ldots \exists v_k \bigwedge_{1\leq i'<j'\leq k} {\sf adj}(v_{i'},v_{j'})\]

So, if \(T(x,y)=o(x\log y)\), then using the algorithm for FO Testing, we can solve Clique in time \(2^{o(k\log n)}\) (because treewidth of \(G'\) is at most \(n\)). This contradicts ETH. ◻