Proofs: nauty

The individualization-refinement search returns a canonical form and the automorphism group order full

This proof shows: correctness, termination.

Setting. $G$ is a simple undirected graph on $V = \{0, \ldots, n-1\}$ with a vertex coloring $c$. A permutation $\gamma$ of $V$ acts on graphs, colorings and ordered partitions by renaming vertices; $G^\gamma$ is the renamed graph. An automorphism is a $\gamma$ with $G^\gamma = G$ and $c^\gamma = c$. For a discrete ordered partition $\pi = (\{v_0\}, \ldots, \{v_{n-1}\})$, the labeling $\lambda_\pi$ maps $v_i$ to $i$, and the leaf value $F(\pi)$ is the pair (colors of $v_0, \ldots, v_{n-1}$, adjacency rows of $G$ relabeled by $\lambda_\pi$). The full tree $T(G)$ has the root $R(\pi_0)$, where $R$ is REFINE and $\pi_0$ the color partition, and a node $\pi$ that is not discrete has the children $R(\pi \downarrow w)$ for $w$ in the target cell, where $\pi \downarrow w$ is individualization.

Lemma 1 (invariance). For every permutation $\gamma$: $R_{G^\gamma}(\pi^\gamma) = R_G(\pi)^\gamma$, $(\pi \downarrow w)^\gamma = \pi^\gamma \downarrow \gamma(w)$, the target cell index of $\pi^\gamma$ equals that of $\pi$, and $F_{G^\gamma}(\pi^\gamma) = F_G(\pi)$ for discrete $\pi$.

Proof. REFINE splits cells by the number $|N(v) \cap S|$ of neighbors in a splitter cell and orders the pieces by that number; renaming changes neither the numbers nor the order of cells, so every step commutes with $\gamma$. Individualization places $\{w\}$ at the index of its cell, which is also invariant. TARGET-CELL uses only cell sizes and indices. For the leaf value, $\pi^\gamma$ lists $\gamma(v_0), \ldots, \gamma(v_{n-1})$, and $\gamma(v_i) \sim \gamma(v_j)$ in $G^\gamma$ exactly when $v_i \sim v_j$ in $G$, with the same colors. $\square$

Hence $\gamma$ maps $T(G)$ onto $T(G^\gamma)$, node by node, and leaves with equal values.

Lemma 2 (equal leaf values give automorphisms). If leaves $\pi, \pi'$ of $T(G)$ have $F(\pi) = F(\pi')$, then $\gamma = \lambda_{\pi'}^{-1} \lambda_\pi$ is an automorphism, and $\pi^\gamma = \pi'$.

Proof. $\gamma$ maps the vertex at position $i$ of $\pi$ to the vertex at position $i$ of $\pi'$. Equal colors and equal relabeled rows mean that $v_i \sim v_j$ iff $\gamma(v_i) \sim \gamma(v_j)$ and $c(v_i) = c(\gamma(v_i))$. This is the map recorded in L6. $\square$

Lemma 3 (pruning is safe). Let $\nu$ be a node with prefix $P$ and children $w, w'$, and let $\gamma$ be an automorphism fixing every vertex of $P$ with $\gamma(w) = w'$. Then the subtrees under $w$ and $w'$ have the same sets of leaf values. The same holds when $\gamma$ is a product of such automorphisms.

Proof. The node $\nu$ is obtained from the root by refining and individualizing the vertices of $P$ in order; since $\gamma$ fixes $P$ and $G^\gamma = G$, Lemma 1 gives $\nu^\gamma = \nu$. Then $\gamma$ maps the child $R(\nu \downarrow w)$ to $R(\nu \downarrow w')$, and by Lemma 1 it maps the subtree of the first onto the subtree of the second with equal leaf values. Products of automorphisms fixing $P$ fix $P$. $\square$

Theorem. The search terminates. It returns $F^\ast(G) = \max \{F(\pi) : \pi \text{ a leaf of } T(G)\}$, so $F^\ast(G) = F^\ast(H)$ exactly when $G \cong H$ as colored graphs; and the returned order equals $|\mathrm{Aut}(G)|$.

Proof. Termination. Each child has strictly more cells than its parent, since $\pi \downarrow w$ splits a cell of size at least 2 and REFINE never merges cells, so the depth is at most $n$; each node has at most $n$ children and each frame scans its target cell once. REFINE stops because each repetition increases the number of cells.

Maximum. L9 skips a child only if it lies in the orbit of an explored sibling under automorphisms that fix the prefix, so by Lemma 3 the skipped subtree has the same leaf values as an explored one. By induction on the height, the explored leaves have the same set of values as all leaves of $T(G)$, and L5 to L7 keep the maximum.

Canonical form. If $H = G^\gamma$, Lemma 1 maps $T(G)$ onto $T(H)$ with the same leaf values, so $F^\ast(G) = F^\ast(H)$. Conversely, $F^\ast(G)$ is the value of a leaf of $T(G)$, which is the colored graph $G$ relabeled by a bijection; if $F^\ast(G) = F^\ast(H)$, both graphs are isomorphic to the same relabeled graph.

Group order. Let $\nu_0, \nu_1, \ldots, \nu_k$ be the first path, where $\nu_k$ is the first leaf, $P_d$ the prefix of $\nu_d$, $C_d$ its target cell, and $w_d \in C_d$ its first child. Let $A_d$ be the automorphisms fixing $P_d$ pointwise, so $A_0 = \mathrm{Aut}(G)$. By Lemma 1, $A_d$ fixes $\nu_d$, so it maps $C_d$ to itself; $A_{d+1}$ is the stabilizer of $w_d$ in $A_d$; and $A_k$ is trivial because it fixes the discrete partition $\nu_k$. By the orbit-stabilizer theorem, $|\mathrm{Aut}(G)| = \prod_{d < k} |w_d^{A_d}|$. It remains to show that the generators $S_d$ found that fix $P_d$ have the orbit $w_d^{\langle S_d \rangle} = w_d^{A_d}$. One inclusion is clear. For the other, let $w = \alpha(w_d)$ with $\alpha \in A_d$. The child $w$ of $\nu_d$ is either explored or skipped. If it is skipped, it is in the orbit of an explored child $u$ under found automorphisms fixing $P_d$, so it suffices to show that each explored child $u$ in the $A_d$-orbit of $w_d$ is joined to $w_d$. The subtree of $u$ is the image under some $\beta \in A_d$ with $\beta(w_d) = u$ of the subtree of $w_d$, so it contains leaves with value $F(\nu_k)$; by the argument of the maximum part applied inside that subtree, the search reaches at least one leaf $\pi$ with $F(\pi) = F(\nu_k)$. At that leaf L6 records $\gamma$ with $\nu_k^\gamma = \pi$ (Lemma 2); REFINE and individualization replace a cell by its pieces in place, so in every leaf below $\nu_d$ a vertex that is a singleton of $\nu_d$ sits at position equal to the number of vertices in the earlier cells of $\nu_d$, and the vertex individualized from $C_d$ sits at the first position of $C_d$. So $\gamma$, which maps the vertex at each position of $\nu_k$ to the vertex at the same position of $\pi$, fixes every vertex of $P_d$ and maps $w_d$ to $u$. So $\gamma \in A_d$, $\gamma \in S_d$, and $\gamma(w_d) = u$. (If the value at $\pi$ equals both stored values, L6 compares with the first leaf first, which is the case used here.) Hence the orbits agree, and L11 computes $|\mathrm{Aut}(G)|$. $\blacksquare$