Static Symmetry Breaking with the Reflex Ordering

1 Introduction

Symmetries are common in many constraint problems. They can be broken statically [Crawford et al., 1996; Flener et al., 2002] or dynamically [Fahle et al., 2001; Roney-Dougal et al., 2004]. LexLeader [Crawford et al., 1996], as the state of the art static method, adds lex ordering constraints to select the lexicographically least solution to break symmetries of indistinguishable objects. In practice, the same method is often used for partial symmetry breaking by only breaking a subset of symmetries, with DOUBLELEX [Flener et al., 2002] and SNAKELEX [Grayland et al., 2009] being well known special cases. The multiset ordering constraint [Frisch et al., 2009] and Gray code constraint [Narodytska and Walsh, 2013] are also proposed to break variable symmetries based on other orderings.

Given the same subset of symmetries, the pruning power of partial symmetry breaking depends highly on the extra composition symmetries that can be broken by the interactions among symmetry breaking constraints [Lee and Li, 2012]. Recently, Lee and Zhu [2016] propose two heuristics to break more composition symmetries on the basis of Partial Symmetry Breaking During Search [Gent and Smith, 2000]. Their method restricts the search heuristic and thus cannot be combined with other search techniques. The multiset ordering is only a partial order and is thus often used in combination with the lex ordering constraint. The Gray code constraint focuses on Boolean variable vectors. We propose a new total ordering, reflex, and also a reflex ordering constraint for breaking variable symmetries on integer problems. We show empirically that given the same subset of symmetries, reflex ordering constraints (and their combination with the Precedence constraints [Law and Lee, 2004]) can break more composition symmetries than lex ordering constraints (and their combination with the Precedence constraints).

We give theorems to compare the reflex and lex orders. An efficient GAC filtering algorithm is given. Based on this reflex ordering, the ReflexLeader method is thus proposed by adding one reflex ordering constraint for every variable symmetry of the problem or a subset. We prove that ReflexLeader is safe to combine with Precedence [Law and Lee, 2004] which is used to break value interchangeability as long as they use the same fixed variable and value orders. In matrix problems, we prove that multiset ordering [Frisch et al., 2009] the rows (columns) and reflex ordering the columns (rows) are sound. Experimentations demonstrate the reflex ordering constraint can drastically reduce the solution set size, search space and runtime when compared against state-ofthe-art methods based on the lex ordering constraint.

2 Background

A constraint satisfaction problem (CSP) P is a tuple (X↪D↪C) where X is a finite set of variables, D is a finite set of domains such that each x 2 X has a domain D(x) and C is a set of constraints, each a subset of the Cartesian product D(xi1 ) ⇥ · · · ⇥ D(xik ) of the domains of the involved variables (scope). A constraint is generalized arc consistent (GAC) iff every value in the domain of a variable in the scope can find compatible values (called supports) from the domains of all the other variables in the scope. An assignment x = v assigns value v to variable x. A full assignment is a set of assignments, one for each variable in X. A solution to P is a full assignment that satisfies every constraint in C.

Here we consider symmetry as a property of the set of solutions. A solution symmetry [Rossi et al., 2006] is a solutionpreserving permutation on assignments. A variable symmetry σ is a bijection on variables that preserves solutions: if ¶xi = vi♣1  i  n♦ is a solution, then ¶xσ(i) = vi♣1  i  n♦ is also one. A value symmetry ✓ is a bijection on values that preserves solutions: if ¶xi = vi♣1  i  n♦ is a solution, then ¶xi = ✓(vi)♣1  i  n♦ is also. A set of values V is interchangeable iff any bijection mapping from V ! V is a value symmetry. A symmetry class [Flener et al., 2002] is an equivalence class of full assignments, where two assignments are equivalent if there is some symmetry mapping one into the other. A symmetry breaking method is sound (complete) iff it leaves at least (most) one solution in each symmetry class.

Given a group of variable symmetries G. LexLeader [Crawford et al., 1996] adds one lex ordering constraint [Frisch et al., 2002], lex, per variable symmetry g 2 G according to a fixed variable order. DOUBLELEX [Flener et al., 2002] and SNAKELEX [Grayland et al., 2009] are two partial methods based on LexLeader by posting constraints to break only special subsets of matrix symmetries.

3 The Reflex Ordering

We introduce reflex, a new total ordering. First, we give some basic definitions. Given an integer vector a. Notation min(a) denotes the min value in a, and posm(a) denotes the first position of min(a) in a. We use a - hposm(a)i to denote the vector after deleting the first occurance of min(a) from a. Vectors are indexed from 0, and ai denotes the ith item of a.

An integer vector a is reflexicographically (reflex) smaller than another integer vector b, written a <rlex b, iff a = NULL and b 6= NULL; or min(a) < min(b); or min(a) = min(b) and posm(a) < posm(b); or min(a) = min(b) and posm(a) = posm(b) and a - hposm(a)i <rlex b - hposm(b)i. An integer vector a is reflex smaller than or equal to another integer vector b, written a rlex b, iff a = b or a <rlex b. In other words, the reflex ordering first compares the least values in the two vectors, then the first occurrence positions of the least values if the values are the same. If both the least values and their first occurrence positions are all equal, the two vectors are compared again after discarding the least values from the vectors respectively.

Consider the following two vectors

a <rlex b since the min values in a and b are both 1 and both occur first at position 1, but the second occurrence of 1 in a appears earlier than that in b.

The reflex ordering is like a mirror reflection of the lex ordering, which compares first the least positions (always the same) and then the values of the least positions in the vectors. If the least (zeroth) position values are the same, they are discarded from the vectors, which will be compared again.

We can also define reflex in another way. If pa = (v↪ p) is a pair, then we define pa▷val = v and pa▷pos = p. Given an integer vector a, the sorted index vector as of a is a vector of pairs such that (1) ♣as ♣ = ♣a♣ = n, (2) each item in as is a pair (v↪ p), (3) 8i 2 [0↪ n), 9j 2 [0↪ n) such that (ai↪ i) = asj and (4) items in as are sorted in increasing order of v and ties are broken by p in increasing order again.

The sorted index vectors as and bs of vectors in (1) are

We overload < for integer pairs and define (p1↪ p2) < (q1↪ q2) iff (1) p1 < q1 or (2) p1 = q1 and p2 < q2. Thus, we can have lex on two vectors of pairs. Suppose a and b are two vectors. We state the following theorem without proof.

Theorem 1. Given two integer vectors a and b. a rlex b iff as lex bs .

We say that a <lex b at position i iff ai < bi and aj = bj for all j < i. Consider the two vectors in (1), a <rlex b since as <lex bs at position 1.

Theorem 2. <rlex is a total ordering on integer vectors.

Proof. The result follows directly from Theorem 1 and the fact that <lex is a total ordering.

The reflex and lex orderings coincide in only a special circumstance.

Theorem 3. Given two integer vectors a and b where the number of distinct values in them is 2. a rlex b iff a lex b.

Proof. W.L.O.G, we assume there are only 0s and 1s in a and b. The theorem is trivially true when a = b. We prove the theorem for a 6= b. ()) a <rlex b means as <lex bs . Suppose as <lex bs at position i. Then all values before this position in a and b are pairwise equal and aasi ▷pos = 0 but basi ▷pos = 1. Thus a <lex b. (() If a <lex b at position j, we must have aj = 0 and bj = 1. Thus as <lex bs at position k and ask ▷pos = j. a <rlex b.

Proposition 1. Given two integer vectors a and b where the number of distinct values in a and b is larger than 2. There are cases that (1) a <rlex b and a <lex b and (2) a <rlex b and a >lex b.

Proof. (1) a = h0↪ 0↪ 1↪ 2↪ 3↪ 1i and b = h0↪ 0↪ 1↪ 3↪ 2↪ 1i. (2) a = h0↪ 0↪ 2↪ 1↪ 0↪ 1i and b = h0↪ 0↪ 1↪ 1↪ 2↪ 0i.

4 GAC Enforcement

Utilizing the definition of sorted index vector and Theorem 1, the reflex ordering constraint X rlex Y can be decomposed into (a) ♣X♣ + ♣Y♣ element constraints and ♣X♣ + ♣Y♣ - 2 ordering constraints to sort pairs to get the sorted index variable vectors Xs and Ys and (b) Xs lex Ys . However, this decomposition hinders propagation and is also expensive due to the introduction of extra variables and constraints.

In the following, we give a GAC algorithm on the reflex ordering constraint X rlex Y on two integer variable vectors. We assume X and Y share no variables and have the same length. We use fx (resp. cy) to denote the vector with all variables in X (resp. Y) assigned the min (resp. max) values for their respective domains. Integer vector fxx=v is the result of replacing the value assigned to x in fx to v, and similarly for cyy=v. Functions min(Xi) and max(Xi) return the min and max values in D(Xi) respectively.

The GAC enforcement is based on the following theorems.

Theorem 4. X rlex Y is GAC iff (1) 8x 2 X, fxx=max(x) rlex cy and (2) 8y 2 Y, fx rlex cyy=min(y).

Proof. ()) If X rlex Y is GAC, all values in the domains of variables in X and Y can find supports. Given any value v in the domain of x 2 X, the min values in the domains of all other variables in X and the max values in the domains of variables inYmust be supports of v. In particular, (1) is true. Similarly, (2) is true. (() If (1) is true, then for all values v in D(x): fxx=v rlex cy. Thus all values in the domain of x are supported. Similarly, by (2), all values in the domains of y 2 Y are also supported.

The proof of the following theorem is similar.

Combining Theorems 4 and 5 with 1 respectively, we get the following corollaries.

Corollary 1. X rlex Y is GAC iff (1) 8x 2 X, (fxx=max(x))s lex cys and (2) 8y 2 Y, fxs lex (cyy=min(y))s .

Enforcing GAC on X rlex Y can be achieved by pruning inconsistent values v from the domains of all x 2 X such that (fxx=v)s >lex cys and from the domains of all y 2 Y such that fxs >lex (cyy=v)s . Thus, the upper bounds of all x 2 X and the lower bounds of all y 2 Y are tightened. Note that this does not change fxs and cys as long as no domains become empty. To prune values v from the domains of x 2 X, we do not generate each (fxx=v)s to check if (fxx=v)s >lex cys is true. Similarly, we do not generate each (cyy=v)s to check if fxs >lex (cyy=v)s is true. We utilize three pointers, fxs and cys plus our own rules to prune inconsistent values. Our algorithm resembles more to that of the multiset ordering constraint [Frisch et al., 2009] than that of the lex ordering constraint [Frisch et al., 2002]. The outline of the algorithm follows.

1. Compute fx, cy, fxs and cys .
2. Set the proper values of the three pointers ↵, β and γ (to be defined below) to help prune inconsistent values.
3. Tighten the lower bounds of all y 2 Y.
4. Tighten the upper bounds of all x 2 X.

Variables with singleton domains are automatically assigned. We can check if x is assigned by x▷assigned(), and x▷gq(v) and x▷lq(v) enforce x ≥ v and x  v respectively.

We give the algorithms to enforce GAC with the help of fxs and cys , and illustrate with a running example. Consider two disjoint and same sized variable vectors, in which variables are represented by their domains: X = h¶5♦↪ ¶2↪ 3♦↪ ¶3♦↪ ¶4♦↪ ¶1↪ 2↪ 5♦↪ ¶3♦↪ ¶1↪ 2♦i and Y = h¶2↪ 4♦↪ ¶1↪ 2↪ 3♦↪ ¶3♦↪ ¶2↪ 3♦↪ ¶0↪ 1♦↪ ¶1↪ 2♦↪ ¶0↪ 1♦i. Then fx = h5↪ 2↪ 3↪ 4↪ 1↪ 3↪ 1i, cy = h4↪ 3↪ 3↪ 3↪ 1↪ 2↪ 1i, fxs = h(1↪ 4)↪ (1↪ 6)↪ (2↪ 1)↪ (3↪ 2)↪ (3↪ 5)↪ (4↪ 3)↪ (5↪ 0)i and cys = h(1↪ 4)↪ (1↪ 6)↪ (2↪ 5)↪ (3↪ 1)↪ (3↪ 2)↪ (3↪ 3)↪ (4↪ 0)i.

Algorithm 1 is the top level of the GAC algorithm. This algorithm is called whenever the domain bound of a variable in X or Y is modified. We first get fx and cy using floor() and

Algorithm 1 Reflex(X↪ Y)

• 1: fxs sortinv(floor(X)); cys sortinv(ceiling(Y));
• 2: int ↵ -1; int β -1; int γ -1;
• 3: SetPointer(X,Y,fx,cy,↵,β,γ);
• 4: if ↵ = -2 then return FAILED;
• 6: EnforceY(Y,fx,cy,↵,β,γ);
• 5: else if ↵ = -1 then return SUBSUMED;
• 7: if EnforceX(fx,cy,Xfxs↵ ▷pos,Yfxs↵ ▷pos,↵,β,γ,♣Y♣) = SUBSUMED then return SUBSUMED;
• 8: return GACED;

ceiling() respectively, and generate the sorted index vectors fxs and cys using function sortinv() respectively (line 1). To help enforce GAC, we define the following three pointers to fxs and cys : ↵, β and γ. They are all initialized to -1 (line 2). Algorithm 2 is called (line 3) to set them so that

1. fxs↵ < cys↵ and 8i 2 [0↪ ↵), fxsi = cysi ;
2. fxsβ+1 > cysβ , β ≥ ↵ and 8i 2 (↵↪ β], fxsi = cysi-1 ;
3. fxsγ > cysγ , γ > β and 8i 2 (β↪ γ), fxsi = cysi .

At ↵, fxs <lex cys . If the vectors are equal, ↵ is still -1. If fxs >lex cys , ↵ is set to -2. Pointer β is always larger than or equal to ↵ for pruning inconsistent values from the domains of Xfxs↵ ▷pos and Yfxs↵ ▷pos. For cases where we cannot find such a β, if 8i 2 (↵↪ ♣fxs ♣), fxsi = cysi-1 , β is still -1. Otherwise, β is set to -2. Pointer γ points to the index larger than β such that hfxsβ+1 ↪ ▷▷▷i >lex hcysβ+1 ↪ ▷▷▷i at position γ. If such case is impossible, γ is still -1. In our example, the values of the three pointers are: ↵ = 2, β = 2 and γ = 3.

For space reasons, we skip the description of the simple iteration in Algorithm 2, which achieves the definition of ↵, β and γ described above. One thing to note in Algorithm 2 is that, if 8j  i↪ fxsj = cysj (lines 3-4), x = Xfxsi ▷pos and y = Ycysi ▷pos are set to their min and max values respectively (lines 5-6). The reason is if x is assigned a larger value v than min(x) or y is assigned a smaller value v than max(y), (fxx=v)s >lex cys and fxs >lex (cyy=v)s . Thus, in our example, X4, X6, Y4 and Y6 are all enforced to be 1.

In Algorithm 1, if ↵ is set to -2 (line 4), fxs >lex cys . The constraint is FAILED (line 4) according to Corollary 2. If ↵ is still -1 (line 5), fxs = cys and all variables in X and Y are set to their min and max values respectively. X = Y and the constraint is SUBSUMED (line 5). Otherwise, Algorithms 3 and 4 are called to prune inconsistent values in the domains of variables in Y and X respectively (lines 67). If Algorithm 4 returns SUBSUMED, X <rlex Y for any possible assignment and the constraint is SUBSUMED (line 7). After the enforcements, the constraint is GACED (line 8).

Algorithm 3 prunes inconsistent values from the domains of variables in Y. Consider all non-assigned variables y = Yi where i < fxs↵▷pos (lines 1-2). If y is assigned a value v  fxs↵▷val, (v↪ i) is moved to the kth position of (cyy=v)s where k  ↵ and fxs >lex (cyy=v)s at position k. In our example, if Y0 = 2, (2↪ 0) is moved to the second position of (cyY0=2)s and fxs >lex (cyY0=2)s at this position. We thus enforce y > fxs↵▷val (line 2). Value 2 is pruned from D(Y0). Consider all non-assigned variables y = Yi where

Algorithm 2 SetPointer(X,Y,fx,cy,↵,β,γ)

1: int i 0; int j 0; 2: while i < ♣X♣, j < n do ¶ 3: if fxsi = cysj then ¶ 4: if ↵ = -1 then ¶ 5: Xfxsi ▷pos fxsi ▷val; 6: Ycysj ▷pos cysj ▷val;♦♦ 7: else if fxsi < cysj then 8: if ↵ = -1 then ¶↵ i; j--;♦ 9: else ¶ 10: if β = -1 then β -2; 11: break;♦ 12: else if ↵ = -1 then ¶↵ -2; break;♦ 13: else if β = -1 then ¶β j; i--;♦ 14: else ¶γ i; break;♦ 15: i++; j++;♦ 16: return;

i > fxs↵▷pos (lines 3-4), if y is assigned a value v < fxs↵▷val, (v↪ i) is moved to the kth position of (cyy=v)s where k  ↵ and fxs >lex (cyy=v)s at this position. In our example, if Y5 = 1, (1,5) is moved to the first position of (cyY5=1)s and fxs >lex (cyY5=1)s at this position. We thus enforce y ≥ fxs↵▷val (line 4). In our example, Yi ≥ 2 for all i > 1. Value 1 is pruned from D(Y5).

For non-assigned variable y = Yfxs↵ ▷pos (line 6), there are five cases. If β  -1 (line 7), fxs lex (cyy=fxs↵ ▷val)s . We only need to enforce y ≥ fxs↵▷val (line 7). Otherwise, if fxs↵▷pos = cysβ ▷pos (line 8), items in fxs and (cyy=fxs↵ ▷val)s are pairwise equal from positions 0 to β. If γ = -1 (line 9), fxs lex (cyy=fxs↵ ▷val)s . Thus we only need to enforce y ≥ fxs↵▷val (line 9). Otherwise (line 10), fxs >lex (cyy=fxs↵ ▷val)s at position γ, we enforce y > fxs↵▷val (line 10). For case fxs↵▷pos 6= cysβ ▷pos and (max(y)↪ fxs↵▷pos) occurring after position β at cys (line 11), if y is assigned a value v < fxs↵▷val, (v↪ fxs↵▷pos) is moved to the kth position of (cyy=v)s where k  ↵ and fxs >lex (cyy=v)s at position k. If y is assigned fxs↵▷val, (fxs↵▷val↪ fxs↵▷pos) is moved to position ↵ in (cyy=fxs↵ ▷val)s . Now fxs↵ = (cyy=fxs↵ ▷val)s↵ and fxs >lex (cyy=fxs↵ ▷val)s at position β + 1. We thus enforce y > fxs↵▷val (line 12). This case occurs in our example since fxs↵▷pos = 1 and cysβ ▷pos = 5, and (3↪ 1) occurs after position β in cys . If Y1 is assigned value 1, (1,1) is moved to the zeroth position of (cyY1=1)s and fxs >lex (cyY1=1)s at this position. If Y1 is assigned value 2, (2,1) is moved to the second position of (cyY1=2)s and fxs >lex (cyY1=2)s at position 3 since (3↪ 2) > (2↪ 5). We thus enforce Y1 > 2 and values 1 and 2 are pruned from D(Y1). Otherwise (line 13), we only need to enforce y ≥ fxs↵▷val (line 13).

Algorithm 4 prunes inconsistent values only from the domain of x = Xfxs↵ ▷pos. All values in the domains of other variables x0 in X already have supports since (fxx0=max(x0 ))s <lex cys at position ↵. If x is assigned (line 1) and Yfxs↵ ▷pos is always larger than fxs↵▷val (line 2),

Algorithm 3 EnforceY(Y,fx,cy,↵,β,γ)

1: for each i in [0↪ fxs↵▷pos) do 2: if not Yi.assigned() then Yi▷gq(fxs↵▷val + 1); 3: for each i in (fxs↵▷pos↪ n) do 4: if not Yi.assigned() then Yi▷gq(fxs↵▷val); 5: y Yfxs↵ ▷pos; 6: if not y.assigned() then 7: if β  -1 then y▷gq(fxs↵▷val); 8: else if fxs↵▷pos = cysβ ▷pos then 9: if γ = -1 then y▷gq(fxs↵▷val); 10: else y▷gq(fxs↵▷val + 1); 11: else if (max(y)↪ fxs↵▷pos) > (cysβ ▷val↪ cysβ ▷pos) 12: then y▷gq(fxs↵▷val +1); 13: else y▷gq(fxs↵▷val); 14: return;

Algorithm 4 EnforceX(fx,cy,x,y,↵,β,γ,n)

1: if x▷assigned() then 2: if min(y) > fxs↵▷val then return SUBSUMED; 3: else if β = -1 then 4: if cysn-1 ▷pos < fxs↵▷pos then 5: x▷lq(cysn-1 ▷val - 1); 6: else x▷lq(cysn-1 ▷val); 7: else if β > -1 then 8: if fxs↵▷pos = cysβ ▷pos then 9: if γ = -1 then x▷lq(cysβ ▷val); 10: else x▷lq(cysβ ▷val - 1); 11: else if fxs↵▷pos < cysβ ▷pos then x▷lq(cysβ ▷val); 12: else x▷lq(cysβ ▷val - 1); 13: return;

there always have X <rlex Y at position ↵. The constraint is SUBSUMED (line 2). Otherwise, if β = -1 (line 3), this means fxsi = cysi-1 for all i > ↵. We need to make sure (x↪ fxs↵▷pos)  cysn-1 and x is enforced accordingly (lines 4-6). If β = -2, all values in the domain of x are supported. If β > -1 (line 7), there are four cases. If fxs↵▷pos = cysβ ▷pos (line 8), items in (fxx=fxsβ ▷val)s and cys are pairwise equal from positions 0 to β. If γ = -1 (line 9), (fxx=fxsβ ▷val)s lex cys . Thus we only need to enforce x  fxsβ ▷val (line 9). Otherwise (line 10), x < fxsβ ▷val (line 10). For the case fxs↵▷pos < cysβ ▷pos (line 11), if x is assigned any value v > cysβ ▷val, (v↪ fxs↵▷pos) is moved to the kth position of (fxx=v)s where k ≥ β and (fxx=v)s >lex cys at position β. We thus enforce x  fxsβ ▷val (line 11). This case occurs in our example since 1 < 5. If X1 = 3, (3↪ 1) replaces (2↪ 1) in (fxX1=3)s and (fxX1=3)s >lex cys at position 2. We thus enforce X1  2 and value 3 is pruned from D(X1). If fxs↵▷pos > cysβ ▷pos, we enforce x < fxsβ ▷val (line 12).

After the enforcements, X and Y in our example are updated to: X = h¶5♦↪ ¶2♦↪ ¶3♦↪ ¶4♦↪ ¶1♦↪ ¶3♦↪ ¶1♦i and Y = h¶4♦↪ ¶3♦↪ ¶3♦↪ ¶2↪ 3♦↪ ¶1♦↪ ¶2♦↪ ¶1♦i. X rlex Y is GAC.

Theorem 6. Algorithm 1 enforces GAC of Xrlex Y.

Proof. Algorithm 1 always terminates. All values pruned in Algorithm 1 are inconsistent values. We now prove values left always have supports. If ↵ = -2, the constraint is unsatisfiable according to Corollary 2. If ↵ = -1 after running Algorithm 1, all variables in X and Y are assigned (lines 5-6 in Algorithm 2), X = Y. If ↵ > -1, based on Corollary 1, we only need to prove for any x 2 X and y 2 Y, (fxx=max(x))s lex cys and fxs lex (cyy=min(y))s . (1) Consider all variables x = Xfxsi ▷pos where i 6= ↵, (fxx=max(x))s <lex cys at ↵. (2) Consider variable x = Xfxs↵ ▷pos. If x is not assigned, there are four cases. If β = -1, (fxx=max(x))s = cys or (fxx=max(x))s <lex cys at the position where (max(x)↪ fxs↵▷pos) appears in (fxx=max(x))s . If β = -2, (fxx=max(x))s <lex cys at the least position among where (max(x)↪ fxs↵▷pos) appears in (fxx=max(x))s and where β is set to -2 in cys in Algorithm 2. If fxs↵▷pos = cysβ ▷pos and γ = -1, (fxx=max(x))s = cys or (fxx=max(x))s <lex cys at the position where (max(x)↪ fxs↵▷pos) appears in (fxx=max(x))s . If fxs↵▷pos = cysβ ▷pos and γ 6= -1, or fxs↵▷pos 6= cysβ ▷pos, (fxx=max(x))s <lex cys at the position where (max(x)↪ fxs↵▷pos) appears in (fxx=max(x))s . (3) Consider all variables Yi where i 6= fxs↵▷pos, fxs <lex (cyYi=min(Yi))s at ↵. (4) Consider variable y = Yfxs↵ ▷pos. If y is not assigned, there are three cases. If β  -1, or fxs↵▷pos = cysβ ▷pos and γ = -1, fxs = (cyy=min(y))s or fxs <lex (cyy=min(y))s at ↵. If fxs↵▷pos = cysβ ▷pos and γ 6= -1, or fxs↵▷pos 6= cysβ ▷pos and (max(y)↪ fxs↵▷pos) occurs after β at cys , fxs <lex (cyy=min(y))s at ↵. If fxs↵▷pos 6= cysβ ▷pos and (max(y)↪ fxs↵▷pos) occurs before β at cys , fxs <lex (cyy=min(y))s at ↵ if min(y) > fxs↵▷val and at ↵ + 1 otherwise.

Theorem 7. Algorithm 1 runs in O(nlog(n)) time for constraint X rlex Y, where ♣X♣ = ♣Y♣ = n.

Proof. Algorithms floor() and ceiling() have O(n) time complexity respectively. Algorithm sortinv() runs in O(nlog(n)). SetPointer() runs in O(n). EnforceY() runs in O(n). EnforceX() runs in O(1). The total is O(nlog(n)).

Theorem 8. The space complexity of Algorithm 1 is O(n).

Proof. Algorithms floor(), ceiling() and sortinv() have space O(n) respectively. Algorithms SetPointer(), EnforceY() and EnforceX() have space O(1) respectively.

GAC enforcement of constraint X <rlex Y under conditions where X and Y do or do not have the same length can be achieved by changing EnforceY() and EnforceX() slightly. We do not show them in here due to space limitation.

5 Reflex in Symmetry Breaking

Given a symmetry group G. Symmetry breaking method ReflexLeader adds one reflex ordering constraint, rlex, per variable symmetry g 2 G according to a fixed variable order. Since reflex is a total ordering, we have the following.

Theorem 9. ReflexLeader is sound and complete.

In this paper, we use ReflexLeader and LexLeader also to break only a given subset of symmetries.

In matrix problems, lex ordering the rows (columns) breaks all the row (column) symmetries. Similarly, reflex ordering the rows (columns) breaks all the row (column) symmetries since it is a total order. Thus, we can have DOUBLEREFLEX by only adding reflex ordering constraints to break adjacent rows and columns interchangeability.

ReflexLeader also has identical pruning power as LexLeader in the following circumstance.

Theorem 10. Given a CSP P = (X↪D↪C) with symmetry group G, D(x) ✓ E for all x 2 X and ♣E♣ = 2. ReflexLeader and LexLeader have the same solution and node pruning powers when both are enforced GAC and based on the same fixed variable and value orders.

Proof. We prove A rlex B is GAC iff A lex B is GAC for any variable vectors A and B. Any support in A rlex B for a value v can be transformed to a support in A lex B according to Theorem 3. The reverse is also true.

Even though ReflexLeader and LexLeader generate the same search tree with Boolean domains, the GAC algorithm of X lex Y is O(n) where n is the size of X and Y. When we use DOUBLEREFLEX and DOUBLELEX to break the matrix symmetries of the 0/1 model of the Balanced Incomplete Block Design problem [Flener et al., 2001], they leave the same search tree but DOUBLELEX will run slightly faster than DOUBLEREFLEX.

Precedence [Law and Lee, 2004] constrains a value s to precede another value t in an integer variable vector X, which means that if there exists j such that Xj = t, then there must exist i < j such that Xi = s. We prove ReflexLeader is safe to combine with Precedence.

Theorem 11. Given a CSP P = (X↪D↪C). If P has variable symmetry group G and value interchangeability H. Using ReflexLeader to break G and Precedence to break H is sound as long as they are based on the same fixed variable and value orders.

Proof. Suppose they are based on the variable and value order Γ. We prove that the reflex least solution according to Γ in each solution symmetry class of symmetry group G ◦ H satisfies Precedence. Suppose S is the reflex least solution in a symmetry class and sequenced according to the variable order in Γ. Suppose further values i < j according to Γ and (a) j occurs earlier than i in S or (b) j occurs but i does not occur in S. In case (a), we interchange i and j in S and get a solution R. In case (b), we replace j by i in S and get a solution R. All the other values in S and R occur at the same positions. We simply delete all these values out to get S0 and R0 respectively. Now the first value of S0 is j and the first value of R0 is i, the first i occurs earlier in R0 than that in S0 . Since i < j, R0 <rlex S0 and R <rlex S which contradicts with S being the reflex least solution.

The multiset ordering constraint [Frisch et al., 2009] ensures the values taken by two variable vectors, when viewed as multisets, are ordered. All static symmetry breaking methods on column (row) symmetries are safe to combine with multiset ordering constriants on row (column) symmetries.

Theorem 12. Suppose M is a static symmetry breaking method. In matrix problems, multiset ordering the rows (columns) and using M to break the columns (rows) interchangeability are sound no matter what variable and value orders are used in each method.

Proof. Since interchanging columns (rows) does not change the occurrences of values in each row (column), their combination is sound.

More specifically, the reflex ordering constraint is safe to combine with the multiset ordering constraint.

Corollary 3. In matrix problems, multiset ordering the rows (columns) and reflex ordering the columns (rows) are sound regardless the variable and value orders used.

Proposition 1 implies that reflex and lex orderings can conflict with each other. Thus ReflexLeader cannot be combined with LexLeader in general.

6 Experimental Results

This section gives four experiments. All static symmetry breaking constraints are posted based on the rowwise variable order and min value order. We compare ReflexLeader with the efficient and widely used static method LexLeader given the same subset of symmetries. All reflex and lex ordering constraints in the experiments can be simplified to constraints on two disjoint and same sized variable vectors.

In searching, we first use the standard rowwise variable order (Rowwise) and min value order. Other orderings, e.g. snake ordering, are also applicable. We skip them for lack of space. We also exploit the smallest min value first (MinMin) variable order and min value order, which align well with ReflexLeader since it always chooses the min value among the values in the domains of all variables to branch.

All experiments are conducted using Gecode Solver 4.2.0 on Intel C2D E8400 3.0Ghz processors with 7GB. In our tables, #s denotes the number of solutions, #f denotes the number of failures and t denotes the runtimes. For the last two experiments, an entry with the symbol "-" indicates that the search timed out after the 1-hour limit. The best results are highlighted in bold.

Matrix Symmetries. To compare ReflexLeader and LexLeader without effects of other factors, we first solve the unconstrained matrix problem (n↪m↪ d) which contains only n ⇥ m variables but no constraints. Error Correcting Code-Lee Distance (ECCLD) problems with parameters (n↪ c↪ b) are also tested using the same model by Lee and Zhu [2014]. Both problems have matrix symmetries. We thus apply ReflexLeader and LexLeader to break the same subset of matrix symmetries used by Lee and Zhu [2015]. Note that [Lee and Zhu, 2015] breaking this subset of symmetries by LexLeader performs better than DOUBLELEX which has similar performance with SNAKELEX [Katsirelos et al., 2010], so that their results are not reported here. The unconstrained matrix problem also has value interchangeability and Precedence can thus be exploited.

In the unconstrained matrix problem (Table 1), the solution set size for ReflexLeader is on average 29% of that of LexLeader. In ECCLD (Table 2), the solution set size for ReflexLeader is reduced by 52% on average. This demonstrates ReflexLeader (and its combination with Precedence) can break more composition symmetries than that of LexLeader (and its combination with Precedence). The runtimes are 3.45 and 3.76 times faster and 1.22 and 4.16 times faster on average under the two orderings for the two problems respectively. ReflexLeader under MinMin runs 1.66 times faster than LexLeader under Rowwise in ECCLD. Note that ReflexLeader and LexLeader have no failures under their respective search orders in the unconstrained matrix problem.

Geometric Symmetries. NNQueen [Kelsey et al., 2004] and Diagonal Latin Square [Harvey, 2005] of size n are tested. Both are modeled with n2 variables and both have 8 geometric symmetries, value interchangeability and their compositions. We first use the VAR constraints [Puget, 2005a; 2005b], which are simplified from LexLeader, and

Table 4: Diagonal Latin Square

n

VAR+Precedence ReflexLeader+Precedence

6

Rowwise MinMin Rowwise MinMin

#s #f t #s #f t #s #f t #s #f

t

128

3,000 0.02 128 128,077,130 467.85

64

2,034 0.02 64 71,959,952 266.81

7 171,200 1,412,605 11.36

-

-

- 85,600 924,584 7.93

-

-

-

Precedence. Note that Precedence eliminates all variable symmetries as it specifies that the first row must be h1↪ ▷▷▷↪ ni. And the VAR constraints cannot further delete symmetric solutions. ReflexLeader on symmetry d1 (reflection on the diagonal), however, can further prune symmetric solutions. We thus use ReflexLeader to break d1 and also Precedence to break value interchangeability.

In Tables 3 and 4, after posting ReflexLeader on d1, half of the solutions of VAR+Precedence is further eliminated. The runtimes are 1.64 and 1.43 times faster for the largest instance under Rowwise for the two problems respectively. This shows again the combination of ReflexLeader and Precedence breaks more composition symmetries than that of LexLeader and Precedence. MinMin happens to conflict with the problem constraints. Although MinMin is aligned with ReflexLeader, our method has the flexibility of resorting to other search orders that cooperate well with problem constraints, in this case Rowwise. This shows the advantage of static symmetry breaking methods: to be able to combine with other search heuristics.

Discussions. The experiments show that ReflexLeader can break more composition symmetries in partial symmetry breaking than LexLeader can. The reason is that the canonical solutions chosen by different ReflexLeader constraints vary a lot more than those of LexLeader. Thus the intersection of ReflexLeader's canonical solutions is smaller in size than that of LexLeader. We also show that the combination of ReflexLeader and Precedence can also break more composition symmetries in partial symmetry breaking than that of LexLeader and Precedence. The reason is the canonical solutions chosen by ReflexLeader have less intersections with those chosen by Precedence. Thus ReflexLeader constraints have better interactions amongst themselves as well as with the Precedence constraint.

Multiset ordering constraints alone do not perform well to break symmetries in matrix problems [Frisch et al., 2009] since multiset ordering is only a partial order. People often combine multiset ordering constraints with lex ordering constraints. We show no results of the combinations of multiset ordering constraint with the two total ordering constraints due to space limitation. When combined with multiset ordering on the rows (columns), ReflexLeader and LexLeader can only post symmetries on columns (rows) interchangeability. This means only a linear and small number of symmetries are given to them. Results shows their combinations with multiset ordering constraints result in the same number of solutions for ECCLD. ReflexLeader is only slightly better than LexLeader for the unconstrained matrix problem when combined with multiset ordering constraints and Precedence. When given their aligned heuristics, the partial ReflexLeader alone runs 1.45 and 2.72 times faster than the combination of LexLeader and multiset ordering constraints on average for ECCLD and the unconstrained matrix problem (breaking also value interchangeability) respectively.

We also do not compare the performance of DOUBLEREFLEX and DOUBLELEX for matrix problems for two reasons. First, Lee and Zhu [2015] show that the subset of symmetries we give to ReflexLeader and LexLeader in here is better than adjacent rows and columns interchangeability, with which ReflexLeader and LexLeader are simplified to DOUBLEREFLEX and DOUBLELEX respectively. Second, with more symmetries posted, the difference on the performances of ReflexLeader and LexLeader is more prominent.

ReflexLeader has the advantage to prune more composition symmetries in partial symmetry breaking. The MinMin heuristic matches well with the propagation of reflex ordering constraints. However, MinMin is not a good heuristic to solve many CSP problems. Often, it does not cooperate well with the problem constraints. When the reduction on the search tree size is small and the problem constraints are in conflict with MinMin, using ReflexLeader and MinMin to solve the problem would give no benefits.

7 Conclusion

Our contributions are four fold. First, we introduce the reflex total ordering on integer vectors and compare it with lex. Second, we present the reflex ordering constraint and give an efficient GAC algorithm. Third, we propose a new static symmetry breaking method ReflexLeader and give conditions when ReflexLeader is safe to combine with the Precedence and multiset ordering constraints. Fourth, we give experimentations to show substantial advantages of the reflex ordering over the lex ordering in partial symmetry breaking.

Acknowledgement

We are grateful to the anonymous referees of IJCAI-16 for their comments. This research has been supported by the grant CUHK413713 from the Research Grants Council of Hong Kong SAR.