DoubleLex Revisited and Beyond

1 Introduction

Many constraint satisfaction problems can be formulated as a matrix model [Flener et al., 2001], which has the decision variables are organized in the form of a matrix with rows and columns. Some such problems consist of matrix symmetries [Flener et al., 2002], in which rows and columns in a solution matrix can be swapped arbitrarily to form symmetrically equivalent solutions. DoubleLex [Flener et al., 2002] is an efficient method for breaking matrix symmetries by posting a linear number of lexicographical ordering constraints. While Flener et al.[2002] demonstrate that DoubleLex can eliminate all row and column symmetries, its observed good performance [Katsirelos et al., 2010] in practice suggests a stronger theoretical pruning guarantee.

In this paper, we propose the notion of Maximum Residue (MR), which is the maximum number of remaining solutions over all symmetry classes of a symmetry group, as a measure of the strength of a symmetry breaking method. A major result is a factorial improvement of the DoubleLex's MR upper bound from m!n! - (m! + n!) to min(m!, n!) for an m × n matrix model. We further show that this bound is tight in general. Our result implies that DoubleLex works well when min(m, n) is relatively small. When min(m, n) is large, our analysis suggests the need for more symmetry breaking constraints over those imposed by DoubleLex. Furthermore, we study the MR bounds of SwapNext and SwapAny[Smith, 2014], which are two slight extensions upon DoubleLex by further breaking products (compositions) of a row and a column symmetries.

Obviously, SwapNext and SwapAny subsume DoubleLex in symmetry breaking power but with similar complexity in terms of MR lower bounds. Our theoretical understanding of these three methods suggests guiding principles on the efficiency of the methods when applied on matrix models of varying sizes as defined by the matrices' dimensions. Experimental results confirm (a) the accuracy of our theoretical predictions and (b) the overhead of extra symmetry breaking constraints in SwapNext and SwapAny can be nicely compensated in practice in certain scenarios.

2 Background

A constraint satisfaction problem (CSP) is a triple P = (X,D,C) where X = {x1, . . . , xn} is a set of variables, each of which takes value from its domain D(xi), and C is a set of constraints each specifying allowed value combinations over a set of variables. An assignment {xi = vi|i ∈ {1, . . . , n}} instantiates each variable xi with vi ∈ D(xi). A solution θ of P is an assignment that satisfies all constraints in C. We denote the set of all solutions of P as sol(P).

A symmetry is a transformation from assignments to assignments and maps a solution to a solution. A symmetry group GΣ is generated by a set of symmetry generators Σ under composition. We use id to denote the identity in GΣ. A symmetry class S of a group G is a set of solutions that are symmetrically equivalent: a solution s ∈ S if and only if g(s) ∈ S for every g ∈ G. Equivalently speaking, if a solution s ∈ S, then S = {g(s)|g ∈ G}. The symmetry group of an m× n matrix model can be generated by a set of row symmetry generators {ri|i ∈ {1, . . . ,m- 1}} and a set of column symmetry generators {cj |j ∈ {1, . . . , n-1}}, where ri switches the i-th and the (i+1)-st rows and cj switches the j-th and the (j+1)-st columns. When the context is clear, we use Grow to denote the group G{r1,...,rm-1}, Gcol for G{c1,...,cn-1}, and Gmat for the matrix symmetry group.

A symmetry breaking constraint removes symmetries, and therefore also symmetric solutions in a CSP. A set of symmetry breaking constraints C sb is sound with respect to G if at least one solution in each symmetry class of G in sol(P) remains in sol(P,C sb ) = sol(P ′ ), where P ′ = (X,D,C ∪ C sb ). A set of symmetry breaking constraints C sb is complete with respect to G if exactly one solution in each symmetry class of G remains in sol(P, C sb ).

3 DoubleLex Revisited

DoubleLex [Flener et al., 2002] posts (m+n-2) constraints requiring a solution to be both row-wise and column-wise lexicographically ordered. We concatenate the rows of a matrix from the top to the bottom to form a string for lexicographic comparison. More specifically, the following sets of constraints are posted for an m × n matrix model:

where r′i s are row symmetry generators that swap the i-th row and (i + 1)-st row, and c′j s are column symmetry generators that swap the j-th column and (j + 1)-st column.

3.1 Improved Bound of Remaining Solutions

Flener et al.[2002] prove that all row symmetries (of size m!) and column symmetries (of size n!) are removed, thus potentially leaving m!n! - (m! + n!) solutions in each symmetry class. However, the method works surprisingly well in practise and leaves much fewer solutions. In the following, we provide further insight to the good performance by improving the best known upper bound to min(m!, n!).

Theorem 1. At most min(m!, n!) distinct solutions satisfy DoubleLex in any symmetry class of Gmat for an m× n matrix.

Proof. Given a solution θ of a symmetry class, the symmetry class of θ can be generated by applying each symmetry in Gmat upon θ. So the symmetry class of θ is {g(θ)|g ∈ G}. We construct a table, where the rows are indexed by row symmetries from Grow and the columns are indexed by column symmetries from Gcol. Since composition of a row symmetry and a column symmetry is commutative, each symmetry g ∈ Gmat can be uniquely written as the product of a row symmetry and column symmetry: g = rpi cpj where rpi ∈ Grow and cpj ∈ Gcol (note that rpi is not necessarily a generator, and similarly for cpj ). We place the solution g(θ) = rpi cpj (θ) at the cell on the row indexed by rpi and the column indexed by cpj thus the table encodes exactly the symmetry class of θ (shown in Table 1).

Among the solutions on the same row of the table, at most one distinct solution satisfies DoubleLex. Assume the contrary and consider the following two distinct solutions on the same row indexed by rpt that both satisfy DoubleLex:

where cp1 ̸= cp2 . Observe that by applying a column symmetry cp2 c-1 p1 on g1(θ), we get g2(θ):

That means by only permuting the columns of a columnwise lexicographically ordered solution g1(θ), the resulting columns are still lexicographically ordered. Lexicographic ordering is a total order and this leads to a contradiction if the two solutions are distinct. So g1(θ) and g2(θ) must be the same. In other words, there can only be at most one solution placed on each row of the table. Similarly, there can only be one distinct solution on each column of the table. We count the number of remaining solutions in the table either by rows or columns and thus there are at most min(m!, n!) solutions in the table.

The theorem give a factorial improvement to the best known upper bound of DoubleLex. The proof has no dependence upon problem constraints, and should apply to any problems with matrix symmetries. Moreover, it implies that the strong guarantee maintains as long as the ordering is total. We immediately have the following more general theorem on any total ordering used in symmetry breaking:

Theorem 2. Given an m× n matrix model and a total order ≺ on strings. At most min(m!, n!) distinct solutions are both rows and columns ordered with respect to ≺ in any symmetry class of Gmat.

By the above theorem, we can order rows and columns using any total order for symmetry breaking to generate other methods enjoying the same theoretical guarantee as DoubleLex. Concretely, we refer to the constraints that order both rows and columns using Reflex [Lee and Zhu, 2016] and Gray code Ordering [Narodytska and Walsh, 2013] (for binary strings) as DoubleReflex and DoubleGrayCode.

Corollary 1. At most min(m!, n!) distinct solutions satisfy DoubleReflex in any symmetry class of Gmat for an m× n matrix.

Corollary 2. At most min(m!, n!) distinct solutions satisfy DoubleGrayCode in any symmetry class of Gmat for an m× n 0/1 matrix.

3.2 MaximumResidue

The strength of a symmetry breaking method is commonly evaluated by the number of remaining solutions. It shows an overall behaviour upon all symmetry classes. Less effort is made to study what really happened within each symmetry class. Indeed, the effects of a set of symmetry breaking constraints on different symmetry classes are different. In some symmetry class, some symmetries are removed yet they remains in another symmetry class. Zeynep [2004] pointed out it is difficult to theoretically study how many symmetries are removed. The above analysis gives a possible direction to progress. We can directly characterize the number of remaining solutions in a symmetry class and consider it as an instructive metric to measure the power of a symmetry breaking method. We define the following notion to capture the power of a set of symmetry breaking constraints C.

Definition 1. Given an m × n unconstrained matrix where each variable has a domain {0, ..., (d - 1)} and a set of symmetry breaking constraints C. We define the Maximum Residue as

where SC(m, n, d) denotes all symmetry classes of an m×n unconstrained matrix with domains {0, ..., (d - 1)}.

MR(m, n, d, C) gives the maximum number of remaining distinct solutions satisfying C over all symmetry classes. Though characterizing only the worst solution class, MR gives a manageable analysis and serves as a supplement to existing measures of strengths of symmetry breaking constraints. A symmetry breaking method having a smaller number of maximum residue generally leaves fewer redundant symmetric solutions and results in a shorter search time. The maximum residue notion captures the symmetry breaking power in theory, and we will show how it agrees with practical performance in the experimental section.

We now give a property of MR.

Property 1. MR(m, n, d, C) ≤ MR(m, n, d′ , C) when d ≤ d′

Without loss of generality, we denote the number of rows as m, the number of columns as n, and assume m ≤ n from now on to ease our discussion. We know from Theorem 1 that MR(m, n, d,DoubleLex) ≤ m!. We provide a construction showing that the bound is tight. Namely, we show a symmetry class of an m × m unconstrained matrix where there are exactly m! solutions satisfying DoubleLex.

Construction 1 Construct an m × m matrix where all elements except those on counter diagonal are zero, and the counter diagonal is filled by any permutation of {1, 2, ..., m}. For example, we construct the following matrix for m = 3:

The matrix satisfies DoubleLex. In fact, any such matrix whose counter diagonal is filled with a permutation of {1, 2, 3} satisfies DoubleLex. Obviously one can transform one such matrix to another by permuting the rows and columns, and thus they are in the same symmetry class. There are exactly m! permutations and therefore we have a symmetry class with m! remaining solutions. Obviously, we construct such matrix with more than m columns by appending zero columns to the construction.

Theorem 3. MR(m, n, d,DoubleLex) =m! for n ≥ m, d ≥ m + 1.

3.3 MR as Performance Indicator

MR(m, n, d, C) captures the worst case behaviour of C and it can be used to indicate the empirical performance of C. It is observed in [Flener et al., 2002] that enforcing lexicographical ordering only between columns (CLex) greatly outperforms enforcing lexicographical ordering only between rows (RLex) on Balanced Incomplete Block Designs (BIBD) instances. The authors conjectured it to be related to the tight scalar product constraint on pairs of rows. We observe BIBD instances involve skew matrices whose number of columns is much larger than its number of rows. We believe this is also a culprit to the peformance difference since RLex has a significantly larger MR (n!) than CLex (m!).

A symmetry breaking method with a smaller MR is expected to perform better in practise. However, we also observe the performance difference between DoubleLex and CLex that have the same maximum residue. We believe this advantage comes from the common wisdom in symmetry breaking: Breaking an "appropriate" number of extra symmetry is beneficial as the time saving from avoiding exploration of symmetric solutions and failures compensates the extra propagation cost. McDonald and Smith [2002] mentioned that the advantage disappears when the size of symmetries used reach a certain point beyond which enforcing symmetry breaking is no more worthwhile. DoubleLex is closer to the optimum tradeoff point than CLex, but we believe breaking more symmetries over DoubleLex can further improve the performance in certain circumstances. We study the MR bounds of two extensions upon DoubleLex.

4 Beyond DoubleLex

We study SwapNext and SwapAny[Smith, 2014] which breaks extra composition symmetries that are products of a row and a column generators.

4.1 SwapNext and SwapAny

We use rowwise order to concatenate the rows of the matrix.

Definition 2. SwapNext posts the following sets of constraints for an m × n matrix model:

The second set of (m-1)(n-1) constraints break a set of composition symmetries that are products of a row symmetry generator and a column symmetry generator.

SwapNext considers only products of a row and a column symmetries that swap adjacent rows/columns. SwapAny further extends the idea to breaking products of row symmetries and column symmetries that swap any pairs of rows and columns.

Definition 3. SwapAny posts the following sets of constraints for an m × n matrix model:

where ri1,i2 swaps the i1-th row and i2-th row, and cj1,j2 swaps the j1-th column and j2-th column.

The (m2 )(n2 ) constraints in (4) break a set of composition symmetries that are products of a row symmetry that swaps two rows and a column symmetry that swaps two columns.

SwapAny is stronger than SwapNext, and SwapNext is stronger than DoubleLex. We are interested in whether breaking these two sets of extra composition symmetries helps lower the maximum residue. We give bounds of maximum residue of SwapNext and SwapAny in the next section.

4.2 MR Bounds

The two methods naturally inherit the MR bound from DoubleLex, and we have MR(m, n, d, SwapNext) ≤ m! and MR(m, n, d, SwapAny) ≤ m!. We are curious if smaller upper bounds exist but we found that m! is in fact a tight upper bound for both methods when d = m + 1.

Proof. We prove both theorems by constructing a symmetry class where we can identify m! distinct solutions satisfying SwapAny (and therefore satisfying SwapNext too).

We construct a matrix by duplicating the columns of Construction 1 and order them lexicographically. For example, we have the following matrix for m = 3 (so the number of columns n = 2m):(0 0 0 0 1 1

Obviously the matrix satisfies DoubleLex. We can easily check by computers that the matrix also satisfies SwapAny thus also SwapNext. The example shows a way to construct such matrix: The matrix should have multiples copies of columns with one non-zero entry. Columns with different non-zero entry should have their entries appear on different rows. We can create copies of m such distinct columns and pack them into an m×2m matrix. There are m! such distinct matrices and they all belong to the same symmetry class. we can construct the desired matrix with more than 2m columns by padding zero columns.

Without restrictions on n and d, the worst cases of MRs of SwapNext and SwapAny equal that of DoubleLex. As many matrix problems involves 0/1 matrix, it is also interesting to see if restricting domain size yields a better upper bound. Unfortunately, the bounds cannot be improved belowm!.

Proof. We use the same idea as in the previous constructions by creating distinct columns. However, the domain is restricted to {0, 1}. We use sequences of 1′ s of different lengths to "represent" distinct values. We construct such a matrix for m = 3.

The matrix satisfies SwapAny. And similarly we can prove m! solutions within this symmetry class satisfy SwapAny. The construction requires 2 + . . . + (m + 1) = m(m+3) 2 columns. Appending zero columns on the left can produce matrices of more than m(m+3) 2 columns.

The flexibility provided by the two unrestricted parameters n and d enables the existence of worst cases where SwapNext and SwapAny hit the bound. The MRs of all three methods grow more than exponentially. We now study if the asymptotic behaviour can be improved when restricting n and d together. We study the case where m = n and d = 2.

For DoubleLex, a construction is given in [Katsirelos et al., 2010] showing a symmetry class of a 2m×2m binary matrix where m! distinct solutions satisfy DoubleLex. The construction packs two identity matrices I, one matrix of zeroes O and an arbitrary permutation matrix P (all of size m×m as the subscripts show) together as follows.

Equivalently speaking, there exists a symmetry class of an m × m binary matrix where ⌊ m2 ⌋! solutions satisfy DoubleLex. So we have MR(m, m, 2, DoubleLex) ≥ ⌊ m2 ⌋!.

How about SwapNext and SwapAny? In fact, we can show their growth is at least exponential in √m.

Proof. For any m being a multiple of 4, we can construct a matrix by packing some identity matrices, zero matrices and an arbitrary permutation matrix P of appropriate sizes as follows.

where

It can be easily verified that the matrix satisfies SwapNext. We obtain other distinct solutions within the same symmetry class for different choice of the permutation matrix Pm/4 so there are at least ( m4 )! solutions. When m is not a multiple of 4, we can construct such matrix for k = (⌊ m4 ⌋)∗4 and further append zero rows and columns to construct the matrix of size m×m. To sum up, we can always construct a symmetry class of an m×m matrix where at least (⌊ m4 ⌋)! solutions satisfy SwapNext.

Proof. We can use the same construction technique in proving Theorem 7. We can construct a k × k(k+3) 2 matrix as a core and append zero rows and columns to obtain an m×m matrix. As the core matrix resides in an m × m matrix, we can pick the largest k where k(k+3) 2 ≤ m holds. Thus k = ⌊ √8m+9-3 2 ⌋ ≥ (⌊√2m- 32 ⌋). The symmetry class has

4.3 Discussion

We show the maximum residues of SwapNext and SwapAny grow at least exponentially in √m. However, the experiment results, which we will show in the next section, suggest that SwapNext and SwapAny potentially have a small upper bound. We conjecture tighter upper bounds of maximum residue.

SwapNext and SwapAny are two useful alternatives for scenarios that DoubleLex cannot handle well. DoubleLex works well when the smaller dimension m is particularly small as maximum residue (m!) will be small. When m is relatively larger, maximum residue (m!) grows significantly and stronger symmetry breaking is worthwhile. We will show in experiments on different benchmarks. When m becomes larger, SwapNext and SwapAny start to outperform DoubleLex and result in shorter runtime and less solutions. The winner between SwapNext and SwapAny depends on the larger dimension n. When n is moderately large, SwapAny generally performs better. When n is larger than a particular value, the overhead of SwapAny cannot be compensated by the saving from symmetry breaking and SwapNext becomes the best option. The exact cutoff points for selecting these methods are problem-specific, but the behaviours are general.

We suggest the following principles on selecting Lex-based symmetry breaking methods.

• DoubleLex: m is relatively small.
• SwapAny: m is relatively larger and n is moderately large.
• SwapNext: m is relatively larger and n is particularly large.

5 Experiment Results

In this section, we compare the pruning powers and running time efficiencies of DoubleLex, SwapNext, SwapAny and DoubleLex+AllPerm [Frisch et al., 2003]. In general, search and solution count reductions are not necessarily strongly connected, since it is always possible to produce a symmetry breaking method which breaks all symmetries but only causes the solver to fail only on leaf nodes. In practice, however, we use global constraints to break symmetries which do not fail only at leaf nodes. Such global constraints also often have good propagation power, but with an overhead. Our experiments aim at demonstrating how well each method strikes balance between search reduction and overhead.

We compare these methods on problems with matrix models and search for all solutions and first solution in satisfaction problems and an optimization problem. The time limit is one hour unless otherwise specified. In the experiments, we use row-wise canonical ordering in ≤lex constraints. Minimum domain size variable heuristic and minimum value heuristic are used unless otherwise specified. The best results are highlighted in bold. In the tables, we report the number of solutions found within timeout (sol) , runtime in seconds (time(s)), and the number of failures encountered (failure) to demonstrate the improved symmetry breaking power of the different methods. We represent large numbers in millions (M). For instances that cannot be solved within time limit, runtime would be noted by "-" and the number of solutions found and failures will be marked with "≥". All experiments are conducted using Gecode 5.0.0 on Intel(R) Xeon(R) CPU E5-2630 v2 2.60GHz processor with 250G memory.

5.1 Finding All Solutions

Unconstrained matrix. We compare the "pure" symmetry breaking effects of three methods on unconstrained m×n matrices with domain size d and results are reported in Table 2. On average, the solution set size of DoubleLex is 1.66 times larger than that of SwapNext, which runs 1.65 times faster than DoubleLex. The solution set size of DoubleLex is 2.57 times larger than that of SwapAny, which runs 2.21 times faster than DoubleLex. These demonstrate the stronger symmetry breaking power of SwapNext and SwapAny in terms of reduced exploration of symmetric solutions.

Error correcting code - Lee Distance (ECCLD). The problem [Frisch et al., 2003] aims at finding a codebook consisting of m codewords, where each codeword is a ncharacter string from the alphabet {1, 2, 3, 4} such that the Lee-Distance between each two codewords is d. The problem can be naturally modelled using an m × n matrix where each row [xi,1, . . . , xi,n] constitutes a codeword. As we could not find available implementation of AllPerm, we simulate AllPerm as in [Lee and Li, 2012] using the global cardinality constraints. Results are shown in Table 3. Experiment shows SwapAny outperforms all other methods. All other three methods have at least left one instance unsolved within time limit. On average, the solution set size of DoubleLex is 2.15 times larger than that of SwapNext, which runs 1.56 times faster than DoubleLex. DoubleLex+AllPerm and SwapNext achieve similar performances both in terms of solution set size and runtime. SwapAny achieves the best performance on almost all instances, which is on average 2.3 times faster than DoubleLex and results in 3.8 times smaller solution set. This agree with our suggestion that SwapAny is the best option when m is relatively larger and n is moderately large.

Balanced incomplete block designs (BIBD). The problem is well-known from design theory that requires a configuration distributing v objects into b blocks. Each object appears in r out of b blocks and there are k objects in each block. In addition, any two objects meet each other in the same block for exactly λ times. The problem can be modelled using a v × b 0/1 matrix where xi,j = 1 indicates that Object i is allocated to Block j. As the occurrences of 0 and 1 on each row are the same, DoubleLex+AllPerm degenerates to DoubleLex so we compare among the other three methods. The results in Table 4 agree with our prediction on the method with best performance: When the number of row v is small (5), DoubleLex performs well and stronger symmetry breaking is not in need. When v grows, SwapNext outperforms DoubleLex. SwapNext also outperfoms SwapAny on instances with large number of columns (b) since SwapNext explores similar numbers of solutions as SwapAny with much less overhead. SwapAny wins over SwapNext on only one instance where b is not too large.

5.2 Optimization

ECCLD (optimization version). We also test the efficiency on an optimization version of ECCLD. The goal is to minimize the average absolute equal occurrence discrepancy over the columns, which is a metric for selecting a good Cover Array [Kim et al., 2017]. The results are shown in Table 5. As SwapNext and DoubleLex+AllPerm achieve similar performance, we skip DoubleLex+AllPerm and compare among the three other methods. SwapAny still outperforms the other two methods. In particular, SwapAny is 2.42 times faster than DoubleLex on average.

5.3 Finding First Solution

We test also if the symmetry breaking methods help in finding first solution. Since symmetry breaking is not worthwhile when there is little search, we experiment on larger ECCLD and BIBD instances. In Tables 6 & 7, we report the runtime and the number of failures of each method. The "NoSB" column reports the result where no symmetry breaking is used.

ECCLD (first solution). We experiment with the rowwise variable heuristic and minimum value heuristic as it greatly outperforms the default heuristic we used in finding all solutions. While we have experimented with quite a number of instances, we report only results of those requiring more than 10s to solve with at least one method (including NoSB). The time limit is 2 hours. The results are reported in Table 6. NoSB is essentially impractical to use as compared to the other four methods. As predicted theoretically, SwapAny has the least failures among all methods. Instances (13 8 6), (13 9 6) and (13 10 6) are hard instances requiring much search, and SwapAny performs the best in terms of runtime with its strongest pruning power. The number of columns of all instances are not too large therefore enforcing strong symmetry breaking for search reduction is worthwhile. DoubleLex and DoubleLex+AllPerm are the worst in runtime among the symmetry breaking methods. The search heuristic always tries assigning 1 to all variables in the first row, making AllPerm constraints trivially satisfied. Thus, DoubleLex and DoubleLex+AllPerm achieve exactly the same performance both in runtime and failures.

BIBD (first solution). The rowwise variable heuristic and minimum value heuritic are equivalent to the default heuristic here since the domains are binary. The results are reported in Table 7. Here, we report results of only instances requiring more than 10s with at least one symmetry breaking method (excluding NoSB). NoSB can solve none of the instances.

DoubleLex wins in runtime in all instances except the last since relatively little search is required to find the first solution and DoubleLex is comparable in search reduction to SwapNext and SwapAny. SwapAny timeouts on instances (9 84 28 3 7) and (9 96 32 3 8) as a prohibitively large number of constraints are introduced by the large number of columns. DoubleLex still wins since SwapNext only achieves minor search reduction. The number of columns of the last instance is moderate and some search (< 10M failures) is needed to find the first solution. SwapNext prevails.

6 Conclusion

We give a factorial improvement to the best known upper bound of remaining solutions over all symmetry classes of Gmat. From there, we propose Maximum Residue (MR) as a notion to evaluate the strength of a symmetry breaking method. We further study the MR bounds of SwapNext and SwapAny, which are extensions to DoubleLex for stronger symmetry breaking. The theoretical comparisons allow us to suggest general principles on selecting Lex-based symmetry breaking methods based on the dimensions of the matrix models and they are confirmed by our experiments. We believe investigation on tighter bounds of SwapNext, SwapAny and other existing symmetry breaking methods are meaningful future works. Studying MRs of other methods potentially give insights and hints for deriving alternative choices of symmetry breaking constraints.