Symmetry Breaking in Constraint Satisfaction

Abstract Symmetry-breaking formulas, introduced by Crawford, Ginsberg, Luks and Roy, are supplementary conditions that are added to a given constraint-satisfaction problem. They are satisfied by exactly one element (e.g. the lexicographic leader) from each set of "symmetrical points " in the search space and can therefore be used to accelerate the search for a solution without sacrificing solvability. We study the computational complexity of generating lex-leader formulas. We show that, even for abelian groups, it may be intractable to generate all the essential clauses in the "natural " lex-leader formula. Nevertheless, we show that techniques of computational group theory allow efficient construction of small lex-leader formulas for these, and more general, groups