Symmetry Quotienting

merc_pbes quotients the state space of a PBES by a symmetry group found on its symmetry detection graph using base and strong generating set (BSGS). The quotienting process then uses this BSGS to efficiently canonicalize orbits and Below is an exposition of the algorithm used.

Stabilizer chains

A group acting on the parameter block gives a descending chain of stabilizers along a base — a sequence of points — where each is the stabilizer of within the previous group in the chain.

Each acts on the previous one's coset space via a transversal : a set of representatives, one per orbit point of under , so that every factors uniquely as for some and . Chaining this over the whole base gives every a unique factorisation , — the fact both algorithms below exploit: fixing already fixes for every , no matter what the remaining factors turn out to be.

Naive algorithm

§5.1 of the report picks the base for every position — the full base . Every position gets its own level, whether or not the group actually moves it; a position the group fixes just gets a singleton transversal . Cleaned up from the report's draft pseudocode into pseudocode that matches what it evidently intends:

The load-bearing detail, easy to read past: the inner loop runs — and current gets filtered on value — even when U[j] is a singleton. A position the group fixes still gets compared, it just never branches. That turns out to matter more than it looks like it should.

Compressed base and Schreier–Sims levels

Building a level for every one of the positions is wasteful when the group's support is small relative to — a symmetry that only permutes a handful of a PBES's data parameters still leaves a base of length under the report's recipe, almost all of it singleton transversals contributing nothing but bookkeeping. merc's Bsgs instead builds a Schreier–Sims base: at each level, is chosen as the smallest point some generator of actually moves, and the recursion stops once no generator moves anything. Positions the group fixes at that depth never get a SchreierLevel at all — Bsgs::chain only holds points that genuinely branch.

This is the actual size reduction: no orbit-transversal BFS, no Schreier generators, no HashMap-backed transversal is ever built for a fixed point. It is not a reduction in how many positions canonicalize has to look at — it still has to visit every index from to in order, for exactly the reason the report's own loop does: lexicographic order is decided position by position, and skipping one silently means silently deciding it's irrelevant, which is only sometimes true (see below).

The optimised pseudocode

Bsgs::canonicalize walks against the compressed chain. At a real base point it does what the report's loop does. Everywhere else, it reconstructs that loop's filtering effect by hand, without the singleton transversal ever being materialized:

The else branch is doing exactly the report's inner loop with U[j] = {identity} substituted in and the now-pointless composition dropped — same filter, same cost per candidate, just without ever allocating a transversal to hold the one element that loop would have used.