Symmetry-breaking formulas for groups with bounded orbit projections

This paper considers the problem of generating lex-leader symmetry-breaking formulas for per-mutation groups whose orbit constituents have bounded size. We prove that one can find an ordering of the permutation domain for which there is a polynomial size lex-leader formula. This generalizes the results of [Luks and Roy, 2004] which considered the problem for permu-tation groups with orbits of size 2. Our con-struction is based on writing a Boolean for-mula that captures the logic of Sims’s meth-ods ([Sims, 1971]) to test membership in per-mutation groups, a classic result in computa-tional group theory.