Orbit Computation by Satisfiability: Structural Invariants and their Boundaries

Abstract

We compute vertex orbits exactly by reducing the problem to pairwise satisfiability queries,with a checked witness in the satisfiable direction and encoding-based certification in the un-satisfiable one. Each query is constructed so that its models are exactly the automorphismsmapping one vertex to the other: a model is an explicitly verifiable witness, and — because theencoding is complete — unsatisfiability is a proof of non-equivalence. A run in which every queryis resolved therefore certifies its own output without appeal to an external tool, which is whatpermits reporting results on instances where no independent computation terminates. The twodirections are not equally guarded, and we are explicit about it: a positive answer is checked byan independent O(m) verifier, whereas a negative answer rests on the solver together with thecompleteness argument, and making it independently checkable — by emitting and checkingunsatisfiability proofs — is left to future work. We identify a consequence for practitioners:symmetry breaking, the standard accelerator for satisfiability instances with large automorphismgroups, is inadmissible here, because it eliminates models and would invalidate the direction onwhich certification rests. Tractability comes instead from invariants that discharge questionsbefore the solver is reached: an isomorphism-invariant colouring anchored to a rooted structuraldecomposition; closure of the orbit equivalence relation in both directions; orbits of a feedbackvertex set propagated by refinement; and, where the construction permits, parity constraintsdischarged by Gaussian elimination. Across 20 benchmark families and 3033 instances we certify2977 (98.2%), with exact orbit partitions up to n = 8000. This is not a performance result: oninstances Traces completes it is usually faster than our method, and on thirteen of the twentyfamilies it is the better tool outright. What the measurements show instead is a difference inreach and in dispersion. On seven families — six rigid Cai–Fürer–Immerman constructions andthe independent Dawar–Yeung family — Traces reaches a practical limit that our method passes by factors of 1.3 to 3.6 in n, and it fails on 174 of 1633 instances under a 1 h/4 GB limit,with first failures from n = 384; within a single instance size its completed running times spanup to 26620×, where ours stay within 14.8×. We report the boundaries with their mechanisms:families whose gadget group condition is not a parity condition and is therefore invisible toWeisfeiler–Leman refinement of any dimension; highly symmetric families on which no invari-ant colouring discriminates and the encoding does not fit; and incidence geometries, which lieoutside the method’s regime altogether.