Refinement-Derived Algebraic Computation of Graph Automorphism Groups

We compute the automorphism group of a graph exactly, with a verified generatingset. Inside each class of an invariant colouring, individualisation and refinement yielda permutation group TC that contains the restriction of every automorphism; a normalseries of these groups turns the edges between classes into affine systems over finitefields, solved without enumeration. This is the classical bounded-colour-multiplicitytower method, applied where bounded multiplicity is not given, and it involves nosearch. Where the local groups are too large, a stabiliser chain individualises rootstaken from a new rooted decomposition, dialysis, and decides their orbits with thesame algebra. Dialysis also yields invariants of projective planes. Exactness is proved.The algebraic solver is polynomial under bounded class size, and it is polynomialon the multipedes of Neuen and Schweitzer, on which individualisation–refinementis exponential. The chain is polynomial whenever refinement computes the orbitsof the pointwise stabilisers it meets. Graphs on which this holds for every tuple ofvertices are the Tinhofer graphs of Arvind, Köbler, Rattan and Verbitsky; we provethat all Johnson graphs, including J(2k, k), and all Hamming graphs are Tinhofer,so the chain is polynomial on them. On projective planes the condition fails and thechain attains the same N^O(log log N ) bound as Miller’s argument. All 12,001 instancesof 36 benchmark families are solved, 10,911 by the algebraic solver alone; Traces,used as an independent oracle, agrees wherever it answered.