Use of inherent symmetries to speed computation has been an effective tech­nique in many constraint satisfaction problems. Typically this involves modifying a search algorithm to exploit the symmetry. As an alternative, we study a general scheme wherein symmetries are used to modify the input problem itself. Thus instead of having to reformulate each advance in search technology, we add a "symmetry breaking" formula that can be used as a preprocessor to existing or future constraint solvers.

A symmetry breaking formula is a boolean formula that is satisfied by exactly one member from each set of symmetric points in the original search space. For example, we choose this member to be the lexicographic leader in the orbit of assignments under the action of a permutation group on the input variables.

A main computational hurdle is that it is often intractable to generate the entire lex leader predicate. Indeed, we prove the existence of groups for which the smallest lex leader predicate is of exponential size. These intractable examples suggest consideration of Sperner families of sets whose incidence vectors form a subspace of Z₂ⁿ. However we show how to construct succinct lex leader formulas for abelian groups and groups with bounded orbit projections (and hence also the groups corresponding to Sperner families). Our formulas exploit the polynomial time algorithmic machinery developed to solve the lex leader problem for "good groups", e.g., solvable groups or more generally for groups with bounded non-cyclic composition factors.

A dual goal to efficiency of search is robustness of solutions. We desire that the solutions produced not be "brittle": an optimal solution is undesirable if any unforeseen event makes it untenable (e.g. a resource suddenly becoming unavailable in a resource allocation problem). To model this concept of fault tolerance, we introduce the notion of δmodels: these are satisfying assignments of a boolean formula for which any small alteration, such as a single bit flip, can be repaired by another small alteration, yielding a nearby satisfying assignment. We study computational problems associated with δmodels and some combinatorial generalizations thereof.