<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>9284</REFNUM><AUTHORS><AUTHOR>Donaldson,A.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2009</YEAR><TITLE>On the constructive orbit problem</TITLE><PLACE_PUBLISHED>Annals of Mathematics and Artificial Intelligence</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>1-102</PAGES><ISBN>1012-2443 (Print) 1573-7470 (Onl</ISBN><LABEL>Donaldson:2009:9284</LABEL><KEYWORDS><KEYWORD>Verification</KEYWORD></KEYWORDS<ABSTRACT>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.</ABSTRACT></RECORD></RECORDS></XML>