Breaking Symmetries with Lex Implications

Abstract

Breaking symmetries is crucial when solving hard combinatorial problems. A common way to eliminate symmetries in CP/SAT is to add symmetry breaking constraints. Ideally, symmetry breaking constraints should be complete and compact. The aim of this paper is to find compact and complete symmetry breaks applicable when solving hard combinatorial problems using CP/SAT approach. In particular: graph search problems and matrix model problems where symmetry breaks are often specified in terms of lex constraints. We show that sets of lex constraints can be expressed with only a small portion of their inner lex implications which are a particular form of Horn clauses. We exploit this fact and compute a compact encoding of the row-wise LexLeader and state of the art partial symmetry breaking constraints. We illustrate the approach for graph search problems and matrix model problems.

Supported by the Israel Science Foundation, grant 625/17 and the German Federal Ministry of Education and Research, combined project 01IH15006A.

1 Introduction

When solving hard combinatorial problems, symmetry breaks play a crucial role. When seeking solutions, the size of the search space is significantly reduced if symmetries are eliminated. The search space can be explored more efficiently when avoiding paths that lead to symmetric solutions and avoiding also those that lead to symmetric non-solutions.

This paper deals with variable symmetry in constraint staisfaction problems (CSP) where symmetry is a permutation defined over a set of variables that preserves solutions. Given a CSP with variables $x_1, ..., x_n$, we say that $\sigma$ is a symmetry if for every assignment $\mu = \{x_1=i_1, ..., x_n=i_n\}$, $\mu$ is a solution if and only if $\{x_1=i_{\sigma (1)}, ..., x_n=i_{\sigma (n)}\}$ is also a solution.

One common approach to eliminate symmetries is to introduce symmetry breaking constraints [1,2,3,4] which rule out isomorphic solutions thus reducing the size of the search space while preserving the set of solutions. Ideally, a symmetry breaking constraint is satisfied by a single member of each equivalence class of solutions, in which case it is said to be complete. However, computing such symmetry breaking constraints is, most often, intractable [2]. In practice, symmetry breaking constraints are often partial, and typically rule out some, but not all of the symmetries in the search. As noted in the survey by Walsh [5], often a few simple constraints rule out most of the symmetries.

In many cases, symmetry breaking constraints, complete or partial, are expressed in terms of lex constraints on the variables of the problem. Each lex constraint, corresponds to one symmetry $\sigma$, and restricts the search space to consider assignments which are lexicographically smaller than their permuted form obtained according to $\sigma$. Typical examples are: graph search problems [6] where rows and columns of the Boolean adjacency matrix can be reordered by some permutation, and matrix models where rows and columns can be reordered by a pair of permutations. For matrix models common partial symmetry breaks described in terms of lex constraints include doubleLex [7] (denoted also $lex ^2$ in [8]) and snake-lex [9]. For graph search problems, Codish et al. [6] introduce partial symmetry breaks (denoted $\textsf {sb}_\ell$ and $\textsf {sb}^*_\ell$) which are refinements of doubleLex for adjacency matrices.

Complete symmetry breaks can be obtained, for both types of problems, by introducing a lex constraint for each reordering of the combinatorial object (graph or matrix) [10]. For matrices, the reordering takes place by permuting rows and columns [7]. For graphs, symmetric solutions can be obtained by permutations of the vertices, which corresponds to simultaneously permuting both rows and columns of the adjacency matrix. However, the number of lex constraints is overwhelming.

The aim of this research is to find compact and complete symmetry breaks applicable when solving hard combinatorial problems. In particular: graph search problems and matrix model problems.

In previous work, Itzhakov and Codish [11] present complete and compact symmetry breaks for graphs based on so-called canonizing sets of permutations where each permutation represents a lex constraint. Their approach is based on the observation that many of the lex constraints expressed in terms of all permutations (of rows and columns of the adjacency matrix) are redundant. Itzhakov and Codish [11] compute compact symmetry breaking constraints for graphs with 10 or less vertices. They observe, for example, that for 10 vertices 7, 853 lex constraints suffice to provide a complete symmetry break instead of the $10!=3{,}628{,}800$ constraints introduced by the definition. Itzhakov and Codish [11] report that this symmetry break takes 4 days to compute.

Heule [12] poses the question: How expensive is it to break all graph symmetries? Heule seeks an answer in terms of the number of clauses in a CNF representation of the corresponding symmetry breaking constraint. For up to $n=5$ vertices, Heule computes size-optimal compact and complete symmetry breaks. A size-optimal complete symmetry break for graphs with 5 vertices consists of only 12 clauses. In contrast, the symmetry break computed by Itzhakov and Codish consists of 7 lex constraints, which can be encoded in 83 clauses. For $5<n\le 8$ vertices, Heule computes complete symmetry breaks which are significantly smaller than those computed by Itzhakov and Codish but which are not determined to be optimal. For 8 vertices, the complete symmetry break computed by Heule consists of 956 clauses (and takes two days to compute). The complete symmetry break computed by Itzhakov and Codish consists of 135 lex constraints (2724 clauses) and as reported in [11] takes 6 min to compute.

Frisch and Harvey illustrate in [13] the redundancies in a complete symmetry break in a three-by-two matrix. They show how to simplify the 11 lex constraints expressing all reorderings of rows and columns. The resulting symmetry break has 8 simplified lex constraints.

In this paper we note the standard decomposition of a lex constraint of the form $x_1\ldots x_n \le _{lex} y_1\ldots y_n$ to a conjunction of Horn clauses of the form

$$(x_1=y_1),\ldots ,(x_k=y_k) \rightarrow x_{k+1}\le y_{k+1}$$

where the literals on the left side are equalities between the variables in the lex constraint and $1\le k < n$ [14]. We call clauses of this form lex implications. We observe that many of the lex implications in the decomposition of the complete symmetry breaks derived in [11] are redundant. This enables to significantly reduce the size of the symmetry breaking constraints. For example, for $n=10$ vertices, a complete symmetry break is obtained in [11] with 7,853 lex constraints. These decompose to 248,604 lex implications which can be reduced (removing implications implied by the others) to a complete symmetry break expressed using only 21,844 lex implications. For 5 vertices, the complete symmetry break computed in [11] involves 7 lex constraints which decompose to 41 lex implications. These can be reduced to 14 non-redundant lex implications and 40 clauses, cf. Example 3. For 8 vertices, the complete symmetry break computed in [11] involves 135 lex constraints which decompose to 2006 lex implications (2724 clauses). These can be reduced to 387 non-redundant lex implications (1077 clauses), c.f. Table 2.

Given the observation that so many lex implications are redundant, we then pose the direct question: how many lex implications are required to express a complete symmetry break on a graph with n nodes. We generate such symmetry breaks directly and not by reducing the complete symmetry breaks presented in [11]. A compact and complete symmetry break for graphs with 8 vertices can be computed in about 1 min. A compact and complete symmetry break for 10 vertices can now be computed in roughly 3 h (in contrast to 4 days as reported in [11]. Moreover, we compute a compact and complete symmetry break for graphs with 11 vertices. This symmetry break consists in 274, 109 lex implications (280, 049 clauses) and is computed in 8 days.

The technique of representing conjunctions of lex constraints in terms of non-redundant lex implications works also for matrix models where symmetry breaks are also defined in terms of lex constraints (swapping rows and columns) and also for partial symmetry breaks for graphs and matrix models.

We analyze the standard doubleLex constraint and observe that it has no redundancies when represented as lex implications. However when using extensions which we call $lex^+$ and $lex^*$ (also known as swapNext and swapAny respectively [15]) there are many redundancies. We give compact versions of these (without the redundancies).

The rest of the paper is organized as follows. In the next section we introduce notation and basic concepts. In Sect. 3 we illustrate the effect of removing redundancy in encoding symmetry breaking constraints. In Sect. 4 we define our approach to efficiently generating compact and complete symmetry breaking constraints, and illustrate the effectiveness on graphs. Finally in Sect. 6 we conclude.

The computations throughout the paper are performed using the finite-domain constraint compiler BEE [16] which compiles constraints to CNF, and solves it applying an underlying SAT solver. We use Glucose 4.0 [17] as the underlying SAT solver except where specified that we used Clasp 3.1.3 [18]. All computations were performed on an Intel E8400 core, clocked at 2 GHz, able to run a total of 12 parallel threads. Each of the cores in the cluster has computational power comparable to a core on a standard desktop computer. Each SAT instance is run on a single thread, and all running times reported in this paper are CPU times.

2 Preliminaries

In this paper, we consider Boolean formulas $\varphi$ which encode the set of solutions of combinatorial problems. In many cases, there are variable symmetries in the solution space of such problems. This is, given a solution $x_i = v_i$ there often exist permutations $\pi$ such that $x_{\pi (i)} = v_i$ is an isomorphic solution [4].

When enumerating the solutions for a particular problem, it is often preferable to consider only non-isomorphic solutions. Furthermore, if one wishes to prove that no solutions for some problem exist, breaking symmetries often allows for smaller proofs.

In order to decrease the size of the solution space, one approach is to use constraints $\psi$ which break symmetries in the solution space of $\varphi$. This is, for every solution x which satisfies $\varphi$, there exists an isomorphic solution $x'$ which satisfies $\varphi \wedge \psi$. Symmetry breaking constraints which rule out all but one solution from each equivalence class are called complete. Symmetry breaking constraints which rule out some but not all isomorphic solutions from an equivalence class are called partial [2].

We consider finite and simple graphs (undirected with no self loops). The set of simple graphs on n nodes is denoted $\mathcal{G}_n$. We assume that the vertex set of a graph, $G = (V,E)$, is $V=\{1,\ldots ,n\}$ and represent G by its $n\times n$ Boolean adjacency matrix. We often let G denote both the graph itself and also its adjacency matrix.

Graph search problems are about the search for a graph which satisfies a given set of constraints, $\varphi$, or to determine that no such graph exists. In this setting the unknown graph is represented by an adjacency matrix consisting of Boolean variables which are constrained by $\varphi$. Often graph search problems are about the search for the set of all graphs, modulo graph isomorphism, that satisfy the given constraints.

The set of permutations $\pi :\{1,\ldots ,n\}\rightarrow \{1,\ldots ,n\}$ is denoted $S_n$. Permutations act on adjacency matrices in the natural way: If A is the adjacency matrix of a graph G and $\pi$ is a permutation, then $\pi (A)$ is the adjacency matrix obtained by simultaneously permuting with $\pi$ the rows and columns of A.

Fig. 1.

The $5\times 5$ Boolean adjacency matrix G and $\pi (G)$ for $\pi = (2,1,3,4,5)$.

Two graphs $G_1,G_2\in \mathcal{G}_n$ are isomorphic, denoted $G_1\approx G_2$, if there exists a permutation $\pi \in S_n$ such that $G_1 = \pi (G_2)$. Sometimes we write $G_1\approx _\pi G_2$ to emphasize that $\pi$ is the permutation such that $G_1=\pi (G_2)$. For sets of graphs $H_1, H_2$, we say that $H_1\approx H_2$ if for every $G_1\in H_1$ (likewise in $H_2$) there exists $G_2\in H_2$ (likewise in $H_1$) such that $G_1\approx G_2$.

We consider an ordering on graphs, defined by representing their adjacency matrices as strings. Because adjacency matrices are symmetric with zeroes on the diagonal, it suffices to focus on the upper triangle parts of the matrices [19].

Definition 1 (ordering graphs)

Let $G_1,G_2 \in \mathcal{G}_n$ and let $s_1, s_2$ be the strings obtained by concatenating the rows of the upper triangular parts of their corresponding adjacency matrices $A_1, A_2$ respectively. Then, $G_1 \preceq G_2$ if and only if $s_1\preceq _{lex} s_2$. We also write $A_1 \preceq A_2$.

A classic complete symmetry break for graphs is the LexLeader constraint [10] defined as follows:

Definition 2 (LexLeader)

$\textsc {LexLeader}(n) = \bigwedge \left\{ ~G \preceq \pi (G) \left| \begin{array}{l}\pi \in S_n\end{array} \right. \right\}$ where G is an $n\times n$ matrix of Boolean variables with 0’s on the diagonal and such that $G_{ij}=G_{ji}$ for all $1\le i<j\le n$. Sometimes we write $\textsc {LexLeader}_G(n)$ to make G explicit.

Example 1

Consider graphs on 5 nodes. Figure 1 depicts the adjacency matrix A of such graphs, where $a\dots j$ denote Boolean variables (on the left side). For the permutation $\pi = (2,1,3,4,5)$, $\pi (A)$, is detailed on the right side of Fig. 1. A complete symmetry break can be created by using the LexLeader constraint, which requires $5! = 120$ lex constraints, one for each permutation in $S_5$.

The constraint $G \preceq \pi (G)$ is expressed as the lex constraint $abcdefghij \preceq _{lex} aefgbcdhij$, which can be simplified to $bcd\preceq _{lex} efg$.

In fact, it is sufficient to consider only some of the LexLeader constraints. In [11], a refinement procedure was used which adds non-redundant lex constraints until a complete symmetry break has been reached.

Example 2

A complete symmetry break for graph search problems on 5 nodes can be expressed in terms of the 7 permutations detailed in Fig. 2 (on the left) which give rise to the corresponding lex constraints (on the right). All of the $5!=120$ lex constraints used by the LexLeader(5) constraint are implied by these 7 lex constraints.

Fig. 2.

A complete symmetry break for graphs with 5 nodes expressed in terms of 7 lex constraints derived from corresponding permutations.

It is well known that lex constraints can be decomposed into lex implications. Using Tseytin variables $T_{x=y} \leftrightarrow x=y$ and replacing $a \le b$ by $(\lnot a \vee b)$, these are Horn clauses. The question we ask in this paper is: How many lex implications are required to represent a complete symmetry break on graphs?

Example 3

In order to break all symmetries on graphs with 5 nodes, it is sufficient to consider the 14 lex implications depicted in Fig. 3. As the Tseytin variables only occur on the left-hand side of the implications, it is sufficient to encode them using two clauses as in $(x \wedge y) \Rightarrow T_{x=y}$ and $(\lnot x \wedge \lnot y) \Rightarrow T_{x=y}$ [20]. Thus, this symmetry break can be encoded using 40 clauses.

Fig. 3.

A complete symmetry break for graphs with 5 nodes expressed in terms of 14 lex implications. These clauses were computed directly, they are not derived from the lex constraints presented in Fig. 2.

In some cases, the redundancy of lex implications can be seen directly. The lex constraint $abcefgi \preceq _{lex} ijghebc$ from Example 2 implies $a\le i$, which is redundant with respect to the lex implications from Fig. 3: If $a=1$, this implies $b = c = d = f=1$ by the inequalities on the left-hand side. This again implies $h=1$ by the lex implication $(T_{a=b}) \Rightarrow f \le h$, and $i=1$ by $(T_{a=h}) \Rightarrow c \le i$. Checking the redundancy of other lex implications often requires a case analysis.

In this paper we consider several partial symmetry breaks for graphs and for matrix models which can be defined in terms of specific sets of permutations. We denote by $S_n^{adj}$ and by $S_n^{pair}$ the sets of permutations on $\{1,\ldots ,n\}$ which swap a single adjacent pair $(i,i+1)$ for $1\le i<n$ and respectively a single pair (i, j) for $1\le i<j\le n$.

The partial symmetry breaks $\textsf {sb}_\ell$ and $\textsf {sb}^*_\ell$ presented in [6] for graphs are defined as follows where A is an $n\times n$ adjacency matrix of Boolean variables:

$$\begin{aligned} \textsf {sb}_{\ell }(A) = \bigwedge _{\pi \in S_n^{adj}} (A\le \pi (A)) \quad \text {and} \quad \textsf {sb}^*_{\ell }(A) = \bigwedge _{\pi \in S_n^{pair}} (A\le \pi (A)) \end{aligned}$$

Thus, they can be encoded using $\mathcal {O}(n)$ and $\mathcal {O}(n^2)$ lex constraints, respectively.

Definition 3 (ordering matrices)

Let $M_1,M_2$ be a pair of $m\times n$ matrices of Boolean variables and let $s_1, s_2$ be the strings obtained by concatenating their rows respectively. Then, $M_1 \preceq M_2$ if and only if $s_1\preceq _{lex} s_2$.

For a $m\times n$ matrix M of Boolean variables and permutations $\pi _1\in S_m$, $\pi _2\in S_n$, let $\pi ^{rows}_1(M)$ denote the matrix obtained by permuting the rows of M by $\pi _1$ and let $\pi ^{cols}_2(M)$ denote the matrix obtained by permuting the columns of M by $\pi _2$. The doubleLex symmetry break, also denoted lex$^2$ [7] is defined by

$$lex^2(M) = \bigwedge \left( \left\{ ~ (M\le \pi ^{rows}(M)) \left| \begin{array}{l}\pi \in S_m^{adj}\end{array} \right. \right\} \bigcup \left\{ ~ (M\le \pi ^{cols}(M)) \left| \begin{array}{l}\pi \in S_n^{adj}\end{array} \right. \right\} \right) $$

It enforces rows and columns to be sorted lexicographically and it can be encoded using $\mathcal {O} (n+m)$ lex constraints. We also consider extensions of lex$^2$, denoted lex$^+$ and lex$^*$.

$$lex^+(M) = lex^2(M) \wedge \bigwedge \left\{ ~ (M\le \pi _1^{rows}\pi _2^{cols}(M)) \left| \begin{array}{l}\pi _1\in S_m^{adj},\pi _2\in S_n^{adj}\end{array} \right. \right\} $$

$$lex^*(M) = lex^2(M) \wedge \bigwedge \left\{ ~ (M\le \pi _1^{rows}\pi _2^{cols}(M)) \left| \begin{array}{l}\pi _1\in S_m^{pair},\pi _2\in S_n^{pair}\end{array} \right. \right\} $$

Encoding these symmetry breaks requires $\mathcal {O}(nm)$ and $\mathcal {O}(n^2m^2)$ lex constraints, respectively.

In [8], the authors suggest combining lex$^2$ with additional constraints which enforce that the first row is lexicographically smaller than every permutation of every other row, and call this symmetry break allPerm. It can be implemented to run in linear time, however, encoding it statically into a SAT formula requires $\mathcal {O}(n!m)$ lex constraints. As we will show in Sect. 3, most of these constraints are actually redundant.

Table 1 illustrates the relative power of several symmetry breaks for Boolean matrix models. We consider matrices of size $n\times n$ and report the number of solutions for each of the symmetry breaks. The smaller the solution, the more precise the symmetry break. The symmetry breaks are detailed from weakest (left) to strongest (right). The left column, titled “None” has the most solutions and corresponds to imposing no symmetry break. The right column, titled “Complete” has the least solutions and corresponds to imposing a complete symmetry break. This column is obtained as OEIS sequence A002724 [21]. We observe that allPerm is only slightly stronger than lex$^2$ and weaker than lex$^+$. This is surprising, as lex$^+$ is polynomial in size whilst allPerm is exponential.

Table 1. The number of solutions for Boolean matrix models with various symmetry breaks.

3 Removing Redundant Constraints

In [11], the authors generated complete symmetry breaks for graph problems. They aimed for a small set of permutations which is canonizing, i.e. lex constraints derived from them create a complete symmetry break. They found that while generating such sets, some of the lex constraints became redundant and could be removed. Thus, after generating a complete symmetry break, they removed as many lex constraints as possible, and derived a set of non-redundant lex constraints. They furthermore noted that the set of permutations required for a complete symmetry break for graph problems on n nodes has significantly less than n! elements.

Here, we consider the set of lex implications derived from a set of lex constraints rather than the lex constraints themselves. We show that even if the set of lex constraints is non-reducible, many of the lex implications are redundant and can be removed. The approach of removing redundant lex implications applies both to complete and partial symmetry breaks.

Table 2 shows the size of different symmetry breaks for graphs, both in terms of lex implications, and in terms of the number of clauses (in parentheses). This includes clauses required for encoding the Tseytin variables. For each symmetry break, the table details the impact of removing redundant lex implications. The columns titled “orig” denote the size of the symmetry breaks before reduction (obtained by decomposing the lex constraints), and the columns titled “red” denote the size of the symmetry breaks after removing redundant lex implications.

The constraints $\textsf {sb}_{\ell }$ and $\textsf {sb}^*_{\ell }$ are partial symmetry breaks introduced in [6]. Interestingly, $\textsf {sb}_{\ell }$ does not contain any redundant lex implications, whereas roughly $65\%$ of the lex implications of $\textsf {sb}^*_{\ell }$ are redundant. For the right-most column, we took canonizing sets from [11], translated them into lex implications, and removed redundant clauses. Although the set of lex constraints does not contain any redundant constraints, more than $90\%$ of the lex implications could be removed for $n=10$ nodes. Furthermore, it is noteworthy that on small graphs, there are more clauses for the Tseytin encoding than for the symmetry break. For larger graphs, most of the clauses are lex implications.

Table 2. Number of lex implications and clauses (in parentheses), before and after the reduction, for partial symmetry breaks $\textsf {sb}_{\ell }$, $\textsf {sb}^*_{\ell }$ (on graphs) and for a complete symmetry break (for graphs) based on canonizing sets.

Table 3 illustrates the reduction in size of symmetry breaks for Boolean matrix models of size $n\times n$. Here we focus on the number of lex implications in the symmetry break (before and after reduce). In the table we consider the symmetry breaks $lex^2$, lex$^+$, lex$^*$ and allPerm which are described in Sect. 2.

Table 3. Number of lex implications for different symmetry breaks for matrix models before and after reduction.

We observe that DoubleLex ($lex^2$) does not contain any redundant implications. On the contrary, more than half of the lex implications from lex$^+$ are redundant and approximately $90\%$ of the lex implications in $lex^*$ are redundant. With regards to the allPerm symmetry break proposed in [8], the constraint itself is huge. We did not generate it for matrices larger than $7\times 7$ for which 99.85% of the lex implications are redundant. This huge size makes it hard to compute a reduced set of lex implications, we refrained from investing computational resources for the reduction of allPerm on matrices of size $8\times 8$ and larger.

How the Reduce Works

Basically, our algorithm iterates over the set of lex implications, and checks for each of them if they are redundant. This is done by removing them from the formula, and checking if there is a solution which would be forbidden by this clause, as shown in Algorithm 2. If this is not the case, the clause is redundant and can be removed. Contrary to other approaches like the one presented in [22], we run a full SAT search to determine if a lex implication is actually redundant or not. This allows for removing more clauses. Furthermore, the number of clauses which can actually be removed depends on the order in which clauses are checked. Some clauses are more helpful as they contribute to making other clauses redundant. Thus, we run our reduction in two phases. The first phase is shown in Algorithm 1. Here, we check if a clause c is redundant. If this is the case, we compute a subset $\psi \subseteq \varphi '$ of clauses which makes c redundant, and increase the ranking of all clauses within this set. The rationale is that removing these clauses is more likely make other clauses no longer redundant, and so increase the size of the final symmetry break.

In the second stage, we sort the clauses by ranking, so clauses which were frequently the cause of redundancy appear as late as possible. We then reduce the set of lex implications using Algorithm 2.

4 Generating Compact and Complete Symmetry Breaks for Graphs

The LexLeader constraint which is a complete symmetry break defined in terms of all permutations of a graph can be expressed as a set of lex implications. Each lex constraint $G\le _{lex}\pi (G)$, for a permutation $\pi$ is decomposed to lex implications, as described in Sect. 2. Each implication is classified by two parameters: the length of the implication and the permutation from which the originating lex constraint was generated. The length of an implication is the number of atoms it contains which is between 1 and $n \atopwithdelims ()2$ (the size of the upper triangle of the adjacency matrix). Formally, let A be an $n \times n$ matrix, $\pi \in S_{n}$ a permutation, and $1 \le k \le {n \atopwithdelims ()2}$ an implication length. Let $x_1,\ldots ,x_{n \atopwithdelims ()2}$ and $y_1,\ldots ,y_{n \atopwithdelims ()2}$ be the upper triangle elements (row by row) of A and $\pi (A)$, respectively. The length k lex implication $Imp _{A}(k,\pi )$ is defined by

$$ Imp _{A}(k,\pi ) = (x_1=y_1) \wedge \cdots \wedge (x_{k-1}=y_{k-1}) \Rightarrow x_k\le y_k$$

Using this notation the classic LexLeader constraint for an $n\times n$ adjacency matrix A is equivalent to the following lex implication representation:

$$ LexLeader _{A}(n) = \bigwedge _{\pi \in S_n} \bigwedge _{k=1}^{n \atopwithdelims ()2} Imp _{A}(k, \pi )$$

In this work we generate a complete symmetry breaking constraint that is equivalent to LexLeader by repeatedly selecting lex implications from the definition of $LexLeader _{A}(n)$ which are not logically implied by those already selected. When no further lex implications can be selected we have found a complete symmetry break. Although we repeatedly select non-redundant lex implications, it is possible, because of the order of selection, that some of the implications in the set become redundant. For this we reason we perform a second pass to repeatedly remove redundant implications. This process is formalized as Algorithm 3 where we select implications according to their length, first the short ones, and then the longer ones. To derive a complete symmetry break for graphs with n vertices, for each $1\le k\le {n \atopwithdelims ()2}$ the algorithm repeatedly finds implications of the form $Imp _{A}(k,\pi )$ until the set obtained so far implies every implication of length k. To find a new implication of length k we check if there exists a permutation $\pi \in S_n$ and an $n\times n$ adjacency matrix A of Boolean variables such that C is satisfied, but there exists a lex implication $Imp _{A}(k, \pi )$ which is not satisfied where C denotes the conjunction of the implications selected so far. This process continues iterating for implications of all lengths, starting from short implications, $k=1$, and finishing with the longest implications, $k= {n\atopwithdelims ()2}$. In the algorithm we apply a reduce step to remove redundant implications after each increment of the value k.

Table 4 details the computation of compact complete symmetry breaks following Algorithm 3 (lex implications) and provides a comparison with those computed in [11] (canonizing), and the symmetry breaks from [12] (isolators). For each value of n (number of vertices) we detail the size of the symmetry break derived and the time it took to compute it. For the symmetry breaks of [11], size is reported in the number of lex constraints (“lex”) and also in the number of clauses in their encoding to CNF. For the symmetry breaks derived in this paper, size is reported in the number of lex implications (“imp”) and also in the number of clauses in their encoding to CNF. Isolators are, by definition, sets of clauses. The times in the right column (Isolator) of the table are reported from [12]. These were obtained, for different values of n, using different techniques. Thus, the computation for 8 nodes is faster than the one for 7 nodes. For 7 nodes, Heule reports in [12], a computation involving 80,000 probes per round with 4 rounds at 7 min (average) per probe. This totals 1555 days of computation. The items denoted − indicate that the corresponding symmetry breaks cannot be computed. The only technique able to compute a symmetry break for graphs with 11 vertices is the technique presented in this paper. We note that this is the first time that a compact and complete symmetry break for graphs of size 11 has been computed.

Table 4. Computing compact and complete symmetry breaking constraints for graphs (time is in seconds except where indicated otherwise).

Table 5 demonstrates the impact of having more compact complete symmetry breaks. We detail the time to compute all graphs that satisfy each form of the complete symmetry break. Because the symmetry breaks are all complete, this number corresponds exactly to the number of non-isomorphic undirected graphs with n vertices (OEIS sequence number A000088) [21] which is detailed in the right column. We see from the table that enumerating graphs with more compact symmetry breaks significantly reduces the computation time.

Table 5. Enumerating graphs using complete symmetry breaking methods: canonizing, lex-implications, and isolators (using Clasp where time in seconds unless indicated otherwise).

5 An Application: Computing Ramsey Colorings (4, 4; n)

In this section we describe the impact of using compact and complete symmetry breaks. We consider a classic example of a graph search problem: the search for Ramsey graphs [23]. The graph R(s, t; n) is a simple graph with n vertices, no clique of size s, and no independent set of size t. The Ramsey number R(s, t) is the smallest number n for which there is no R(s, t; n) graph. Table 6 reports on the search for all solutions for R(4, 4, n). For $n>17$ there are no solutions and hence the Ramsey number $R(4,4)=18$. The table compares three configurations: First, using the partial symmetry breaking predicate $\textsf {sb}^*_\ell$ defined in [6]. Second, using the complete canonizing symmetry breaks computed in [11]. Third, using the complete symmetry breaks computed in this paper. For each configuration we detail the size of the SAT encoding (clauses and variables), the time in seconds (except where indicated in hours) to find all solutions using a SAT solver, and the number of solutions found. The symmetry breaks based on canonizing permutations and on lex implications are both complete, so they both compute the exact number of solutions. In the upper part of the table, we use the corresponding complete symmetry breaks described in [11] (for $n\le 10$) and in Sect. 4 of this paper (for $n\le 11$). These symmetry breaks are “instance independent”. They apply to break symmetries for any graph search problem. For $12\le n\le 17$ we compute “instance dependent” symmetry breaks. We refine Algorithm 3 to compute lex implications that break symmetries for the specific application to R(4, 4, n). This is, we restrict Algorithm 3 to consider only R(4, 4, n) graphs instead of all graphs in $\mathcal {G}_n$.

Table 6. Enumerating Ramsey graphs using $\textsf {sb}^*_{\ell }$, canonizing sets and lex implications. (Clasp solver, computation time in seconds).

The lower part of Table 6 reports on the search for all solutions of R(4, 4, n) for $n\ge 12$ using these complete symmetry breaks. The items denoted − indicate that the corresponding symmetry breaks cannot be computed within the timeout period (72 h).

It can be seen that for $12 \le n \le 15$, in which the number of non-isomorphic solutions is large, these problem dependent symmetry breaks significantly improve the solving time over the partial symmetry break $\textsf {sb}^*_{\ell }$. For $n=16$, the symmetry break computed here is significantly stronger than $\textsf {sb}^*_{\ell }$, allowing for only 2 instead of 94 solutions.

Using the lex-implications approach we were able to compute instance dependent symmetry breaks for all R(4, 4, n) instances whereas the computation of canonizing sets exceeded the timeout for three cases.

6 Conclusion

We provided an analysis of the redundancy in symmetry breaking constraints for graphs and matrix models. Previous work had shown that many of the lex constraints in the LexLeader symmetry break are redundant. Here, we considered the decomposition of lex constraints in lex implications, and showed that many of them are redundant in complete symmetry breaks. This allowed us to reduce the size of complete symmetry breaks for graphs by an order of magnitude, and enabled us to compute a complete and compact symmetry break for graphs on 11 nodes.

Furthermore, we analyzed partial symmetry breaks and the redundancies in them. While small symmetry breaks like $\textsf {sb}_\ell$ for graphs, and lex$^2$ for matrices do not contain any redundant lex implications, there are significant redundancies in their extensions $\textsf {sb}^*_{\ell }$ and lex$^+$, lex$^*$, respectively.