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×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)∧SB(M) is satisfiable, where SB(M) is a symmetry-breaking predicate—a predicate satisfied by at least one matrix M in each isomorphism class. P(M)∧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 for their respective classes of objects.