Symmetry Breaking in Constraint Satisfaction.
Eugene M. Luks, Amitabha Roy · 2002
Symmetry-breaking formulas, introduced by Crawford, Ginsberg, Luks and Roy, are supplementary conditions that are added to a given constraint-satisfaction problem. They are satis ed 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 sacri cing 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 \ atural" lex-leader formula. Nevertheless, we show that techniques of computational group theory allow ecient construction of small lex-leader formulas for these, and more general, groups.