Excluding Symmetries in Constraint-Based Search.
We introduce a new method, called i>symmetry excluding search (SES), for excluding symmetries in constraint based search. To our knowledge, it is the first declarative method that can be applied to i>arbitrary symmetries. The SES-method is based on the notion of symmetric constraints, which are used in our modification of a general constraint based search algorithm. The method does not influence the search strategy. Furthermore, it can be used with either the full set of symmetries, or a subset of all symmetries.We proof correctness, completeness and symmetry exclusion properties of our method. Then, we show how to apply the SES-method in the special case of geometric symmetries (rotations and reflections) and permutation symmetries. Furthermore, we give results from practical applications.
Introduction
In many search problems, one is faced with the existence of symmetries. Symmetries
give rise to many dierent solutions found by the search procedure, which
are all considered to be "similar". Often, one is not interested in also getting all
the symmetric solutions to every found solution. Without exclusion of symme-
tries, whenever a solution is found or proven to be inconsistent with the search
problem, the search algorithm still considers all symmetric solutions. Those symmetries
will then give rise to an (often exponential) amplication of the search
space. Hence, symmetry exclusion promises to eciently prune the search tree.
E.g., consider constraint problems, where nite domain variables have a geometric
interpretation such as in the N-queens problem or the square-tiling problem
(where set of squares of given sizes must t exactly into a xed square).
A more complex, real-world problem is the lattice protein structure prediction
problem. In [2], it is shown how to nd solutions for this problem using constraint
programming techniques. In this case, dierent solutions are symmetric if they
can be generated using re
ections or rotations. In other problems, symmetric
solutions can be generated by performing permutations on variables valuations
(like in the map coloring (or graph coloring) problem).
In the following, we consider search problems that stems from constraint satisfaction
problems (CSP). A common approach is to transform (problem specif-
ically) a CSP C 1 into a CSP C 2 that excludes at least some of the symmetries
of the original problem C 1 .
Unfortunately, symmetry exclusion was often not straightforward to imple-
ment. Even then, it had to be redesigned for every special problem or enumeration
strategy. This leaded to an in
exibility in the program structure once it
was introduced. Thus, the widespread usage of symmetry exclusion was strongly
hindered by its complexity. Often symmetry exclusion was not done at all or
only for a small set of symmetries. In other cases, where symmetry exclusion
was implemented it distracted the programmers attention from more important
tasks.
In this paper, we will present a new approach for symmetry exclusion, which
works by modifying the search algorithm. The technique of modifying the search
algorithm to exclude symmetries was already used in the literature. In contrast
to the known approaches, our approach is (to our knowledge) the rst declarative
method that can be applied to arbitrary symmetries that can be dened declar-
atively. Furthermore, it does not restrict the search strategy (i.e., the symmetry
exclusion can be done independently of the search strategy). This is important
since in many constraint problems, major part of the knowledge of the problem
is encoded in the search strategy.
We have implemented our method in the concurrent constraint programming
language Oz [10] using the programmable search engine described in [9]. But
the method can be implemented in any system that handles implication (via
and allows to modify the search procedure such that additional
constraints are added in one branch of a branching step.
Related Work Previous work on symmetry exclusion by modifying the search
algorithm handled only restricted forms of symmetries. In [7], the notion of
interchangeable values is introduced. Two values a and b are interchangeable for
a variable V i for every solution that maps V to a, the corresponding valuation
that maps V to b is also a solution.
The method in [3] handles only permutations of domain values in the case
of binary constraints (thus, e.g., the all-distinct constraint has to be translated
into binary inequalities, which implies that ecient propagation methods for all-
distinct cannot be applied). Furthermore, it works by introducing a symmetry
excluding form of constraint propagation, which is a modied form of domain
propagation (thus, the method cannot make use of interval propagation).
[1] and [4] consider only propositional calculus. The symmetries there are
permutations of Boolean variables. These methods do not apply to general constraint
satisfaction problems.
The symmetry exclusion algorithm presented in [8] is essentially an implementation
and application of our method to solve practical problems, which will
be compared in greater detail in Section 3.
An example of a symmetry exclusion method that works by a (not problem
specic) transformation of the constraint satisfaction problem is [5]. They introduce
symmetry breaking predicates, which are true only for the smallest solution
within an equivalence class (where the ordering is xed in advance). Thus, if the
search strategy encounters a non-minimal (according to the pre-xed ordering)
solution rst, then it will be excluded by the symmetry breaking predicates. This
implies that not every search strategy is possible given the pre-xed ordering.
In contrast, there is no prexed ordering in which symmetrical solutions will
be excluded by our method. This implies that we respect used-dened search
strategies as much as possible. 1
Overview of the paper We start with an introductory example explaining the
basic ideas of our method. After some preliminaries, we present the formal de-
nition as wells as completeness and correctness proofs in Section 3. Additionally,
we show that our method guarantees to exclude all specied symmetries. The
proofs indicate that a subset of all symmetries can be enough to exclude the
complete symmetry group. In Section 4, we treat geometric symmetries. We
show how to dene symmetric constraints and present the results of applying
the problem to a complex problem. In Section 5, we consider symmetries which
are generated by permuting the values of the variables. E.g., such symmetries
occur in the graph coloring problem. We proof, that in this case, it is sucient
to exclude the subset of transposition in order to exclude all permutations. Fur-
thermore, we present the results of applying the method to random instances of
graph coloring.
Introductory Example We start with a simple example to explain the main
concepts. Consider the N-queens problem, where we have an array Q[1::N ],
whose elements can take values from 1::N . states that there is a queen
at position (i; j). Now consider the symmetry corresponding to the re
ection at
the axis
2 , which is parallel to the x-axis (in the sequel denoted by Rx).
Clearly, for every solution of the N-queens, the the Rx-symmetric version is also
a solution of N-queens. Hence, we want to exclude these symmetric solutions.
To use our method, we have rst to introduce symmetric versions of the
constraints which are inserted by the search procedure. One kind of constraint
is j. If we have any distribution of queens on the board satisfying
j, then the Rx-symmetric distribution will satisfy j. Hence, the
constraint is the Rx-symmetric version of the constraint
Similarly, we get that the Rx-symmetric constraint of Q[i]  j is Q[i]  N j.
In the following, we write S Rx (c) to denote the Rx-symmetric constraint to c.
Our method works by adding additional constraints at the right branches of
the search tree, which exclude the symmetric solutions that are encountered in
the right branch. Consider the following search tree for the 10-queens problem,
where we indicate the constraints added by symmetry exclusion via frames:
Clearly, if the search strategy depends on the constraint store, then any method of
symmetry exclusion that prunes the search tree must in
uence the way solutions are
encountered (since the constraint store is changed by the symmetry exclusion).
This can be interpreted intuitively as follows. In the topmost branch, if we search
for a solution in the right branch satisfying Q[1] > 5, then the Rx-symmetric
solution will satisfy Q[1] < 5. Hence, the symmetric solution was already encountered
earlier in the left branch (under Q[1]  5), which is the reason that
we can close the topmost right branch. For the second right branch labeled
Q[2] 6= 3, we want again to exclude the Rx-symmetric solutions found in the
right branch. Hence, we would like to add the constraint :S Rx to the
right branch. But this would exclude too many solutions. The prerequisite of the
Rx-symmetric solution to be found in the right branch is that both the solution
and its Rx-symmetric version satises Q[1]  5. Now the only solutions that
satisfying this conditions are solutions that satisfy 5. Hence, we can add
under the condition that 5. But this is exactly the eect
that we achieve by adding at the second right
branch (since the constraint store contains already Q[1]  5).
Preliminaries
We x a rst-order signature  including the equality :
with a set of variables
. Constraints are literals, and constraint formulae are quantier-free formulae
over . We identify
t. C denotes the set of all constraints. A
set of constraints C  C is interpreted as the conjunction of the constraints
contained in C, and we will freely mix set notation and conjunction. The set of
free variables of C is denoted by V(C).
We x a standard interpretation A with domain D A , which describes our
constraint theory. In the following, we assume a xed constraint set C Pr describing
the problem to be solved. An assignment  in A is a partial function
We say that an (possible partial) assignment  satises  (short
there is a total assignment  0   with A;  0 j= . We write
for every  we have  . A constraint set C (syntactically) determines
a set of variables X to an assignment  i for all x 2 X exists a t such that
x
In many problems, one is interested in only a subset of all variables, whose
valuations uniquely determine the valuation of the other (auxiliary) variables.
This is captured by the denition of solution variables.
Denition 1 (Solution Variables). Let X  V be a set of variables. X is a
solution variables set for C if
where 9!() ('exists a unique  satisfying ()') is short for
solution variables set X , we say that  is a X -solution
for C if we denote the set of X -solutions
of C.
In the following, we x X . Hence, we use the term 'solution' as short for
'X -solution for C', and we write kCk as short for kCk X .
Denition 2 (Symmetry). A symmetry s for C Pr is a bijective function
A symmetry set S for C Pr is a set of symmetries operating on kC Pr k. A symmetry
group S is a symmetry set for C Pr which is a group.
Note that for every symmetry s for C Pr , also s 1 is a symmetry for C Pr . We
denote the identity function on kC Pr k with id CPr (which is a symmetry by def-
inition). Clearly, the set of all symmetries for C Pr is a group. But many cases,
we do not want to consider all symmetries, since either there are too many of
them, or some of them do not have an intuitive characterization. In this case,
we consider only a subset of all symmetries, which may not be a group.
3 Symmetry Excluding Search Trees
Now we have to dene the notion of a search tree as we need it for the symmetry
exclusion. We describe the eects of applying a constraint solver to a constraint
set C by a function P (C), which returns the closure of C under constraint
propagation. Clearly, we have P (C) j=j C.
Usually, a search tree is a labeled tree, where the nodes are labeled with the
constraints in the constraint store, and the edges are labled by constraints or
negated constraints. A single node v is of the form
c
C store
The root node is labeled with P (C Pr ). Additionally, we need for the symmetry
exclusion to store at a node v the positive and negative constraints that have
been used along the path from the root to v to generate the node v.
Denition 3 (Search Tree). Let t be a nite, binary, rooted and ordered tree,
whose egdes are labeled by literals, and whose nodes are labeled by triples of
constraint sets. The tree t is a search tree for C Pr if the following conditions are
1. The root node has the label (;; ;; P (C Pr )),
2. every binary node has the form
store
c :c
store
with C l
store
store
Intuitively, the reason for distinguishing between positive and negative constraints
is just that Cn describes the previously found solutions, i.e.
Here, we denote with  t the partial ordering of nodes induced by t.
Note that we do not force C l
store (resp. C r
store ) to be equivalent to C store ^
c (resp. C store ^ :c). The reason is that we do have to add some additional
constraints during search for excluding symmetries. Since C store describes all
constraints valid at some node v, we set for a node v in t with
label
We now state general properties of search tree in the presence of symmetries.
Denition 4 (Expanded, C Pr -Complete and S-Reduced Trees).
The search tree t is completely expanded if every unary node
either determines X to . A search tree t
is C Pr -complete if for every  2 kC Pr k there is a leaf v in t with
S be a symmetry set for C Pr . A search tree is C Pr -complete w.r.t. S if for every
there is a leaf v for such that
A search tree is S-reduced if for every leaf v with
Note that (1) is equivalent to 8s 2 S 8v 0
S is closed under inversion.
Before we can show how to produce a S-reduced search tree that is C Pr -
complete w.r.t S, we rst have to dene how symmetries operate on constraints.
In the following, we will assume that for every constraint c and every s, there
is a constraint c 0 such that s  s  on sets of C Pr -
solutions by s Ag. For every c, there are usually dierent
constraints c 0 with s  k. Hence, x a function s con on constraints such
that
ks con (c)k:
In the next sections, we give examples of how to construct this function.
Proposition 1. Let s con be dened as before. Then s con distributes over the
Boolean operators, i.e., s  (kc^c 0 ks con (c)^s con ks con (c)_
ks con (:c)k.
Hence, we identify s con with its homomorphic extension to constraint sets
and arbitrary formulae. Now we can state a general mechanism for generating a
search tree that is S-reduced.
Denition 5 (S-excluding). Let S be a symmetry set. A search tree for C Pr
is S-excluding if every binary node v has the form
store
c :c
store
with C l
Before we prove S-reducedness and C Pr -completeness w.r.t S of S-excluding
search trees, we state a proposition to precise the eect of adding the implications
in denition 5 to C r
store . For convenience, we write C v
store to access
store in the label (C store ) of v. For a binary node v we refer
to its left child as v l and to its right child as v r .
Proposition 2. Let S be a symmetry set and t a S-excluding search tree. For
every symmetry s 2 S and for every node v of t we have C v
store
s con (C v
For notational convenience we introduce the notation C path
C Pr . A good intuition is to think of C path (v) describing the constraint store of
v in a simple not symmetry excluding search tree.
Reducedness and completeness will be essentially corollaries to the following
proposition.
Lemma 1. Let S be a symmetry set. Every S-excluding search tree t for C Pr
satises for every node v
where A v
Proof. We proof this by tree induction. For the root this is valid, since A v
and (v)k. Assume that we have proven the claim for a
binary node v:
store
c :c
store
For the left child v l the claim follows immediately from the induction hy-
potheses, since A v l
S .
For v r , we have to show kv r
S . Note that A vr
subdivides into its two subsets A v
S and
)k)g. Further according to
our denitions C path (v r ) is equivalent to C path (v) ^ :c.
To show that kv r k  kC path (v) ^ :ck A vr
then we
have to show for every v 0  t v that
The rst case is v 0  t v. Let  2 kC path (v 0 )k. Then s() 62 kvk by induction
hypotheses. Since kv r k  kvk, this immediately implies s() 62 kv r k.
The second case is (v 0 6 t v) and v 0  t v r , i.e., v 0 is a subnode of v l . Let
k. From  2 kv l k we have
s con (C p ^c). That's a contradiction, because from denition of S-excluding search
tree s()
It remains to be shown that kv r k  kC path (v r )k A vr
S Let  62 kv r k. We have
to show
62 kC path (v r )k A vr
We have the following cases:
1.  62 kC path (v r )k. Then (3) follows immediately.
2.  2 kC path (v r )k and  62 kvk. We have to show  2 A vr
S .
Now  2 kC path (v r )k implies  2 kC path (v)k and henceforth  2 A v
by induction hypotheses.
3.  2 kC path (v r )k and  2 kvk. We will show that
Since
store , there is at least one s 2 S with  6j=
(c) by the denition of an S-excluding tree. Fix one of these
symmetries s. Then
by Proposition 2, we get
Hence, s 1 (), which exists by denition of symmetries, satises s 1 ()
that C path
with we have a valuation such that  2 kC path (v l )k and
which shows that  is in the set dened by (4).
Theorem 1. Let S be a symmetry set. Every S-excluding search tree t for C Pr
is S-reduced.
Proof. Fix a symmetry s 2 S, let v be a leaf of t with fg. We have to
show for every node v 0 of t with v 0  t v that kv 0
v 0 to be a node of t with v 0  t v and kv It follows
and from this the contradiction
62 kvk by Lemma 1.
By now we understand that an S-excluding search tree may exclude more
symmetries than actually declared by S directly. Hence, we have to investigate
the completeness property of S-excluding search trees.
Theorem 2. Let S be a symmetry set. Every S-excluding search tree t for C Pr
is C Pr -complete w.r.t S 0 , where S 0 is the closure of S under composition and
inversion.
Proof. We have to show that t is C Pr -complete w.r.t. to S 0 , where S 0 is the
closure under composition of S, i.e. for every  2 kC Pr k there is a leaf v with
Hence x an  2 kC Pr k. Then there exists a leaf v 0 in t with  2 kC path (v 0 )k
from denition 5. There are two cases.
1.  2 kv 0 k. This yields immediately kv and (5) is proven.
2.  62 kv 0 k. By Lemma 1 follows  2 A v 0
there is a s 1 2 S and a
path (v 00 )k: By induction we get
a sequence of symmetries s
for a leaf v (n+1) of t. Since S 0 is the closure of S, claim (5) follows.
We will given an example for symmetry excluding search trees in Secion 5,
where the symmetrie group of permutation are excluded by the subset of all
transpositions (as indicated by the above theorem).
Now we are able to give a more detailed comparison with [8]. The SBDS-
method therein is essential our symmetry exclusion restricted to the case where
the search tree branches over constraints of the form V ar al. In this case, the
constraint collected in C p is of the form V ar
C p is a partial assignment A. For the restricted SBDS-method, consider the case
that a symmetry S  is dened by a permutation  rst. Then S
al n at some node v of
the search tree, which branches over V ar al. Then the constraint added by
our method for excluding the symmetry S  is S  (V ar
which is by the denition of S  the same as
ar
Now the antecedence is nothing else than a test whether S  leaves C p (i.e.,
the partial assignment at the node v) unchanged. Thus, the entailment will be
evaluated and removed directly at the right subnode of v. The restricted SBDS-
method essentially replaces the entailment test by the test whether the symmetry
leaves the assignment unchanged. Only those symmetries are excluded, where
the test can be decided at the node the corresponding implication would be
integrated by our method (even if the corresponding implication would delay
this test to a later point).
Note on implementation For the symmetry exclusion we have to add implications
of the form s con (C v
during the search procedure. Hence, one has
to change the search procedure for implementing the symmetry exclusion. The
antecedents of these implications can be computed during the search eciently,
using the observation that the antecedences of the added implications of ancestor
nodes are prexes of the ones added in their ospring. To be more precise, let
v be a node, which branches over the constraint c, and let v l (resp. v r ) its left
(resp. right) daughter. Now
s con (C v l
For
Therefore the computation of the condition
s con (C p ) can be done incrementally. We maintain Boolean variables for this reason
in our implementation. We need one variable for each symmetry s, containing
the values for s con (C p ).
4 Geometric Symmetries
We will give now a concrete example for symmetries, namely geometry symme-
tries. We will treat the special case where we have points in Z d , although our
method is not restricted to this case. We will exemplify the symmetry constructions
in two dimensions, and give an example for the exclusion of additional
symmetries as indicated by Theorem 2.
Denition of Geometric Symmetries There are many problems where one encodes
the two-dimensional position of an object i using nite domain integer
variables . Examples are the N-queens and the tiling problem. A more
complex and realistic example (in three dimensions) is the lattice protein structure
prediction problem [2].
The symmetries for Z 2 have exactly the same structure as for the general
case Z d . They are dened by ane mappings
that map Z d onto Z d . I.e., the matrix AS is an orthogonal matrix
with the property that the set of columns fv of AS equals fe j
e is a unit-vector of Z d g: E.g., for Z 2 , the matrix 0 1
denotes the rotation
by 90  . For Z 2 , we have 8 symmetries consisting of the identity, the 4 re
ections
(at x- and y-axis, and the two diagonals) and the 3 rotations by 90  , 180  and
270  . For Z 3 , we have 48 symmetries including the identity.
By now, the vector v S is not yet xed. There are two dierent approaches
for xing the symmetry. We will consider Z 2 as an example. The methods work
for all other dimensions as well.
The rst case is that every possible solution lies within a xed square (in the
general case, within a hypercube). 2 This is equivalent to the proposition that
there are integers xmin such that for all  2 kC Pr k we have
2 The technique can be extended to the case that the hypercube is not xed in advance.
Thus, the minimal square around the position of all objects is dened by the
points in every solution. We call this the frame
of the problem C Pr . In the N-queens problem, this is just the board.
Now knowing the frame of a problem C Pr , we can x the vector v S for all
symmetries. Consider as an example a problem whose frame is dened by (0;
and (3; 2). Furthermore, consider the three symmetries re
ection at the y-axis,
rotation by 90  and rotation by 180  , which we will name S 1 , S 2 and S 3 in the
following. The corresponding mappings are dened by S i
where the matrices AS1 ; AS2 and AS3 are dened by
The corresponding mappings of the frame are
A symmetry S is compatible with the above dened frame if the frame is mapped
to itself, i.e., if fv j (0; 2)g. For a
given matrix AS , there exists a v S such that
condition if and only if AS satises
AS (3;
For the matrices AS1 , AS2 and AS3 , we get ( 3; 2), ( 2; 3) and ( 3; 2), which
excludes the symmetry characterized by AS2 . We nally get
The second case is that we know a point should remain
unchanged under the symmetries. In that case, we know that the symmetries
are dened by S i
(p).
The remaining part is to dene symmetric constraints. We use a specic example
where we leave the point (5; 5) x. Consider the two symmetries re
ection
at the y-axis and rotation by 90  . By what we have said above, the corresponding
mappings are
Now suppose that we have modeled points using variables
and we want to dene S Ry
con and S 90
con for the constraints of the
other kind of constraints c, the denition S con (c) is analo-
gous). Now the symmetric constraints S Ry
con
con must
express the constraint valid for S Ry () (resp. S 90
for every possible  with
does not restrict the valuation of (Y i ), we know that S Ry
con
is
con Analagously, we get that S Ry
con
is and that S 90
con Note that S Ry (c) has the same
type as c (i.e., both have the same variable). This does not hold for c and S 90
(c).
We will now turn to an example where we exclude only one symmetry, but
the exclusion method excludes compositions of this symmetry. This shows that
there are cases where the symmetry exclusion method excludes more than the
symmetries contained in the symmetry set S (as indicated by Theorem 2). We
will use an articial example to show the existence of such a case.
Example 1. Let C Pr be a geometric constraint problem over the variables X;Y ,
where X and Y have the domain [0::10] associated. Furthermore, suppose that
C Pr has (6; 6) as a solution that we can apply the rotational symmetries with x
point (5; 5). This implies, that (4; 4), (4; are also solutions of C Pr .
Now consider the following S-excluding search tree for
(where
the constraints added by the symmetry exclusion are in a framed box):
Then the solution (4; (which is (6; rotated by 90  ) is excluded by the symmetry
exclusion in t 1 . But furthermore, the solution (4; is excluded in t 2 by
our symmetry exclusion method. This is (6; rotated by 180  . Hence, although
contains only S 90
, the symmetry S 180
(which is just S 90
excluded by our method. Note that (6; 4) (which is (6; rotated by 270  ) is not
excluded and may be found in t 2 .
Clearly, in the case of geometric symmetries, the full symmetry group is
usually small enough that we can include all symmetries. But we wanted to
show the eects of excluding only a subset of the full symmetry group using
the above simple example. In the next section on permutation, we will give an
example where the exclusion of transpositions allows to exclude all permutations.
Results We have applied the method to the lattice protein structure prediction
[2], which is a hard combinatorical problem. The following table shows the
number of solutions, search steps and runtimes for nding all minimal energy
structures for 4 sequences, in the rst case without symmetry exclusions, and
with symmetry exclusion in the second part:
without sym. excl. with sym. excl. ratio
seq. length #noex nnoex tnoex #ex nex tex #noex
#ex
nnoex
nex
ex
We have added simple exclusion methods in both cases, which is the reason that
we have only 16 (instead of 48) symmetries left in S1; S2 and S 6 . As one can see
from the table, we have a nearly linear speedup in number of search steps, and
a close to linear speedup in runtime. In S3, the simple exclusion does not apply,
which gives rise to 48 symmetries. Furthermore, the optimal conformations and
the symmetric ones are very similar, which implies that we have less speedup
(since detecting the symmetric solution is harder).
Permutation symmetries
In the following, we consider nite domain integer problems, where the variables
have the domain D  N associated. In the following, we denote with Perm(D)
the set of all permutations of D, and with Trans(D) the set of all transpositions
of D (i.e., those permutations, which exchange just two elements of D). With
Perm(D) , we denote the set of all symmetries that permute the values of the
variables in X .
Denition 6. Let X be the set of solution variables. The set of all value permutations
of X is dened as the symmetry set
The subset of all transposition symmetries S X
is dened analogously.
Now we consider search trees that branch over constraints having one single
constraints of the forms
The interesting part is that if a search tree branches over constraints that have
one single
Trans(D) -excluding tree is even S X
reduced. Thus, we need to exclude only the quadratically many transpositions
to exclude the exponentially many permutations in this case.
Theorem 3. Let C Pr be a problem which has S X
Perm(D) as a symmetry group. Let
t be a S X
Trans(D) -excluding search tree such that for every branch v, the constraint
c used at this branch has one free variable out of X . Then t is S X
Perm(D)
-reduced.
Proof (sketch). Consider a permutation  and the corresponding symmetry S  .
Now consider any node
l
c(x)
we know that ((x)) must be dierent
from (x). Now let  be the transposition such that
let S  be the corresponding symmetry. Then the exclusion of all transposition
would exclude the solution  if we can show that in the node considered above,
we have that S  1  S  () 2 kv l k. But this can be shown under the assumption
that the search tree uses only constraints that have one
Graph Coloring As noted above the graph coloring is an example for a problem
with value permutations as symmetries. The graph coloring problem is as follows.
Given a graph E) and a set of colors. An admissible coloring c of G, is
a mapping of the vertices V to the set of colors, satisfying the constraint that
for all (v What is the minimal set of colors, where we
still can nd an admissible coloring.
In this problem colorings are considered to be symmetric, if they are just
permuted in colors to each other.
We compare two implementations of a solver for this problem. The rst one
is a naive implementation that uses a simple rst fail heuristic. This implementation
does not have symmetry exclusion. The second implementation with full
exclusion of symmetries is just a simple extension of the rst one, where we
added our symmetry exclusion mechanism. Note that, due to the above theo-
rem, it suces to handle only the set of transpositions instead of handling the
group of all permutations to get the full symmetry exclusion.
We give the results for some randomly generated problem instances of dier-
ent problem sizes.
problem size with symmetry excl. without symmetry excl. ratio
verts edges colors cloned failed time cloned failed time cloned time
6 Conclusion and Future Work
We have introduced the rst method that can exclude arbitrary symmetries in
constraint-based search. In contrast to many other methods that can be found
in the literature, the method does not restrict the search strategy.
The method is based on a declarative description of the symmetries in the
form of symmetric constraints, which usually can be obtained easily. We have
given completeness and correctness proofs as well as the proof, that the method
exclude all considered symmetries. In the case that the full symmetry group is
too large, our method can handle arbitrary subsets of the full symmetry group.
We have shown for the case of permutation symmetries that it is sucient to exclude
the (quadratically many) transposition to exclude all (exponentially many)
permutations.
The method can be implemented in any (constraint-based) search machinery
that handles implications and allows to introduce additional, user-dened
constraints during search. This holds for the most modern constraint programming
systems. Since the method is very general, we plan to investigate in which
other (logic-based) search methods our symmetry exclusion can be used. Fur-
thermore, we intend to investigate more general conditions under which a subset
of the full symmetry group allows to exclude all symmetries (as it is the case for
the permutations).



--R

Alfonso San Miguel Aguirre.
Constraint techniques for solving the protein structure prediction problem.
Study of symmetry in constraint satisfaction problems.
Tractability through symmetries in propositional calculus.
Symmetry breaking predicates for search problems.
Thierry Boy de la Tour.
Eliminating interchangeable values in constraint satisfaction prob- lems
Symmetry breaking during search in constraint programming.

The Oz programming model.
--TR

--CTR
Y. C. Law , J. H. Lee, Symmetry Breaking Constraints for Value Symmetries in Constraint Satisfaction, Constraints, v.11 n.2-3, p.221-267, July      2006
Rolf Backofen , Sebastian Will, A Constraint-Based Approach to Fast and Exact Structure Prediction in Three-Dimensional Protein Models, Constraints, v.11 n.1, p.5-30, January   2006
geometric symmetries;permutation symmetries;symmetry excluding search SES;symmetry exclusion;constraint-based search