breaking and randomly branching. As we saw in the example, different symmetries of the symmetry breaking constraints interact in different ways with the problem constraints. Although the problem constraints are themselves initially symmetrical, branching decisions quickly break the symmetries.

## 5 Posting Constraints Dynamically

We now consider a more sophisticated use of the observations that any symmetry acting on a set of symmetry breaking constraints itself breaks symmetry, and that differentsymmetries pick out different solutions in each symmetry class.

We will incrementally and dynamically post a symmetry of the symmetry breaking constraints which is consistent with the branching decisions made so far. Thus, if the branching heuristic is smart or lucky enough to branch immediately to a solution, symmetry breaking will not interfere with this. Running Example. Consider again the all interval series problem. Suppose we begin by trying X1 = 10*. Since the* Xi are all different, X11 ∈ [0, 9]*. Hence, the symmetry breaking* constraint X11 < X1 *is entailed. This is* σrev *of (1). It is* also θinv *of (1). We do not yet need to commit to which of* these two symmetries of the symmetry breaking constraints we will post. We are sure, however, that we are not posting σid or θinv ◦ σrev of the constraints (1) to (3). These two symmetries would require X1 > X11*, and this is dis-entailed.* We therefore post X11 < X1 *and continue search.* ♣
In the example, we posted symmetry breaking constraint once they are entailed. When there are only a few symmetries, we can easily implement this with non-backtrackable variables and reification. Suppose we reify the two ordering constraints:

$$11$$

## B1 ⇔ (X1 < X11), B2 ⇔ (X11 < X1)

We then make the Boolean variables, B1 and B2 nonbacktrackable so that, once they are instantiated, their value remains on backtracking. We assume that our solver posts the conclusion of an implication when its hypothesis is entailed.

Suppose X1 < X11 is entailed. Then B1 will be set **true**. As B1 is non-backtrackable, X1 < X11 will be posted. Unfortunately, posting symmetry breaking constraints like this as soon as they are entailed may be a little eager. Running Example. *Consider again the all interval series* problem. As before, suppose the branching heuristic has set X1 = 10*, and we have posted the entailed symmetry breaking constraint* X11 < X1. Now X1 ≥ 5 is also entailed. This is θinv *of the first inequality in (2). If we post this, we commit to breaking symmetry with* θinv of (1) to (3). However, this would rule out breaking symmetry with σrev *of (1) to (3)*
which are also still consistent with the branching decisions so far.

Suppose we next branch on X11 = 5*. The assignments to* X1 and X11 *are only consistent with* θinv *of (2) and of (3).*
In fact, both of these constraints are now entailed. However, X1 = 10 and X11 = 5 *are not consistent with posting* σrev of (3). This would require that:

$$\begin{array}{r l}{\langle X_{11},\ldots,X_{6}\rangle}&{{}\leq_{l e x}\quad\langle10-X_{1},\ldots,10-X_{6}\rangle}\end{array}$$

This is dis-entailed. Hence, our branching decisions have committed us to break symmetry with θinv *of (1) to (3). We* therefore post these constraints. If search continues, we will discover the unique solution consistent with symmetry breaking and the initial branching decisions:
X1, X2**, . . . , X**11 = 10, 0, 9, 1, 8, 2, 7, 3, 6, 4, 5

## ♣

There is a tradeoff between posting symmetry breaking constraints early (so propagation prunes the search space) and late (so we do not conflict with future branching decisions). We propose the following rule for when to post symmetry breaking constraints. The rule only posts symmetry breaking constraints once the branching heuristic has forced their choice. It would, however, be interesting to explore other more eager or lazy rules. Suppose S is a set of symmetry breaking constraints for Σ, and we have posted T , a symmetry of a subset of S. A symmetry σ ∈ Σ is *consistent* with T iff T is entailed by σ(S) and *inconsistent* otherwise. A
symmetry σ ∈ Σ is *eliminated* by posting some symmetry breaking constraint c iff σ is consistent with T but inconsistent with T ∪ {c}. The *forced symmetry* rule is defined as follows:
Given a set of symmetry breaking constraints, if during backtracking search a symmetry of one of these constraints is entailed, this symmetry is consistent with previously posted symmetry breaking constraints, and all symmetries eliminated by this entailed constraint are inconsistent with the current state then we post the entailed constraint.

We first show that this rule is sound.

Observation 3. Given a set of symmetries Σ of C*, if* S is a sound set of symmetry breaking constraints for Σ then the forced symmetry rule using S *is a sound symmetry breaking* method.

Proof: The rule only permits constraints of a particular symmetry to be posted. By Observation 1, this is sound. ✷
In general, this rule may not be complete even when given a complete set of symmetry breaking constraints. However, it is easy to modify the rule so that it is complete. Whenever we reach a solution, we simply pick a consistent symmetry and post all the symmetry breaking constraints associated with this symmetry. We can also define a common property of many symmetry breaking constraints for which the unmodified rule is complete. A set of symmetry breaking constraints S for the symmetries Σ of C is *proper* iff S is sound and complete for Σ and every non-identity symmetry in Σ maps any solution of S ∪C onto a different solution. With a proper set of symmetry breaking constraints, each solution within a symmetry class is associated with a different symmetry. For instance, constraints (1) to (3) form a proper set of symmetry We new prove that with a proper set of symmetry breaking constraints, the forced symmetry rule is a sound and complete symmetry breaking method. That is, it will find exactly one solution in each symmetry class.

Observation 4. Given a set of symmetries Σ of C, if S *is a* proper set of symmetry breaking constraints for Σ *then the* forced symmetry rule is both sound and complete.