I've thought of the problem some more, and think I have more insight:
1. The current approach actually computes all permuted states from each reachable state by performing the permutations, but storing only a (deterministically) selected representative. This assumes that building such steps through permutations is faster than reaching it through a next step. The difference, however, is not as big as it can be, which can make this optimization not powerful enough or even somewhat harmful, and potentially very harmful in light of point 2.
2. It is possible (and is indeed the case in my model) that many of the permuted states -- while valid -- are not actually reachable. This means that the optimization computes many more states than would have been computed through reachability alone, and due to 1, it is sensitive to even to non-extreme correlations between symmetry sets. As an example, we can have two symmetry sets {a, b, c} and {x, y, z} that are both valid but are strongly correlated in the model which may ensure that in all reachable states, `a` always maps to `x`, `b` to `y` and `c` to `z`. Which means that the optimization will compute 9 steps, while only 3 are actually reachable (i.e. 3x states). As the computation via permutation is less than 3 times faster than computation via next-step, the result is a net loss which may be large.
Problem 1 may be solved through a different implementation of permute(), preferably one that doesn't allocate an actual complete state for each permutation.
Problem 2 may be solved by letting the user supply a predicate which would validate reachable compund permutations. In the example above, it would declare the compund permutation ([a |-> b, b |-> c, c |-> a], [x |-> y, y |-> z, z |->x]) as valid, but ([a |-> b, b |-> c, c |-> a], [x |-> x, y |-> y, z |->z]) as invalid.
Ron