Generating effective symmetry-breaking predicates for search problems

Consider the problem of testing for existence of an n-node graph G satisfying some condition P, expressed as a Boolean constraint among the n x n Boolean entries of the adjacency matrix M. This problem reduces to satisfiability of P(M). If P is preserved by isomorphism, P(M) is satisfiable iff P(M) boolean AND SB(M) is satisfiable, where SB(M) is a synunetr-breaking predicate-a predicate satisfied by at least one matrix M in each isomorphism class. P(M) A SB(M) is more constrained than P(M), so it is solved faster by backtracking than P(M)-especially if SB(M) rules out most matrices in each isomorphism class. This method, proposed by Crawford et al., applies not just to graphs but to testing existence of a combinatorial object satisfying any property that respects isomorphism, as long as the property can be compactly specified as a Boolean constraint on the object's binary representation. We present methods for generating symmetry-breaking predicates for several classes of combinatorial objects: acyclic digraphs, permutations, functions, and arbitrary-arity relations (direct products). We define a uniform optimality measure for symmetry-breaking predicates, and evaluate our constraints according to this measure. Results indicate that these constraints are either optimal or near-optimal or near-optimal for their respective classes of objects. (c) 2006 Elsevier B.V. All tights reserved.