On the constructive orbit problem

摘要

Symmetry reduction techniques aim to combat the state-space explosion problem for model checking by restricting search to representative states from equivalence classes with respect to a group of symmetries. The standard approach to representative computation involves converting a state to its minimal image under a permutation group G, before storing the state. This is known as the constructive orbit problem (COP), and is NP hard. It may be possible to solve the COP efficiently if G is known to have certain structural properties: in particular if G is isomorphic to a full symmetry group, or G is a disjoint/wreath product of subgroups. We extend existing results on solving the COP efficiently for fully symmetric groups, and investigate the problem of automatically classifying an arbitrary permutation group as a disjoint/wreath product of subgroups. We also present an approximate COP strategy based on local search, and some computational group-theoretic optimisations to improve the basic approach of solving the COP by symmetry group enumeration. Experimental results using the TopSpin symmetry reduction package, which interfaces with the computational group-theoretic system Gap, illustrate the effectiveness of our techniques.