AN ADAPTIVE PREFIX-ASSIGNMENT TECHNIQUE
FOR SYMMETRY REDUCTION

arXiv:1706.08325v1 [cs.LO] 26 Jun 2017

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

Abstract. This paper presents a technique for symmetry reduction that
adaptively assigns a prefix of variables in a system of constraints so that the
generated prefix-assignments are pairwise nonisomorphic under the action of
the symmetry group of the system. The technique is based on McKay’s canonical extension framework [J. Algorithms 26 (1998), no. 2, 306–324]. Among
key features of the technique are (i) adaptability—the prefix sequence can be
user-prescribed and truncated for compatibility with the group of symmetries;
(ii) parallelisability—prefix-assignments can be processed in parallel independently of each other; (iii) versatility—the method is applicable whenever the
group of symmetries can be concisely represented as the automorphism group
of a vertex-colored graph; and (iv) implementability—the method can be implemented relying on a canonical labeling map for vertex-colored graphs as the
only nontrivial subroutine. To demonstrate the tentative practical applicability of our technique we have prepared a preliminary implementation and report
on a limited set of experiments that demonstrate ability to reduce symmetry
on hard instances.

1. Introduction
1.1. Symmetry reduction. Systems of constraints often have substantial symmetry. For example, consider the following system of Boolean clauses:
(1)

(x1 ∨ x2 ) ∧ (x1 ∨ x̄3 ∨ x̄5 ) ∧ (x2 ∨ x̄4 ∨ x̄6 ) .

The associative and commutative symmetries of disjunction and conjunction induce
symmetries between the variables of (1), a fact that can be captured by stating that
the group Γ generated by the two permutations (x1 x2 )(x3 x4 )(x5 x6 ) and (x4 x6 )
consists of all permutations of the variables that map (1) to itself. That is, Γ is the
automorphism group of the system (1), cf. Sect. 2.
Known symmetry in a constraint system is a great asset from the perspective of
solving the system, in particular since symmetry enables one to disregard partial
solutions that are isomorphic to each other under the action of Γ on the space of
partial solutions. Techniques for such isomorph rejection1 [42] (alternatively, symmetry reduction or symmetry breaking) are essentially mandatory if one desires an
exhaustive traversal of the (pairwise nonisomorphic) solutions of a highly symmetric system of constraints, or if the system is otherwise difficult to solve, for example,
with many “dead-end” partial solutions compared with the actual number of solutions.
A prerequisite to symmetry reduction is that the symmetries are known. In
many cases it is possible to automatically discover and compute these symmetries to
1A term introduced by J. D. Swift [42]; cf. Hall and Knuth [20] for a survey on early work on
exhaustive computer search and combinatorial analysis.
1

2

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

enable practical and automatic symmetry reduction. In this context the dominant
computational approach for combinatorial systems of constraints is to represent Γ
via the automorphism group of a vertex-colored graph that captures the symmetries
in the system. Carefully engineered tools for working with symmetries of vertexcolored graphs [15, 27, 35, 37] and permutation group algorithms [10, 40] then
enable one to perform symmetry reduction. For example, for purposes of symmetry
computations we may represent (1) as the following vertex-colored graph:
x1 ∨ x2

(2)

x1 ∨ x̄3 ∨ x̄5

x2 ∨ x̄4 ∨ x̄6

x1

x2

x3

x4

x5

x6

x̄1

x̄2

x̄3

x̄4

x̄5

x̄6

In particular, the graph representation (2) enables us to discover and reduce symmetry to avoid redundant work when solving the underlying system (1).
1.2. Our contribution. The objective of this paper is to document a novel technique for symmetry reduction on systems of constraints. The technique is based on
adaptively assigning values to a prefix of the variables so that the obtained prefixassignments are pairwise nonisomorphic under the action of Γ. The technique can
be seen as an instantiation of McKay’s [36] influential canonical extension framework for isomorph-free exhaustive generation.
To give a brief outline of the technique, suppose we are working with a system
of constraints over a finite set U of variables that take values in a finite set R.
Suppose furthermore that Γ ≤ Sym(U ) is the automorphism group of the system.
Select k distinct variables u1 , u2 , . . . , uk in U . These k variables form the prefix
sequence considered by the method. The technique works by assigning values in
R to the variables of the prefix, in prefix-sequence order, with u1 assigned first,
then u2 , then u3 , and so forth, so that at each step the partial assignments so
obtained are pairwise nonisomorphic under the action of Γ. For example, in (1)
the partial assignments x1 7→ 0, x2 7→ 1 and x1 7→ 1, x2 7→ 0 are isomorphic since
(x1 x2 )(x3 x4 )(x5 x6 ) ∈ Γ maps one assignment onto the other; in total there
are three nonisomorphic assignments to the prefix x1 , x2 in (1), namely (i) x1 7→
0, x2 7→ 0, (ii) x1 7→ 0, x2 7→ 1, and (iii) x1 7→ 1, x2 7→ 1. Each partial assignment
that represents an isomorphism class can then be used to reduce redundant work
when solving the underlying system by standard techniques—in the nonincremental
case, the system is augmented with a symmetry-breaking predicate requiring that
one of the nonisomorphic partial assignments holds, while in the incremental setting
[22, 43] the partial assignments can be solved independently or even in parallel.
Our contribution in this paper lies in how the isomorph rejection is implemented
at the level of isomorphism classes of partial assignments by careful reduction to
McKay’s [36] isomorph-free exhaustive generation framework. The key technical
contribution is that we observe how to generate the partial assignments in a normalized form that enables both adaptability (that is, the prefix u1 , u2 , . . . , uk can
be arbitrarily selected to match the structure of Γ) and precomputation of the
extending variable-value orbits along a prefix.
Among further key features of the technique are:

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

3

(1) Implementability. The technique can be implemented by relying on a canonical labeling map for vertex-colored graphs (cf. [27, 35, 37]) as the only
nontrivial subroutine that is invoked once for each partial assignment considered.
(2) Versatility. The method is applicable whenever the group of symmetries
can be concisely represented as a vertex-colored graph; cf. (1) and (2). This
is useful in particular when the underlying system has symmetries that are
not easily discoverable from the final constraint encoding, for example, due
to the fact that the constraints have been compiled or optimized2 from a
higher-level representation in a symmetry-obfuscating manner. A graphical
representation can represent such symmetry directly and independently of
the compiled/optimized form of the system.
(3) Parallelisability. As a corollary of implementing McKay’s [36] framework,
the technique does not need to store representatives of isomorphism classes
in memory to perform isomorph rejection, which enables easy parallelisation
since the partial assignments can be processed independently of each other.
The main technical contribution of this paper is developed in Sect. 4 where we
present the prefix-assignment technique. The required mathematical preliminaries
on symmetry and McKay’s framework are reviewed in Sects. 2 and 3, respectively.
Our development in Sect. 4 relies on an abstract group Γ, with the understanding
that a concrete implementation can be designed e.g. in terms of a vertex-colored
graph representation, as will be explored in Sect. 5.
1.3. Preliminary implementation and experiments. To demonstrate the tentative practical applicability of our technique we have prepared a preliminary experimental implementation.3 The implementation is structured as a preprocessor that
works with an explicitly given graph representation and utilizes the nauty [35, 37]
canonical labeling software for vertex-colored graphs as a subroutine to prepare an
exhaustive collection of nonisomorphic prefix assignments relative to a user-supplied
or heuristically selected prefix of variables. In Sect. 6 we report on a limited set
of experiments with solving systems of Boolean polynomial equations that demonstrate the ability to reduce symmetry on hard instances and give an initial favorable
comparison with earlier techniques.
1.4. Earlier work. A classical way to exploit symmetry in a system of constraints
is to augment the system with so-called symmetry-breaking predicates (SBP) that
eliminate either some or all symmetric solutions [5, 14, 19, 39]. Such constraints
are typically lexicographic leader (lex-leader) constraints that are derived from a
generating set for the group of symmetries Γ. Among recent work in this area,
Devriendt et al. [16] extend the approach by presenting a more compact way for expressing SBPs and a method for detecting “row interchangeabilities”. Itzhakov and
Codish [26] present a method for finding a set of symmetries whose corresponding
lex-leader constraints are enough to completely break symmetries in search problems on small (10-vertex) graphs; this approach is extended by Codish et al. [12]
2For a beautiful illustration, we refer to Knuth’s [31, §7.1.2, Fig. 10] example of optimum
Boolean chains for 5-variable symmetric Boolean functions—from each optimum chain it is far
from obvious that the chain represents a symmetric Boolean function. (See also Example 2.)
3This implementation can be found at https://github.com/pkaski/reduce/ .

4

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

by adding pruning predicates that simulate the first iterations of the equitable partition refinement algorithm of nauty [35, 37]. Heule [23] shows that small complete
symmetry-breaking predicates can be computed by considering arbitrary Boolean
formulas instead of lex-leader formulas.
Our present technique can be seen as a method for producing symmetry-breaking
predicates by augmenting the system of constraints with the disjunction of the nonisomorphic partial assignments. The main difference to the related work above is
that our technique does not produce the symmetry-breaking predicate from a set
of generators for Γ but rather the predicate is produced recursively, and with the
possibility for parallelization, by classifying orbit representatives up to isomorphism
using McKay’s [36] framework. As such our technique breaks all symmetry with
respect to the prescribed prefix, but comes at the cost of additional invocations
of graph-automorphism and canonical-labeling tools. This overhead and increased
symmetry reduction in particular means that our technique is best suited for constraint systems with hard combinatorial symmetry that is not easily capturable from
a set of generators, such as symmetry in combinatorial classification problems [28].
In addition to McKay’s [36] canonical extension framework, other standard frameworks for isomorph-free exhaustive generation in this context include orderly algorithms due to Faradžev [18] and Read [38], as well as the homomorphism principle
for group actions due to Kerber and Laue [30].
It is also possible to break symmetry within a constraint solver during the search
by dynamically adding constraints that rule out symmetric parts of the search space
(cf. [11, 19] and the references therein). If we use the nonisomorphic partial assignments produced by our technique as assumption sequences (cubes) in the incremental cube-and-conquer approach [22, 43], our technique can be seen as a restricted
way of breaking the symmetries in the beginning of the search, with the benefit—
as with cube-and-conquer—that the portions of the search space induced by the
partial assignments can be solved in parallel, either with complete independence
or with appropriate sharing of information (such as conflict clauses) between the
parallel nodes executing the search.
2. Preliminaries on group actions and symmetry
This section reviews relevant mathematical preliminaries and notational conventions for groups, group actions, symmetry, and isomorphism for our subsequent
development. (Cf. [10, 17, 25, 28, 29, 40] for further reference.)
2.1. Groups and group actions. Let Γ be a finite group and let Ω be a finite
set (the domain) on which Γ acts. For two groups Λ and Γ, let us write Λ ≤ Γ to
indicate that Λ is a subgroup of Γ. We use exponential notation for group actions,
and accordingly our groups act from the right. That is, for an object X ∈ Ω
and γ ∈ Γ, let us write X γ for the object in Ω obtained by acting on X with γ.
Accordingly, we have X (βγ) = (X β )γ for all β, γ ∈ Γ and X ∈ Ω. For a finite set
V , let us write Sym(V ) for the group of all permutations of V with composition of
mappings as the group operation.
2.2. Orbit and stabilizer, the automorphism group. For an object X ∈ Ω
let us write X Γ = {X γ : γ ∈ Γ} for the orbit of X under the action of Γ and
ΓX = {γ ∈ Γ : X γ = X} ≤ Γ for the stabilizer subgroup of X in Γ. Equivalently

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

5

we say that ΓX is the automorphism group of X and write Aut(X) = ΓX whenever
Γ is clear from the context; if we want to stress the acting group we write AutΓ (X).
We write Ω/Γ = {X Γ : X ∈ Ω} for the set of all orbits of Γ on Ω. For Λ ≤ Γ and
γ ∈ Γ, let us write Λγ = γ −1 Λγ = {γ −1 λγ : λ ∈ Λ} ≤ Γ for the γ-conjugate of Λ.
For all X ∈ Ω and γ ∈ Γ we have Aut(X γ ) = Aut(X)γ . That is, the automorphism
groups of objects in an orbit are conjugates of each other.
2.3. Isomorphism. We say that two objects are isomorphic if they are on the
same orbit of Γ in Ω. In particular, X, Y ∈ Ω are isomorphic if and only if there
exists an isomorphism γ ∈ Γ from X to Y that satisfies Y = X γ . An isomorphism
from an object to itself is an automorphism. Let us write Iso(X, Y ) for the set of
all isomorphisms from X to Y . We have that Iso(X, Y ) = Aut(X)γ = γAut(Y )
where γ ∈ Iso(X, Y ) is arbitrary. Let us write X ∼
= Y to indicate that X and Y
are isomorphic. If we want to stress the group Γ under whose action isomorphism
holds, we write X ∼
=Γ Y .
2.4. Elementwise action on tuples and sets. Suppose that Γ acts on two sets,
Ω and Σ. We extend the action to the Cartesian product Ω × Σ elementwise by
defining (X, S)γ = (X γ , S γ ) for all (X, S) ∈ Ω×Σ and γ ∈ Γ. Isomorphism extends
accordingly; for example, we say that (X, S) and (Y, T ) are isomorphic and write
(X, S) ∼
= (Y, T ) if there exists a γ ∈ Γ with Y = X γ and T = S γ . Suppose that
Γ acts on a set U . We extend the action of Γ on U to an elementwise action of Γ
on subsets W ⊆ U by setting W γ = {wγ : w ∈ W } for all γ ∈ Γ and W ⊆ U . In
what follows we will tacitly work with these elementwise actions on tuples and sets
unless explicitly otherwise indicated.
2.5. Canonical labeling and canonical form. A function κ : Ω → Γ is a canonical labeling map for the action of Γ on Ω if
(K) for all X, Y ∈ Ω it holds that X ∼
= Y implies X κ(X) = Y κ(Y )
(canonical labeling).
For X ∈ Ω we say that X κ(X) is the canonical form of X in Ω. From (K) it follows
that isomorphic objects have identical canonical forms, and the canonical labeling
map gives an isomorphism that takes an object to its canonical form.
We assume that the act of computing κ(X) for a given X produces as a side-effect
a set of generators for the automorphism group Aut(X).
3. McKay’s canonical extension method
This section reviews McKay’s [36] canonical extension method for isomorph-free
exhaustive generation. Mathematically it will be convenient to present the method
so that the isomorphism classes are captured as orbits of a group action of a group
Γ, and extension takes place in one step from “seeds” to “objects” being generated,
with the understanding that the method can be applied inductively in multiple
steps so that the “objects” of the current step become the “seeds” for the next
step. For completeness and ease of exposition, we also give a correctness proof for
the method. We stress that all material in this section is well known. (Cf. [28].)
3.1. Objects and seeds. Let Ω be a finite set of objects and let Σ be a finite set of
seeds. Let Γ be a finite group that acts on Ω and Σ. Let κ be a canonical labeling
map for the action of Γ on Ω.

6

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

3.2. Extending seeds to objects. Let us connect the objects and the seeds by
means of a relation e ⊆ Ω × Σ that indicates which objects can be built from which
seeds by extension. For X ∈ Ω and S ∈ Σ we say that X extends S and write XeS
if (X, S) ∈ e. We assume the relation e satisfies
(E1) e is a union of orbits of Γ, that is, eΓ = e (invariance), and
(E2) for every object X ∈ Ω there exists a seed S ∈ Σ such that XeS
(completeness).
For a seed S ∈ Σ, let us write e(S) = {X ∈ Ω : XeS} for the set of all objects that
extend S.
3.3. Canonical extension. We associate with each object a particular isomorphisminvariant extension by which we want to extend the object from a seed. A function
M : Ω → Σ is a canonical extension map if
(M1) for all X ∈ Ω it holds that (X, M (X)) ∈ e (extension), and
∼ Y implies (X, M (X)) =
∼
(M2) for all X, Y ∈ Ω we have that X =
(Y, M (Y )) (canonicity).
That is, (M1) requires that X is in fact an extension of M (X) and (M2) requires
that isomorphic objects have isomorphic canonical extensions. In particular, X 7→
(X, M (X)) is a well-defined map from Ω/Γ to e/Γ.
3.4. Generating objects from seeds. Let us study the following procedure,
which is invoked for exactly one representative S ∈ Σ from each orbit in Σ/Γ:
(P) Let S ∈ Σ be given as input. Iterate over all X ∈ e(S). Perform
zero or more isomorph rejection tests on X and S. If the tests
indicate we should accept X, visit X.
Let us first consider the case when there are no isomorph rejection tests.
Lemma 1. The procedure (P) visits every isomorphism class of objects in Ω at
least once.
Proof. To see that every isomorphism class is visited, let Y ∈ Ω be arbitrary. By
(E2), there exists a T ∈ Σ with YeT . By our assumption on how procedure (P)
is invoked, T is isomorphic to a unique S such that procedure (P) is invoked with
input S. Let γ ∈ Γ be an associated isomorphism with S γ = T . By (E1) and YeT ,
−1
we have XeS for X = Y γ . By the structure of procedure (P) we observe that X
is visited and X ∼
= Y . Since Y was arbitrary, all isomorphism classes are visited at
least once.

Let us next modify procedure (P) so that any two visits to the same isomorphism
class of objects originate from the same procedure invocation. Let M : Ω → Σ be a
canonical extension map. Whenever we construct X by extending S in procedure
(P), let us visit X if and only if
(T1) (X, S) ∼
= (X, M (X)).
Lemma 2. The procedure (P) equipped with the test (T1) visits every isomorphism
class of objects in Ω at least once. Furthermore, any two visits to the same isomorphism class must (i) originate by extension from the same procedure invocation on
input S, and (ii) belong to the same Aut(S)-orbit of this seed S.

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

7

Proof. Suppose that X is visited by extending S and Y is visited by extending T , with X ∼
= Y . By (T1) we must thus have (X, S) ∼
= (X, M (X)) and
∼
(Y, T ) = (Y, M (Y )). Furthemore, from (M2) we have (X, M (X)) ∼
= (Y, M (Y )).
Thus, (X, S) ∼
= (Y, T ) and hence S ∼
= T . Since S ∼
= T , we must in fact have
S = T by our assumption on how procedure (P) is invoked. Since X and Y
were arbitrary, any two visits to the same isomorphism class must originate by
extension from the same seed. Furthermore, we have (X, S) ∼
= (Y, S) and thus
X ∼
=Aut(S) Y . Let us next observe that every isomorphism class of objects is visited at least once. Indeed, let Y ∈ Ω be arbitrary. By (M1), we have YeM (Y ).
In particular, there is a unique S ∈ Σ with S ∼
= M (Y ) such that procedure (P) is
invoked with input S. Let γ ∈ Γ be an associated isomorphism with S γ = M (Y ).
−1
By (E1), we have XeS for X = Y γ . Furthermore, X ∼
= Y implies by (M2)
γ
that (X, M (X)) ∼
= (X, S), so (T1) holds and X is vis= (Y, M (Y )) = (X , S γ ) ∼
ited. Since X ∼
= Y and Y was arbitrary, every isomorphism class is visited at least
once.

Let us next observe that the outcome of test (T1) is invariant on each Aut(S)orbit of extensions of S.
Lemma 3. For all α ∈ Aut(S) we have that (T1) holds for (X, S) if and only if
(T1) holds for (X α , S).
Proof. From X ∼
= (X α , M (X α )). Thus,
= X α and (M2) we have (X, M (X)) ∼
α
α
α ∼
∼
(X, S) = (X, M (X)) if and only if (X , S) = (X , S ) = (X, S) ∼
= (X, M (X)) ∼
=
α
α
(X , M (X )).

Lemma 3 in particular implies that we obtain complete isomorph rejection by
combining the test (T1) with a further test that ensures complete isomorph rejection
on Aut(S)-orbits. Towards this end, let us associate an arbitrary order relation on
every Aut(S)-orbit on e(S). Let us perform the following further test:
(T2) X = min X Aut(S) .
The following lemma is immediate from Lemma 2 and Lemma 3.
Lemma 4. The procedure (P) equipped with the tests (T1) and (T2) visits every
isomorphism class of objects in Ω exactly once.
3.5. A template for canonical extension maps. We conclude this section by
describing a template of how to use an arbitrary canonical labeling map κ : Ω → Γ
to construct a canonical extension map M : Ω → Σ.
For X ∈ Ω construct the canonical form Z = X κ(X) . Using the canonical form
Z only, identify a seed T with ZeT . In particular, such a seed must exist by
(E2). (Typically this identification can be carried out by studying Z and finding
an appropriate substructure in Z that qualifies as T . For example, T may be the
minimum seed in Σ that satisfies ZeT . Cf. Lemma 9.) Once T has been identified,
−1
set M (X) = T κ(X) .
Lemma 5. The map X 7→ M (X) above is a canonical extension map.
−1

−1

Proof. By (E1) we have XeM (X) because Z κ(X) = X, T κ(X) = M (X), and
ZeT . Thus, (M1) holds for M . To verify (M2), let X, Y ∈ Ω with X ∼
= Y be
arbitrary. Since X ∼
= Y , by (K) we have X κ(X) = Z = Y κ(Y ) . It follows that
−1
−1
M (X) = T κ(X) and M (Y ) = T κ(Y ) , implying that γ = κ(X)κ(Y )−1 is an
isomorphism witnessing (X, M (X)) ∼

= (Y, M (Y )). Thus, (M2) holds for M .

8

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

4. Generation of partial assignments via a prefix sequence
This section describes an instantiation of McKay’s method that generates partial
assignments of values to a set of variables U one variable at a time following a prefix
sequence at the level of isomorphism classes given by the action of a group Γ on U .
Let R be a finite set where the variables in U take values.
4.1. Partial assignments, isomorphism, restriction. For a subset W ⊆ U
of variables, let us say that a partial assignment of values to W is a mapping
X : W → R. Isomorphism for partial assignments is induced by the following
group action.4 Let γ ∈ Γ act on X : W → R by setting X γ : W γ → R where X γ is
defined for all u ∈ W γ by
(3)

X γ (u) = X(uγ

−1

).

Lemma 6. The action (3) is well-defined.
Proof. We observe that for the identity  ∈ Γ of Γ we have X  = X. Furthermore,
for all γ, β ∈ Γ and u ∈ W γβ = (W γ )β we have
−1 
−1
−1 
−1 
X γβ (u) = X u(γβ)
= X (uβ )γ
= X γ uβ
= (X γ )β (u) .

For an assignment X : W → R, let us write X = W for the underlying set of
variables assigned by X. Observe that the underline map is a homomorphism of
group actions in the sense that X γ = X γ holds for all γ ∈ Γ and X : W → R. For
Q ⊆ X, let us write X|Q for the restriction of X to Q.
4.2. The prefix sequence and generation of normalized assignments. We
are now ready to describe the generation procedure. Let us begin by prescribing
the prefix sequence. Let u1 , u2 , . . . , uk be k distinct elements of U and let Uj =
{u1 , u2 , . . . , uj } for j = 0, 1, . . . , k. In particular we observe that
U0 ⊆ U1 ⊆ · · · ⊆ Uk
with Uj \ Uj−1 = {uj } for all j = 1, 2, . . . , k.
For j = 0, 1, . . . , k let Ωj consist of all partial assignments X : W → R with
W ∼
= Uj . Or what is the same, using the underline notation, Ωj consists of all
partial assignments X with X ∼
= Uj .
We rely on canonical extension to construct exactly one object from each orbit
of Γ on Ωj , using as seeds exactly one object from each orbit of Γ on Ωj−1 , for each
j = 1, 2, . . . , k. We assume the availability of canonical labeling maps κ : Ωj → Γ
for each j = 1, 2, . . . , k.
Our construction procedure will work with objects that are in a normal form to
enable precomputation for efficient execution of the subsequent tests for isomorph
rejection. Towards this end, let us say that X ∈ Ωj is normalized if X = Uj . It
is immediate from our definition of Ωj and (3) that each orbit in Ωj /Γ contains at
least one normalized object.
Let us begin with a high-level description of the construction procedure, to be
followed by the details of the isomorph rejection tests and a proof of correctness.
4For conciseness and accessibility, the present conference version develops the method only for
variable symmetries, and accordingly the group action (3) acts only on the variables in U and not
on the values in R. However, the method does extend to capture symmetries on both variables
in U and values in R (essentially by consideration of the Cartesian product U × R in place of U ),
and such an extension will be developed in a full version of this paper.

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

9

Fix j = 1, 2, . . . , k and study the following procedure, which we assume is invoked
for exactly one normalized representative S ∈ Ωj−1 from each orbit in Ωj−1 /Γ:
Aut(Uj−1 )

(P’) Let a normalized S ∈ Ωj−1 be given as input. For each p ∈ uj
and each r ∈ R, construct the assignment
X : Uj−1 ∪ {p} → R

defined by X(p) = r and X(u) = S(u) for all u ∈ Uj−1 . Perform the
isomorph rejection tests (T1’) and (T2’) on X and S. If both tests
accept, visit X ν(p) where ν(p) ∈ Aut(Uj−1 ) normalizes X.
From an implementation point of view, it is convenient to precompute the orbit
Aut(Uj−1 )
Aut(Uj−1 )
uj
together with group elements ν(p) ∈ Aut(Uj−1 ) for each p ∈ uj
that satisfy pν(p) = uj . Indeed, a constructed X with X = Uj−1 ∪ {p} can now be
normalized by acting with ν(p) on X to obtain a normalized X ν(p) isomorphic to
X.
4.3. The isomorph rejection tests. Let us now complete the description of procedure (P’) by describing the two isomorph rejection tests (T1’) and (T2’). This
subsection only describes the tests with an implementation in mind, the correctness
analysis is postponed to the following subsection.
Let us assume that the elements of U have been arbitrarily ordered and that
κ : Ωj → Γ is a canonical labeling map. Suppose that X has been constructed by
extending a normalized S with X = S ∪ {p} = Uj−1 ∪ {p}. The first test is:
(T1’) Subject to the ordering of U , select the minimum q ∈ U such that
−1
−1
Aut(Uj )
q κ(X) ν(p) ∈ uj
. Accept if and only if p ∼
=Aut(X) q κ(X) .
From an implementation perspective we observe that we can precompute the orbit
Aut(Uj )
uj
. Furthermore, the only computationally nontrivial part of the test is the
computation of κ(X) since we assume that we obtain generators for Aut(X) as a
side-effect of this computation. Indeed, with generators for Aut(X) available, it is
−1
easy to compute the orbits U/Aut(X) and hence to test whether p ∼
=Aut(X) q κ(X) .
Let us now describe the second test:
(T2’) Accept if and only if p = min pAut(S) subject to the ordering of U .
From an implementation perspective we observe that since S is normalized we
Aut(Uj−1 )
have Aut(S) ≤ Aut(S) = Aut(Uj−1 ) and thus the orbit uj
considered by
procedure (P’) partitions into one or more Aut(S)-orbits. Furthermore, generators
for Aut(S) are readily available (due to S itself getting accepted in the test (T1’)
Aut(Uj−1 )
at an earlier level of recursion), and thus the orbits uj
/Aut(S) and their
minimum elements are cheap to compute. Thus, a fast implementation of procedure
(P’) will in most cases execute the test (T2’) before the more expensive test (T1’).
4.4. Correctness. We now establish the correctness of procedure (P’) together
with the tests (T1’) and (T2’) by reduction to McKay’s framework and Lemma 4.
Fix j = 1, 2, . . . , k. Let us start by defining the extension relation e ⊆ Ωj × Ωj−1
for all X ∈ Ωj and S ∈ Ωj−1 by setting XeS if and only if
(4)

there exists a γ ∈ Γ such that X γ = Uj , S γ = Uj−1 , and X γ |Uj−1 = S γ .

This relation is well-defined in the context of McKay’s framework:

10

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

Lemma 7. The relation (4) satisfies (E1) and (E2).
Proof. From (4) it is immediate that (E1) holds. Furthermore, (E2) holds because
for an arbitrary X ∈ Ωj there exists a γ ∈ Γ with X γ = Uj , and thus XeS holds
−1
for S = T γ , where T is obtained from Y = X γ by deleting the assignment to the
variable uj .

The following lemma establishes that the iteration in procedure (P’) constructs
exactly the objects X ∈ e(S); cf. procedure (P).
Lemma 8. Let S ∈ Ωj−1 be normalized. For all X ∈ Ωj we have XeS if and only
Aut(Uj−1 )
with X = Uj−1 ∪ {p} and X|Uj−1 = S.
if there exists a p ∈ uj
Proof. From (4) we have that XeS if and only if there exists a γ ∈ Γ with X γ = Uj ,
S γ = Uj−1 , and X γ |Uj−1 = S γ . Since S is normalized, we have S = Uj−1 and
γ
hence Uj−1
= S γ = Uj−1 . Thus, γ ∈ Aut(Uj−1 ) and
X|Uj−1 = X γγ

−1

|Uj−1 = (X γ |Uj−1 )γ

−1

= (S γ )γ

−1

=S.

Thus, to establish the “only if” direction of the lemma, take p = uγj
“if” direction, take γ ∈ Aut(Uj−1 ) with pγ = uj .

−1

, and for the


Next we show the correctness of the test (T1’) by establishing that it is equivalent
with the test (T1) for a specific canonical extension function M . Towards this end,
let us use the assumed canonical labeling map κ : Ωj → Γ to build a canonical
extension function M using the template of Lemma 5. In particular, given an X ∈
Ωj as input with X = Uj−1 ∪ {p}, first construct the canonical form Z = X κ(X) . In
−1
Aut(Uj )
accordance with (T1’), select the minimum q ∈ U such that q κ(X) ν(p) ∈ uj
.
−1

Now construct M (X) from X by deleting the value of q κ(X) .
Lemma 9. The mapping X 7→ M (X) is well-defined and satisfies both (M1) and
(M2).
−1

Proof. Since Aut(Z) ≤ Aut(Z) and Z κ(X)
−1

Aut(Z)κ(X)

ν(p)

ν(p)

= Uj , we have
−1

≤ Aut(Z)κ(X)

ν(p)

= Aut(Uj ) .

It follows that the choice of q depends on Z and uj but not on the choices of κ(X) or
−1
ν(p). Furthermore, we observe that q ∈ Z and q κ(X) ∈ X. Thus, the construction
of M (X) is well-defined and (M2) holds by Lemma 5.
−1
Aut(Uj )
To verify (M1), observe that since q κ(X) ν(p) ∈ uj
, there exists an α ∈
−1

Aut(Uj ) with q κ(X) ν(p)α = uj . Thus, for γ = ν(p)α we have X γ = (Uj−1 ∪
−1
γ
{p})ν(p)α = Ujα = Uj , M (X) = (Uj \ {q κ(X) ν(p) })α = Uj−1 , and X γ |Uj−1 =
M (X)γ . Thus, from (4) we have XeM (X) and thus (M1) holds.

To complete the equivalence between (T1’) and (T1), observe that since X and
−1
p determine S by X|X\{p} = S, and similarly X and q κ(X) determine M (X) by
X|X\{qκ(X)−1 } = M (X), the test (T1) is equivalent to testing whether (X, p) ∼
=
κ(X)−1
κ(X)−1
∼
holds. Observe that this is
(X, q
) holds, that is, whether p =Aut(X) q
exactly the test (T1’).
It remains to establish the equivalence of (T2’) and (T2). We start with a lemma
that captures the Aut(S)-orbits considered by (T2).

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

11

Lemma 10. For a normalized S ∈ Ωj−1 the orbits in e(S)/Aut(S) are in a oneAut(Uj−1 )
/Aut(S)) × R.
to-one correspondence with the elements of (uj
Proof. From (3) we have Aut(S) ≤ Aut(S) = Aut(Uj−1 ) since S is normalized.
Furthermore, Lemma 8 implies that every extension X ∈ e(S) is uniquely deterAut(Uj−1 )
mined by the variable p ∈ uj
∩ X and the value X(p) ∈ R. Since the action
(3) fixes the values in R elementwise, for any X, X 0 ∈ e(S) we have X ∼
=Aut(S) X 0
0
0 0
∼
if and only if both p =Aut(S) p and X(p) = X (p ). The lemma follows.

Now order the elements X ∈ e(S) based on the lexicographic ordering of the pairs
Aut(Uj−1 )
(p, X(p)) ∈ uj
× R. Since the action (3) fixes the values in R elementwise,
we have that (T2’) holds if and only if (T2) holds for this ordering of e(S). The
correctness of procedure (P’) equipped with the tests (T1’) and (T2’) now follows
from Lemma 4.
4.5. Selecting a prefix. This section gives a brief discussion on how to select the
prefix. Let Uk = {u1 , u2 , . . . , uk } be the set of variables in the prefix sequence. It is
immediate that there exist |R|k distinct partial assignments from Uk to R. Let us
write RUk for the set of these assignments. The group Γ now partitions RUk into
orbits via the action (3), and it suffices to consider at most one representative from
each orbit to obtain an exhaustive traversal of the search space, up to isomorphism.
Our goal is thus to select the prefix Uk so that the setwise stabilizer ΓUk has comparatively few orbits on RUk compared with the total number of such assignments.
In particular, the ratio of the number of orbits |RUk /ΓUk | to the total number of
mappings |R|k can be viewed as a proxy for the achieved symmetry reduction and
as a rough5 proxy for the speedup factor obtained compared with no symmetry
reduction at all.
4.6. Subroutines. By our assumption, the canonical labeling map κ produces as
a side-effect a set of generators for the automorphism group Aut(X) for a given
input X. We also assume that generators for the groups Aut(Uj ) for j = 0, 1, . . . , k
can be precomputed by similar means. This makes the canonical labeling map
essentially the only nontrivial subroutine needed to implement procedure (P’). Indeed, the orbit computations required by tests (T1’) and (T2’) are implementable
by elementary permutation group algorithms [10, 40]. The next section describes
how to implement κ by reduction to vertex-colored graphs.6
5. Representation using vertex-colored graphs
This section describes one possible approach to represent the group of symmetries
Γ ≤ Sym(U ) of a system of constraints over a finite set of variables U taking values
5Here it should be noted that executing the symmetry reduction carries in itself a nontrivial
computational cost. That is, there is a tradeoff between the potential savings in solving the system
gained by symmetry reduction versus the cost of performing symmetry reduction. For example, if
the instance has no symmetry and Γ is a trivial group, then executing symmetry reduction merely
makes it more costly to solve the system.
6Reduction to vertex-colored graphs is by no means the only possibility to obtain the canonical labeling map to enable (P’), (T1’), and (T2’). Another possibility would be to represent Γ
directly as a permutation group and use dedicated permutation-group algorithms [33, 34]. Our
present choice of vertex-colored graphs is motivated by easy availability of carefully engineered
implementations for working with vertex-colored graphs.

12

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

in a finite set R. Our representation of choice will be vertex-colored graphs over
a fixed finite set of vertices V . In particular, isomorphisms between such graphs
are permutations γ ∈ Sym(V ) that map edges onto edges and respect the colors of
the vertices; that is, every vertex in V maps to a vertex of the same color under
γ. It will be convenient to develop the relevant graph representations in steps,
starting with the representation of the constraint system and then proceeding to the
representation of setwise stabilizers and partial assignments. These representations
are folklore (see e.g. [28]) and are presented here for completeness of exposition
only.

5.1. Representing the constraint system. To capture Γ ∼
= Aut(G) via a vertexcolored graph G with vertex set V , it is convenient to represent the variables U
directly as a subset of vertices U ⊆ V such that no vertex in V \ U has a color
that agrees with a color of a vertex in U . We then seek a graph G such that
Aut(G) ≤ Sym(U ) × Sym(V \ U ) projected to U is exactly Γ. In most cases
such a graph G is concisely obtainable by encoding the system of constraints with
additional vertices and edges joined to the vertices representing the variables in U .
We discuss two examples.
Example 1. Consider the system of clauses (1) and its graph representation (2).
The latter can be obtained as follows. First, introduce a blue vertex for each
of the six variables of (1). These blue vertices constitute the subset U . Then,
to accommodate negative literals, introduce a red vertex joined by an edge to the
corresponding blue vertex representing the positive literal. These edges between red
and blue vertices ensure that positive and negative literals remain consistent under
isomorphism. Finally, introduce a green vertex for each clause of (1) with edges
joining the clause with each of its literals. It is immediate that we can reconstruct
(1) from (2) up to labeling of the variables even after arbitrary color-preserving
permutation of the vertices of (2). Thus, (2) represents the symmetries of (1).
Let us next discuss an example where it is convenient to represent the symmetry
at the level of original constraints rather than at the level of clauses.
Example 2. Consider the following system of eight cubic equations over 24 variables
taking values modulo 2:
x11 y11 z11 + x12 y12 z12 + x13 y13 z13
x11 y11 z21 + x12 y12 z22 + x13 y13 z23
x11 y21 z11 + x12 y22 z12 + x13 y23 z13
x11 y21 z21 + x12 y22 z22 + x13 y23 z23

=0
=0
=1
=1

x21 y11 z11 + x22 y12 z12 + x23 y13 z13
x21 y11 z21 + x22 y12 z22 + x23 y13 z23
x21 y21 z11 + x22 y22 z12 + x23 y23 z13
x21 y21 z21 + x22 y22 z22 + x23 y23 z23

=0
=1
=1
=1

This system seeks to decompose a 2 × 2 × 2 tensor (whose elements appear on
the right hand sides of the equations) into a sum of three rank-one tensors. The
symmetries of addition and multiplication modulo 2 imply that the symmetries of
the system can be represented by the following vertex-colored graph:

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION
x11

×

x12

×

×

+

x13

×

x21

×

x22

×

×

+

x23

×

+

0

y11

×

y12

×

y13

×

+

×

y21

×

y22

×

+

y23

×

×

z11

×

z12

×

z13

×

+

z21

×

+

×

13
z22

z23

×

×

×

+

1

Indeed, we encode each monomial in the system with a product-vertex, and group
these product-vertices together by adjacency to a sum-vertex to represent each
equation, taking care to introduce two uniquely colored constant-vertices to represent the right-hand side of each equation.
Remark. The representation built directly from the system of polynomial equations
in Example 2 concisely captures the symmetries in the system independently of the
final encoding of the system (e.g. as CNF) for solving purposes. In particular,
building the graph representation from such a final CNF encoding (cf. Example 1)
results in a less compact graph representation and obfuscates the symmetries of the
original system, implying less efficient symmetry reduction.
5.2. Representing the values. In what follows it will be convenient to assume
that the graph G contains a uniquely colored vertex for each value in R. (Cf. the
graph in Example 2.) That is, we assume that R ⊆ V \U and that Aut(G) projected
to R is the trivial group.
5.3. Representing setwise stabilizers in the prefix chain. To enable procedure (P’) and the tests (T1’) and (T2’), we require generators for Aut(Uj ) ≤ Γ for
each j = 0, 1, . . . , k. More generally, given a subset W ⊆ U , we seek to compute a
set of generators for the setwise stabilizer AutΓ (W ) = ΓW = {γ ∈ Γ : W γ = W },
with W γ = {wγ : w ∈ W }. Assuming we have available a vertex-colored graph
G that represents Γ by projection of AutSym(V ) (G) to U , let us define the graph
G ↑ W by selecting one vertex r ∈ R and joining each vertex w ∈ W with an edge
to the vertex r. It is immediate that AutSym(V ) (G ↑ W ) projected to U is precisely
AutΓ (W ).
5.4. Representing partial assignments. Let X : W → R be an assignment of
values in R to variables in W ⊆ U . Again to enable procedure (P’) together with
the tests (T1’) and (T2’), we require a canonical labeling κ(X) and generators for
the automorphism group Aut(X). Again assuming we have a vertex-colored graph
G that represents Γ, let us define the graph G ↑ X by joining each vertex w ∈ W
with an edge to the vertex X(w) ∈ R. It is immediate that AutSym(V ) (G ↑ X)
projected to U is precisely AutΓ (X). Furthermore, a canonical labeling κ(X) can
be recovered from κ(G ↑ X) and the canonical form (G ↑ X)κ(G↑X) .
5.5. Using tools for vertex-colored graphs. Given a vertex-colored graph G as
input, practical tools exist for computing a canonical labeling κ(G) ∈ Sym(V ) and a
set of generators for Aut(G) ≤ Sym(V ). Such tools include bliss [27], nauty [35, 37],
and traces [37]. Once the canonical labeling and generators are available in Sym(V )
it is easy to map back to Γ by projection to U so that corresponding elements of Γ
are obtained.

14

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

6. Preliminary experimental evaluation
This section documents a preliminary and limited experimental evaluation of an
implementation of the adaptive prefix-assignment technique. The implementation
is written in C and structured as a preprocessor that works with an explicitly given
graph representation and utilizes the nauty [35, 37] canonical labeling software for
vertex-colored graphs as a subroutine.
6.1. Instances. We study systems of polynomial equations aimed at discovering
the tensor rank of a small m × m × m tensor T = (tijk ) modulo 2, with tijk ∈ {0, 1}
and i, j, k = 1, 2, . . . m. Computing the rank of a given tensor is NP-hard [21].7 In
precise terms, we seek to find the minimum r such that there exist three m × r
matrices A, B, C ∈ {0, 1}m×r such that for all i, j, k = 1, 2, . . . , m we have
(5)

r
X

ai` bj` ck` = tijk

(mod 2) .

`=1

Such instances are easily compilable into CNF with A, B, C constituting three matrices of Boolean variables so that the task becomes to find the minimum r such
that the compiled CNF instance is satisfiable. Independently of the target tensor
T such instances have a symmetry group of order at least r! due to the fact that
the columns of the matrices A, B, C can be arbitrarily permuted so that (5) maps
to itself. In our experiments we select the entries of T uniformly at random so that
the number of 1s in T is exactly n.
6.2. Hardware and software configuration. The experiments were performed
on a cluster of Dell PowerEdge C4130 compute nodes, each equipped with two
Intel Xeon E5-2680v3 CPUs and 128 GiB of main memory, running Linux version
3.10.0514.10.2.el7.x86 64. All experiments were executed by allocating a single
core on a single CPU of a compute node. Other unrelated compute load was in
general present on the nodes during the experiments. A time-out of five hours of
CPU time was applied.
6.3. Symmetry reduction tools and SAT solvers. We report on three methods for symmetry reduction on aforementioned tensor-rank instances: (1) no reduction (“raw”), (2) breakid version 2.2 [16], (3) our technique (“reduce”) with
a user-selected prefix consisting of 2r variables that constitute the first two rows
of the matrix A, and a graph representation of (5) as in Example 2. Three different SAT solvers were used in the experiments: lingeling and ilingeling version bbc-9230380 [7], and glucose version 4.1 [6]. We use the incremental solver
ilingeling together with the incremental CNF output of reduce.
6.4. Results. Table 1 shows the results of a tensor rank computation modulo 2 for
two random tensors T with m = 5, n = 16 and m = 5, n = 18. In both cases we
observe that the rank is 9. The running times displayed in the table are in seconds,
with “t/o” indicating a time-out. For both tensors we observe decreased running
time due to symmetry reduction, with reduce performing better than breakid, but
also taking more time to perform the preprocessing (indicated in columns labelled
7Yet considerable interest exists to determine tensor ranks of small tensors, in particular tensors
that encode and enable fast matrix multiplication algorithms; cf. [1, 2, 3, 4, 8, 9, 13, 24, 32, 41, 44].

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

15

Table 1. Computing tensor rank for two 5 × 5 × 5 tensors
raw
preproc.
breakid
preproc.
reduce
m r n glucose lingeling breakid glucose lingeling reduce glucose lingeling ilingeling Sat?
5
5
5
5
5
5

6
7
8
9
10
11

16
16
16
16
16
16

60.02
t/o
t/o
3.20
0.99
0.16

114.14
t/o
t/o
23.78
12.56
33.17

0.06
0.19
0.12
0.07
0.07
0.28

36.01
t/o
t/o
1.20
0.69
0.09

81.86
t/o
t/o
158.44
21.49
52.71

0.29
1.07
2.56
5.03
9.06
16.24

3.70
372.43
t/o
0.72
30.64
1.37

9.67
7.28
614.04 249.10
t/o 15316.01
149.82
1.16
166.37
0.80
6.36
1.48

no
no
no
yes
yes
yes

5
5
5
5
5
5

6
7
8
9
10
11

18 14.37
18 4606.30
18
t/o
18 395.75
18 13.05
18 19.47

31.34
t/o
t/o
444.84
22.03
43.68

0.23 11.05
0.18 3604.87
0.06
t/o
0.06
2.68
0.07
3.79
0.22 27.29

23.96
t/o
t/o
209.66
356.18
859.40

0.53
2.79
1.01 114.77
3.23 6901.79
5.93
40.32
10.46
7.75
17.11
31.86

2.90
4.25
116.80
94.89
t/o 3867.00
39.21
1.32
11.67
1.45
112.62
1.42

no
no
no
yes
yes
yes

with “preproc.”) due to repeated calls to the canonical labeling software. Further
experiments are documented in Appendix A.
Remark. We would like to highlight that the comparison between reduce and
breakid in particular illustrates the relevance of a graph representation of the
symmetries in (5), which are not easily discoverable from the compiled CNF. In
our experiments reduce receives as input the graph representation of the system
(5) constructed as in Example 2, whereas breakid works on the compiled CNF
input alone.
Acknowledgements. The research leading to these results has received funding
from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement 338077 “Theory and
Practice of Advanced Search and Enumeration” (M.K., P.K., and J.K.). We gratefully acknowledge the use of computational resources provided by the Aalto ScienceIT project at Aalto University. We thank Tomi Janhunen for useful discussions.
References
1. V. B. Alekseev, On bilinear complexity of multiplication of 5 × 2 matrix by 2 × 2 matrix,
Physics and mathematics, vol. 156, Uchenye Zapiski Kazanskogo Universiteta. Seriya FizikoMatematicheskie Nauki, no. 3, Kazan University, Kazan, 2014, pp. 19–29.
2.
, On bilinear complexity of multiplication of m × 2 and 2 × 2 matrices, Chebyshevskii
Sb. 16 (2015), no. 4, 11–27.
3. V. B. Alekseev and A. V. Smirnov, On the exact and approximate bilinear complexities of
multiplication of 4 × 2 and 2 × 2 matrices, Proceedings of the Steklov Institute of Mathematics
282 (2013), no. 1, 123–139.
4. V. B. Alekseyev, On the complexity of some algorithms of matrix multiplication, Journal of
Algorithms 6 (1985), no. 1, 71–85.
5. F. A. Aloul, K. A. Sakallah, and I. L. Markov, Efficient symmetry breaking for boolean satisfiability, Proc. IJCAI 2003, Morgan Kaufmann, 2003, pp. 271–276.
6. G. Audemard and L. Simon, Extreme cases in sat problems, Proc. SAT 2016, Lecture Notes
in Computer Science, vol. 9710, Springer, 2016, pp. 87–103.
7. A. Biere, Splatz, lingeling, plingeling, treengeling, yalsat entering the sat competition 2016,
Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions, Department of
Computer Science Series of Publications, vol. B-2016-1, University of Helsinki, 2016, pp. 44–
45.

16

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

8. M. Bläser, Lower bounds for the multiplicative complexity of matrix multiplication, Computational Complexity 8 (1999), no. 3, 203–226.
9. M. Bläser, On the complexity of the multiplication of matrices of small formats, Journal of
Complexity 19 (2003), no. 1, 43–60.
10. G. Butler, Fundamental algorithms for permutation groups, Lecture Notes in Computer Science, vol. 559, Springer, 1991.
11. G. Chu, M. G. de la Banda, C. Mears, and P. J. Stuckey, Symmetries, almost symmetries,
and lazy clause generation, Constraints 19 (2014), no. 4, 434–462.
12. M. Codish, G. Gange, A. Itzhakov, and P. J. Stuckey, Breaking symmetries in graphs: The
nauty way, Proc. CP 2016, Lecture Notes in Computer Science, vol. 9892, Springer, 2016,
pp. 157–172.
13. N. T. Courtois, D. Hulme, and T. Mourouzis, Multiplicative complexity and solving generalized Brent equations with SAT solvers, Proceedings of the third international conference
on computational logics, algebras, programming, tools, and benchmarking (COMPUTATION
TOOLS 2012), 2012, pp. 22–27.
14. J. M. Crawford, M. L. Ginsberg, E. M. Luks, and A. Roy, Symmetry-breaking predicates for
search problems, Proc. KR 1996, Morgan Kaufmann, 1996, pp. 148–159.
15. P. T. Darga, M. H. Liffiton, K. A. Sakallah, and I. L. Markov, Exploiting structure in symmetry
detection for CNF, Proc. DAC 2004, ACM, 2004, pp. 530–534.
16. J. Devriendt, B. Bogaerts, M. Bruynooghe, and M. Denecker, Improved static symmetry
breaking for SAT, Proc. SAT 2016, Lecture Notes in Computer Science, vol. 9710, Springer,
2016, pp. 104–122.
17. J. D. Dixon and B. Mortimer, Permutation groups, Graduate Texts in Mathematics, vol. 163,
Springer, 1996.
18. I. A. Faradžev, Constructive enumeration of combinatorial objects, Problèmes Combinatoires
et Théorie des Graphes (Paris), Colloq. Internat. CNRS, no. 260, CNRS, 1978, pp. 131–135.
19. I. P. Gent, K. E. Petrie, and J.-F. Puget, Symmetry in constraint programming, Handbook of
Constraint Programming, Foundations of Artificial Intelligence, vol. 2, Elsevier, 2006, pp. 329–
376.
20. M. Hall, Jr. and D. E. Knuth, Combinatorial analysis and computers, Amer. Math. Monthly
72 (1965), no. 2, part 2, 21–28.
21. J. Håstad, Tensor rank is NP-complete, J. Algorithms 11 (1990), no. 4, 644–654. MR 1079455
22. M. Heule, O. Kullmann, S. Wieringa, and A. Biere, Cube and conquer: Guiding CDCL
SAT solvers by lookaheads, Proc. HVC 2011, Lecture Notes in Computer Science, vol. 7261,
Springer, 2011, pp. 50–65.
23. M. J. H. Heule, The quest for perfect and compact symmetry breaking for graph problems,
Proc. SYNASC 2016, IEEE Computer Society, 2016, pp. 149–156.
24. J. E. Hopcroft and L. R. Kerr, On minimizing the number of multiplications necessary for
matrix multiplication, SIAM Journal on Applied Mathematics 20 (1971), no. 1, 30–36.
25. J. F. Humphreys, A course in group theory, Oxford University Press, Oxford, 1996.
26. A. Itzhakov and M. Codish, Breaking symmetries in graph search with canonizing sets, Constraints 21 (2016), no. 3, 357–374.
27. T. Junttila and P. Kaski, Engineering an efficient canonical labeling tool for large and sparse
graphs, Proc. ALENEX 2007, SIAM, 2007.
28. P. Kaski and P. R. J. Östergård, Classification algorithms for codes and designs, Algorithms
and Computation in Mathematics, no. 15, Springer-Verlag, 2006.
29. A. Kerber, Applied finite group actions, 2nd ed., Algorithms and Combinatorics, vol. 19,
Springer, 1999.
30. A. Kerber and R. Laue, Group actions, double cosets, and homomorphisms: Unifying concepts
for the constructive theory of discrete structures, Acta Appl. Math. 52 (1998), no. 1–3, 63–90.
31. D. E. Knuth, The art of computer programming. Vol. 4A. Combinatorial algorithms. Part 1,
Addison-Wesley, 2011. MR 3444818
32. J. D. Laderman, A noncommutative algorithm for multiplying 3 × 3 matrices using 23 multiplications, Bull. Amer. Math. Soc. 82 (1976), 126–128.
33. J. S. Leon, Permutation group algorithms based on partitions, I: Theory and algorithms,
Journal of Symbolic Computation 12 (1991), no. 4–5, 533–583.

ADAPTIVE PREFIX-ASSIGNMENT FOR SYMMETRY REDUCTION

34.

35.
36.
37.
38.
39.
40.
41.
42.
43.
44.

17

, Partitions, refinements, and permutation group computation, Groups and Computation, II, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, no. 28,
American Mathematical Society, 1997, pp. 123–158.
B. D. McKay, Practical graph isomorphism, Congressus Numerantium 30 (1981), 45–87.
B. D. McKay, Isomorph-free exhaustive generation, J. Algorithms 26 (1998), no. 2, 306–324.
B. D. McKay and A. Piperno, Practical graph isomorphism, II, J. Symb. Comput. 60 (2014),
94–112.
R. C. Read, Every one a winner; or, How to avoid isomorphism search when cataloguing
combinatorial configurations, Ann. Discrete Math. 2 (1978), 107–120.
K. A. Sakallah, Symmetry and satisfiability, Handbook of Satisfiability, Frontiers in Artificial
Intelligence and Applications, vol. 185, IOS Press, 2009, pp. 289–338.
Á. Seress, Permutation group algorithms, Cambridge University Press, Cambridge, 2003.
V. Strassen, Gaussian elimination is not optimal, Numer. Math. 13 (1969), no. 4, 354–356.
J. D. Swift, Isomorph rejection in exhaustive search techniques, Combinatorial Analysis,
American Mathematical Society, 1960, pp. 195–200.
S. Wieringa, The icnf file format, http://www.siert.nl/icnf/, 2011, accessed in April 2017.
S. Winograd, On multiplication of 2 × 2 matrices, Linear Algebra and its Applications 4
(1971), no. 4, 381–388.

Appendix A. Experiments with matrix-multiplication tensors
This appendix documents experiments with tensors that represent matrix multiplication. That is, the task of multiplying an a × b matrix with a b × c matrix to
yield an a × c product matrix is captured by the ab × bc × ac tensor T with entries
(
1 if i = i0 , j = j 0 , and k = k 0 ;
(6)
t(i,j 0 ),(j,k),(i0 ,k0 ) =
0 otherwise
for all i, i0 = 1, 2, . . . , a, j, j 0 = 1, 2, . . . , b, and k, k 0 = 1, 2, . . . , c.
A.1. The case a = b = c = 2. The table below displays running times in seconds
(symmetry breaking and solver combined) to discover Strassen’s [41] matrix multiplication algorithm (modulo 2) by solving the system (5) with the right-hand side
equal to (6) for a = b = c = 2. The columns “reduce (1)”, “reduce (2)” and “reduce
(3)” refer to different choices of prefix, namely taking as the prefix the 1 × r, 2 × r,
and the 3 × r submatrix of the matrix A, respectively. The abbreviation “ling.”
stands for the lingeling solver and “iling.” for ilingeling.
raw
breakid
reduce (1)
reduce (2)
reduce (3)
r glucose ling. glucose ling. glucose ling. iling. glucose ling. iling. glucose ling. iling.
6
51.57 164.19
34.73 57.59
4.69 7.69 8.07
4.33 8.23 6.19
7.31 18.49 8.77
7
0.07 0.34
0.36 0.66
1.19 1.55 0.20
0.95 5.35 0.97
15.39 21.27 15.29

We observe that this instance is small enough so that the rank 7 can be recovered
even without symmetry reduction, but symmetry reduction clearly decreases the
running times in the unsatisfiable instance.
A.2. The case a = b = 2, c = 3. The table below displays running times in
seconds (symmetry breaking and solver combined) for the case a = b = 2 and
c = 3. In this case the rank is known to be 11 [4, 24], so instances with r ≤ 10
are unsatisfiable. For the unsatisfiable instances the running times increase quickly
with increasing r, with reduce supplying the best performance used in incremental
mode with ilingeling. For the satisfiable instance with r = 11 the results are more
varied. Runs that did not finish in 25 hours are marked with “t/o”, and “mem.”
marks a case where the solver failed due to insufficient memory allocation.

18

TOMMI JUNTTILA, MATTI KARPPA, PETTERI KASKI, AND JUKKA KOHONEN

raw
breakid
reduce (1)
reduce (2)
r glucose ling. glucose
ling. glucose lingelig iling. glucose
ling. iling.
6
25.9 91.6
22.8
38.2
2.8
5.4
6.5
2.1
2.9
2.4
7 24246.3 t/o 11914.1 16007.1 110.3 412.3 211.8
7.1
7.9 14.9
8
t/o t/o
t/o
t/o
t/o
t/o
t/o 197.0
211.9 200.3
9
t/o t/o
t/o
t/o
t/o
t/o
t/o 9266.3
t/o t/o
10
t/o t/o
t/o
t/o
t/o
t/o
t/o
t/o
t/o t/o
11
t/o t/o
21.5 29182.2
t/o
t/o 5869.6 3295.8 20119.9 63.7

reduce (3)
glucose ling. iling.
31.5
39.8
31.4
160.9 212.7 160.2
1123.2 3840.9 921.6
66858.1
t/o 8295.2
t/o mem.
t/o
12107.0 6018.6 5817.9

Aalto University, Department of Computer Science
E-mail address: Tommi.Junttila@aalto.fi
Aalto University, Department of Computer Science
E-mail address: Matti.Karppa@aalto.fi
Aalto University, Department of Computer Science
E-mail address: Petteri.Kaski@aalto.fi
Aalto University, Department of Computer Science
Current address: University of Helsinki, Department of Computer Science
E-mail address: Jukka.Kohonen@cs.helsinki.fi

