# Exploiting Isomorphic Subgraphs in SAT
(Long version)

Alexander Ivrii  IBM Haifa Research Lab, Israel
<EMAIL_ADDRESS>Ofer Strichman  Information System Engineering,
IE, Technion, Haifa, Israel
<EMAIL_ADDRESS>
###### Abstract

While static symmetry breaking has been explored in the SAT community for
decades, only as of 2010 research has focused on exploiting the same
discovered symmetry dynamically, during the run of the SAT solver, by learning
extra clauses. The two methods are distinct and not compatible. The former may
prune solutions, whereas the latter does not – it only prunes areas of the
search that are guaranteed not to have solutions, like standard conflict
clauses. Both approaches, however, require what we call _full symmetry_ ,
namely a propositionally-consistent mapping $\sigma$ between the literals,
such that $\sigma(\varphi)\equiv\varphi$, where here $\equiv$ means syntactic
equivalence modulo clause ordering and literal ordering within the clauses. In
this article we show that such full symmetry is not a necessary condition for
adding extra clauses: isomorphism between possibly-overlapping subgraphs of
the colored incidence graph is sufficient. While finding such subgraphs is a
computationally hard problem, there are many cases in which they can be
detected a priori by analyzing the high-level structure of the problem from
which the CNF was derived. We demonstrate this principle with several well-
known problems, including Van der Waerden numbers, bounded model checking and
Boolean Pythagorean triples.

##  I Introduction: symmetry, almost symmetry, and e-clauses

Symmetry breaking [25] is a well known technique for accelerating SAT solving,
which originated decades ago by Puget [24] for CSP, and later by Crawford et
al. [8] for CNF. Symmetry-breaking for CNF was implemented efficiently in the
tool shatter [3] and later improved in BreakID [11]. In a nutshell, it means
that new predicates, called _symmetry-breaking_ predicates, are added to the
input formula $\varphi$, without changing its satisfiability. These predicates
prune the search space and are likely to remove solutions, but without
changing the satisfiability of the formula. The construction of those
predicates is based on finding a mapping $\sigma$ between the literals of the
input formula $\varphi$, such that $\sigma(\varphi)\equiv\varphi$. Here
‘$\equiv$’ means syntactic equivalence modulo clause ordering and literal
ordering within the clauses. The mapping has to be _propositionally-
consistent_ , which means that $\forall v_{1},v_{2}\in var(\varphi).\
\sigma(v_{1})=v_{2}\Rightarrow\sigma(\bar{v}_{1})=\bar{v}_{2}$ and
$\sigma(v_{1})=\bar{v}_{2}\Rightarrow\sigma(\bar{v}_{1})=v_{2}$. If we find
such a mapping, then it means that every satisfying solution $\alpha$ to
$\varphi$ has the property that $\sigma(\alpha)$ also satisfies $\varphi$. We
can then add a constraint that prunes one of those solutions. As an example,
consider

$\varphi=\mbox{(1 -3)}\mbox{(2 -3)}\mbox{(1 2 3)}\mbox{(-1 -2)}$

and the mapping $\sigma:{1\mapsto 2,2\mapsto 1}$ (by convention, each such
mapping implies that the mapping of the negated literals is also included in
$\sigma$, e.g., $-1\mapsto-2\in\sigma$). We see that

$\sigma(\varphi)=\mbox{(2 -3)}\mbox{(1 -3)}\mbox{(2 1 3)}\mbox{(-2 -1)}\;,$

and that $\sigma(\varphi)\equiv\varphi$. Indeed if we take any solution
$\alpha$ to $\varphi$, we see that $\sigma(\alpha)$ is a solution as well. For
example, for $\alpha=(1,2,3)\mapsto(T,F,F)$ we have $\alpha\models\varphi$,
and indeed $\sigma(\alpha)\models\varphi$ as well, since
$\sigma(\alpha)=(1,2,3)\mapsto(F,T,F)$. Crawford et al. showed how to add
symmetry-breaking constraints, which we will not detail here. In this case it
may amount to adding the clause (-1 2), which indeed in this case excludes the
first solution without excluding the second one.

Symmetry-breaking tools discover such mappings by analyzing the colored
literals incidence graph111Such a graph is constructed from a CNF by
introducing a vertex for each literal and each clause, connecting opposite
literals with an edge, and connecting the literals to the clauses that they
are part of. The clauses’ nodes have one color, and the literals’ nodes have a
different color. $G$ with respect to multiple potential mappings $\Sigma$: if
for $\sigma\in\Sigma$ it holds that $\sigma(G)\equiv G$ (this is called
‘automorphism’), then $\sigma$ defines a symmetry. The isomorphism in this
case is restricted such that for every two nodes, $n_{1},n_{2}\in G$, if
$\sigma(n_{1})=n_{2}$ then $n_{1}$ and $n_{2}$ must have the same color, i.e.,
clause nodes are mapped to clause nodes and literal nodes to literal nodes.

Symmetry breaking can be effective in shortening the run time if it helps the
solver skip the inference process that is required for detecting that certain
partial solutions cannot be extended to full solutions. This is especially
relevant when there are many such un-extendable partial assignment that are
pruned by those predicates, whether the formula is satisfiable or not.
Symmetry breaking can also slow down the solver, for example when the formula
is satisfiable and it happens that the solution that is still possible after
adding those predicates is harder to find than those that were excluded.
Indeed, symmetry breaking has been shown to be effective especially in
unsatisfiable formulas, and enabled, for example, an increase in the size of
‘pigeonhole’ problems (which are unsat) that can be solved within a given time
limit [3, 19].

Another way to exploit symmetry is by adding clauses during search. Henceforth
we will call such clauses ‘e-clauses’, for ‘Extra’ clauses. This option has
mostly been researched in the CSP community, under the names _Symmetry
breaking during search - SBDS_ [4, 15, 16, 7] and _Symmetry Breaking by
Dominance Detection - SBDD_ [13]. In the SAT community this route was first
explored via the Symmetrical Learning Scheme (SLS) [5], which adds new clauses
during the search based on learned clauses and a pre-computed set of symmetry
‘generators’. SLS was later improved by Symmetry Propagation (SP) [9], which
only adds such extra clauses if they lead to further (immediate) propagations,
and several years later by Symmetric Explanation Learning (SEL) [10], which is
integrated within BCP (it takes the reason clause of the propagation as the
base for adding e-clauses). According to [10], SEL is the only one of those
that is competitive with modern static symmetry breaking. Finally, [29] has a
similar scheme in which e-clauses are only added if the learned clause has a
low LBD. In [10] those methods were jointly called _dynamic_ symmetry
_handling_ , to emphasize that unlike _static_ symmetry _breaking_ they are
based on an analysis during the search (hence ‘dynamic’), and that they do
_not break symmetry_ , as they do not remove solutions. We find this name
inadequate, however, because symmetry does not need to be ‘handled’. A more
proper name is dynamic symmetry _exploitation_ , which is the name we will use
in the rest of this article. Although static symmetry breaking and dynamic
symmetry exploitation are based on the same data – the symmetries in the
formula – they are not compatible. One cannot use dynamic symmetry
exploitation if the symmetries it relies on are broken by added predicates.

Dynamic symmetry exploitation was also studied for the case of _almost
symmetric_ formulas (also called ‘weak symmetry’) [22, 7], formalized as
follows. Let

$\varphi\equiv\varphi_{1}\cup\varphi_{2}\;,$ (1)

where here we equate formulas $\varphi,\varphi_{1},\varphi_{2}$ with sets of
clauses. Let $\sigma$ be a literal map of $\varphi$ such that

$\sigma(\varphi_{2})\equiv\varphi_{2}\;.$ (2)

This reflects a common scenario, where a few clauses – marked here by
$\varphi_{1}$ – disrupt the symmetries in the formula. The main method that
was suggested in these references is to add e-clauses based on $\varphi_{2}$.
That is, once a clause $c$ is learned from $\varphi_{2}$ alone, add
$\sigma(c)$ as well.

In this article we observe that the requirement of symmetry as used by all of
those prior works on dynamic symmetry exploitation is a sufficient, yet not a
_necessary_ condition for adding e-clauses. We will need the following
definitions for explaining this claim.

###### Definition 1 (The _refined_ colored incidence graph):

The _refined_ version of a colored incidence graph assigns separate colors to
clauses of different arity.

We will denote this graph by $G$, assuming the underlying formula is clear
from the context (it can also include learned clauses).

###### Definition 2 (The subgraph induced by a clause):

Given a clause $c$, the subgraph of $G$ that is _induced_ by $c$ is comprised
of the nodes in $G$ that correspond to $c$ and its literals, and the edges
between them.

We now overload this term so it can be used with a resolution sequence:

###### Definition 3 (The subgraph induced by a resolution sequence):

Given a resolution sequence $c_{1},\ldots,c_{n}$, its corresponding _induced_
subgraph in $G$ is comprised of the subgraphs induced by its clauses (Def. 2)
and the edges between opposite literals that were resolved in the sequence.

Now, consider such a resolution sequence $c_{1},\ldots,c_{n}$ that was used
for learning a clause $c$ ($c$ itself is not part of the sequence), and its
corresponding induced subgraph $g$. Consider also another subgraph
$g^{\prime}$ of $G$ that is color-isomorphic to $g$. It is not hard to see
that $g^{\prime}$ reflects another possible resolution sequence in the
formula, ending with a different clause, which we can add as an e-clause. This
criterion is _ad-hoc_ and does not require automorphism of the original
formula or some pre-defined part of it as in almost-symmetries. In fact, it
can be seen as an application of the SR-II inference rule suggested by
Krishnamurthy in [21] already in 1985 (there was no indication, however, how a
solver may exploit that rule in [21]). In some types of formulas, finding
e-clauses based on this reasoning is computationally cheap, and can lead to
improvements in the overall run-time of the solver. The important point is
that this technique can be applied even when there is no mapping $\sigma$ such
that $\sigma(\varphi)\equiv\varphi$, which implies that this technique can
derive e-clauses that cannot be derived by the above-mentioned symmetry
exploitation techniques.

In fact, this idea was implicitly used in the past by the second author [27]
for adding e-clauses in the case of bounded-model checking problems, and by
Say et al. for adding such clauses in the case of optimizing a planning
process with neural networks [26]. Both references reported performance gains.
In this article we give a general view that encompasses also these two
references, and show that the potential for such clauses is present in many
other types of formulas.

Let us demonstrate this idea with an example.

###### Example 1:

Let $\varphi$ be comprised of the following clauses:

(1 2 3) | (-1 -2 -3) | (2 3 4) | (-2 -3 -4)
---|---|---|---
(3 4 5) | (-3 -4 -5) | (4 5 6) | (-4 -5 -6)
(5 6 7) | (-5 -6 -7) | (1 3 5) | (-1 -3 -5)
(2 4 6) | (-2 -4 -6) | (3 5 7) | (-3 -5 -7)
(1 4 7) | (-1 -4 -7) |  |
(3)

It happens to be the Van der Waerden formula (3,3; 7). We will describe this
type of formulas later, in section III-A.

Symmetry breaking, as emitted by BreakID, discovers the two mappings below
(these are also called ‘generators’). To get to the full set of possible
mappings one needs to also consider their compositions.

$\begin{array}[]{l}\sigma_{1}:\ \mbox{[ 1 7 ] [ 2 6 ] [ 3 5 ]}\\\ \sigma_{2}:\
\mbox{[ 1 -1 ] [ 2 -2 ] [ 3 -3 ] ... [ 7 -7 ]}\end{array}$ (4)

This representation is called ‘cycle form’, and should be interpreted as
follows: in each line, every literal appears at most once; it should be
replaced with the literal that comes next in the brackets, and if it is the
last one then with the first literal in the brackets. In this example
$\sigma_{1}$ implies that simultaneously swapping literals 1 and 7, 2 and 6, 3
and 5 (and correspondingly, their negated versions, -1 and -7, etc.) results
in the same formula. Readers familiar with Van der Waerden formulas may notice
that this symmetry corresponds to a reversal of the indices, i.e., the first
variable becomes last, the second one becomes second to last, etc, and that
$\sigma_{2}$ corresponds to a swap of the colors. In such formulas, regardless
of their length, these are the only two possible symmetries.

Now suppose that we learn a new conflict clause $c=\mbox{(1 2 -5 6)}$, via the
following resolution sequence:

$\mbox{(1 2 3), (-3 -4 -5), (2 4 6)}\;.$ (5)

We can therefore add two e-clauses corresponding to the two generators:

$\sigma_{1}\mbox{(1 2 -5 6)}=\mbox{(7 6 -3 2)}\qquad\sigma_{2}\mbox{(1 2 -5
6)}=\mbox{(-1 -2 5 -6)}\;.$ (6)

However, more e-clauses can be derived based on this conflict clause. We need
to find a subgraph of $G$ that is color-isomorphic to the one representing the
sequence (5). Going back to our example, it is indeed not hard to see that (2
3 4), (-4 -5 -6), (3 5 7), all of which are clauses in $\varphi$, give us just
that – see Fig. 1. Applying the same resolution steps yields a new e-clause (2
3 -6 7), which cannot be deduced by any composition of
$\sigma_{1},\sigma_{2}$, simply because our inference is not based on the
original CNF’s symmetry, rather it is inferred dynamically from the resolution
process. ∎

\begin{picture}(3054.0,1132.0)(918.0,-842.0)\end{picture}
\begin{picture}(3054.0,1132.0)(918.0,-842.0)\end{picture}
---
Figure 1: Two isomorphic subgraphs of the same refined colored incidence graph
corresponding to (3). The literals are nodes with a separate color than the
clause nodes. All the clause nodes in this example are of the same arity,
hence they have the same color.

###### Example 2:

In the Boolean Pythagorean triples problem with 2 colors, we attempt to assign
one of two colors to each number up to a given $n\in\mathbb{N}$, such that no
Pythagorean triple (i.e., three numbers $a,b,c$ that are related by
$a^{2}+b^{2}=c^{2}$) is monochromatic. For $n=26$, the corresponding CNF is

(3 4 5) | (5 12 13 ) | (6 8 10)
---|---|---
(7 24 25) | (8 15 17 ) | (9 12 15)
(10 24 26) | (12 16 20) | (15 20 25)
(7)

together with the same clauses but with negated literals. Two generators are
emitted by BreakID for this formula, both of which simply swap the two colors.
Now, suppose that the solver resolved (3 4 -12 -13) from (3 4 5) and (-5 -12
-13). Symmetry does not help us detect that (6 8 -24 -26) is a legitimate
e-clause: a resolvent of $\mbox{(6 8 10)},\mbox{(-10 -24 -26)}$. On the other
hand we know that these two clauses are present in the formula because if
$a,b,c$ form a Pythagorean triple, then so do $\alpha\cdot a,\alpha\cdot
b,\alpha\cdot c$ for any $\alpha\in\mathbb{N}$, as long as they are within the
bound $n$. Using this high-level information, we can safely add (6 8 -24 -26).
∎

Since the subgraph isomorphism problem is NP-complete, we only focus on cases
in which it can be indirectly inferred from analyzing the high-level structure
of the original problem and controlling (or knowing) how it is encoded.
Specifically, in such problems we derive a mapping between the literals, and
adapt the solver to use this information in order to derive new e-clauses. Our
implementation of this technique shows average overall improvement in terms of
run-time.

To summarize, our contributions in this article are:

  1. 1.

We show several problem domains in which this known principle can be exploited
by the SAT solver for improving performance. So far it has only been used in
bounded model checking and in neural network verification;

  2. 2.

We show how this technique is superior to, and can be seen as an extension of,
dynamic symmetry;

  3. 3.

We show how to modify the SAT-solver in order to implement this technique, and
suggest several techniques for filtering e-clauses (i.e., decide which ones to
keep, in light of possibly having too many of them) and deletion of such
clauses;

  4. 4.

We present experimental results that show certain performance improvements
(around 50% reduction in run time) due to this technique with domains in which
it has not been used before.

Although any paper that mentions an open mathematical problem such as Van der
Warden numbers raises the expectation that it was able to solve it (i.e., find
a new Van der Waerden number), this is not a result that can be found here: we
only use it as one of several examples of problem domains in which the high-
level structure can be used for improving run-time.

We continue in the next section by describing the method in detail. In Sec.
III we will demonstrate how to apply it with several famous problems.

##  II Finding additional e-clauses

Let us recap. Symmetry over $\varphi$ is a propositionally-consistent map
$\sigma:lits(\varphi)\mapsto lits(\varphi)$ such that
$\sigma(\varphi)\equiv\varphi$. In this situation we can add symmetry-breaking
constraints, and also use dynamic symmetry exploitation by adding e-clauses,
but not both.

Almost symmetries refer to a situation where we have a formula
$\varphi\equiv\varphi_{1}\cup\varphi_{2}$ and a propositionally-consistent map
$\sigma:lits(\varphi_{2})\mapsto lits(\varphi_{2})$ such that
$\sigma(\varphi_{2})\equiv\varphi_{2}$. Here we _cannot_ add symmetry-breaking
constraints because of the $\varphi_{1}$ clauses, but we can still use dynamic
symmetry exploitation by adding e-clauses that are based on $\varphi_{2}$.

We now generalize almost symmetries as follows. Let

$\varphi\equiv\varphi_{1}\cup\varphi_{2}\cup\varphi_{3}\;,$ (8)

where $\varphi,\varphi_{1},\ldots$ are sets of clauses, possibly overlapping.
Let $\sigma:lits(\varphi_{2})\mapsto lits(\varphi_{3})$ be a literal map such
that

$\sigma(\varphi_{2})\equiv\varphi_{3}\;.$ (9)

Our central claim is:

###### Proposition 1:

Let $c$ be a conflict clause that was learned from $\varphi_{2}$’s clauses,
i.e., $\varphi_{2}\models c$. Then $\varphi$ and $\varphi\cup\sigma(c)$ have
the same solutions.

  * Proof:

Consider the resolution process by which $c$ was inferred from $\varphi_{2}$.
The same resolution process can be applied to $\sigma(\varphi_{2})$, and the
result will be $\sigma(c)$. Hence $\sigma(\varphi_{2})\models\sigma(c)$, and
because of (9) we have $\varphi_{3}\models\sigma(c)$. Therefore,
$\varphi\models\sigma(c)$ and we can add the e-clause $\sigma(c)$ to $\varphi$
without removing solutions. ∎

The following table summarizes the discussion so far.

| Symmetry | Almost symmetry | e-clauses
---|---|---|---
Formula: | $\varphi$ | $\varphi_{1}\cup\varphi_{2}$ | $\varphi_{1}\cup\varphi_{2}\cup\varphi_{3}$
Requires: | $\sigma(\varphi)\equiv\varphi$ | $\sigma(\varphi_{2})\equiv\varphi_{2}$ | $\sigma(\varphi_{2})\equiv\varphi_{3}$

For a given formula $\varphi$, the question is how to define
$\varphi_{2},\varphi_{3}$ and the corresponding mapping $\sigma$ that satisfy
(9). As we will see in the next section, for certain types of formulas it can
be done in such a way that e-clauses can be added in linear time. In fact it
can be done in multiple ways, i.e., many such mappings exist, and we can use
all of them.

##  III Examples

We will show here several example problems that received attention in the SAT
community in recent years, and in which e-clauses can be added efficiently .

###  III-A Van der Waerden numbers (2 colors)

We begin with the following definition:

###### Definition 4:

The Van der Waerden number $W(j,k)$ is the smallest integer $n$ such that
every 2-coloring of $1..n$ has a monochromatic arithmetic progression of
length $j$ of color 1, or of length $k$ of color 2.

For example, the following coloring proves that $W(3,3)>8$, since there is no
arithmetic progression of size 3 of either color:

\begin{picture}(1905.0,260.0)(709.0,119.0)\end{picture}

.

However, there is no such coloring for $n=9$, hence $W(3,3)=9$.

The following table shows the currently known Van der Waerden numbers when
$j=k$ (concisely denoted by $w(k)$ in the table). As of $k>6$ only lower-
bounds are known. Even the case of $k=6$ is far beyond the capability of
modern SAT solvers. The value 1132 was proven by relying on mathematical
argumentation in combination with a SAT solver for discharging millions of
lemmas regarding smaller numbers [20].

$k$ | $w(k)$ | $k$ | $w(k)$ | $k$ | $w(k)$
---|---|---|---|---|---
3 | 9 | 6 | 1,132 | 9 |  $>$ 41,265
4 | 35 | 7 |  $>$ 3,703 | 10 |  $>$ 103,474
5 | 178 | 8 |  $>$ 11,495 | 11 |  $>$ 193,941

There is relatively little symmetry in such formulas. An obvious one is the
symmetry between the colors, when $j=k$. Another type of symmetry is reversal
(reading the sequence from the end). Reconsidering Example 1,
$\sigma_{1},\sigma_{2}$ of (4) break these two symmetries.

Given $j,k$ and $n$, encoding the decision problem whether $W(j,k)>n$ with CNF
is simple. Define $n$ variables $x_{i}$ for $1\leq i\leq n$, indicating
whether location $i$ is assigned the color ‘1’. The constraints on the
arithmetic progression are given by

$\begin{array}[]{l}\\{(x_{i}\vee x_{i+d}\vee\cdots\vee x_{i+(j-1)d})\mid
i\in[1,n-(j-1)d],d\geq 1\\}\\\ \bigcup\\\
\\{(\bar{x}_{i}\vee\bar{x}_{i+d}\vee\cdots\vee\bar{x}_{i+(j-1)d})\mid
i\in[1,n-(k-1)d],d\geq 1\\}\;,\end{array}$ (10)

as was described, e.g., by Knuth in [19]. From here on we will use integers as
representatives of literals.

###### Example 3:

Consider the case of $j=k=3,n=10$. When a variable $i$ is assigned true, it
represents the decision to assign slot $i$ the color ‘1’, and ‘0‘ otherwise.
Then no 3 slots…

  * •

… with gap 1 are all ‘0’: (1 2 3) (2 3 4) … (8 9 10)

  * •

… with gap 2 are all ‘0’: (1 3 5) (2 4 6) … (6 8 10)

  * •

… with gap 3 are all ‘0’: (1 4 7) (2 5 8) … (4 7 10)

  * •

… with gap 4 are all ‘0’: (1 5 9) (2 6 10)

The same constraints, but with negated literals, are now added for the color
‘1’. For example, for gap 1, add (–1,–2, –3) … (-8, -9, -10), etc. ∎

The clauses as defined in (10) have what we call a _gliding symmetry_
222Mathematicians use this term for describing a pattern that repeats itself
by an operation of shifting in one dimension in space, e.g., $\spadesuit\
\spadesuit\ \spadesuit\ \spadesuit\ \ldots$. This means that the same clause
is replicated in the formula while shifting the variable index by a constant
up to some bound, for example (1 2 3) is in $\varphi$, but also (2 3 4)…(8 9
10). Similarly (-1 -2 -3) is replicated with a negative constant. For a clause
$c$, let $c^{i}_{z}$ denote the clause attained by taking $i$ steps towards
zero, and similarly let $c^{i}_{n}$ denote the clause attained by taking $i$
steps away from zero, i.e., towards $n$ or $-n$. For example $\mbox{(3 4
5)}^{1}_{z}=\mbox{(2 3 4)}$ and $\mbox{(1 2 3)}^{1}_{n}=\mbox{(2 3 4)}$. As
another example, this time focusing on the negative constraints, $\mbox{(-1 -3
-5)}^{1}_{n}=\mbox{(-3 -5 -7)}^{1}_{z}=\mbox{(-2 -4 -6)}$.

For each clause $c\in\varphi$, we save the _gliding bounds_ $[i,j]$, where
$i,j$ are the maximal integers such that $c^{i}_{z},c^{j}_{n}\in\varphi$. For
example, for the clause $c=\mbox{(2 3 4)}$ of Example 3, we save the pair [1,
6], because we can ‘glide’ by up to one step towards zero and by up to six
steps towards $n=10$ (giving us, respectively, (1 2 3) and (8 9 10)). As
another example, the pair for the clause (-4 -5 -6) is [3,4], because we can
glide by up to three steps towards zero, and by up to four steps towards
$-n=-10$. Denote by $c.z$ and $c.n$ the two bounds of a clause $c$,
corresponding to $i,j$ above, respectively.

So far we only considered the original clauses of the problem. We now consider
the question of what are the bounds for the learned clauses. Let
$c_{1},\ldots,c_{m}$ be the antecedent clauses of a new learned clause $c$. We
compute the gliding bounds of $c$ as follows:

$c.z=\min(c_{1}.z,\ldots,c_{m}.z)\qquad c.n=\min(c_{1}.n,\ldots,c_{m}.n)\;.$
(11)

The rational of (11) is that we can only glide $c$ towards zero (or away from
zero) as much as we can glide all of its antecedents towards zero (or away
from zero).

Given the gliding bounds of each clause, it is easy to use Proposition 1 for
learning new e-clauses. Using the terminology of that proposition, the
antecedents of $c$ form $\varphi_{2}$, and $\sigma$ is a mapping that applies
‘gliding’ to them. Each amount of gliding is a separate mapping $\sigma$. The
gliding bounds tell us the amount by which gliding each clause results in a
clause that is still in $\varphi$ – those new clauses are $\varphi_{3}$ in the
proposition. In other words, those bounds define the mappings that we can use
for deriving new e-clauses.

###### Example 4:

Suppose $\varphi$ includes the following clauses and respective bounds:

$\mbox{(3 6 10)}[2,0]\quad\mbox{(-7 -5 -3)}[2,2]\quad\mbox{(-7 -6 -5)}[4,2]$
(12)

from which the solver inferred via resolution the clause $c=\mbox{(-7 -5
10)}$. With (11) we compute the gliding bounds [2,0] for $c$. This means that
we have two mappings:

  * •

$\sigma_{1}$ maps each positive literal $l$ to $l-1$ and negative literal $-l$
to $-l+1$

  * •

$\sigma_{2}$ maps each positive literal $l$ to $l-2$ and negative literal $-l$
to $-l+2$,

i.e., a glide by one and two towards 0. So we add the e-clauses
$\sigma_{1}(c)=\mbox{(-6 -4 9)}$ and $\sigma_{2}(c)=\mbox{(-5 -3 8)}$. Indeed,
if we apply $\sigma_{1}$ to the clauses in (12), we get three clauses in
$\varphi$, from which we can infer $\sigma_{1}(c)$:

$\begin{array}[]{ll}\sigma_{1}\mbox{(3 6 10)}=\mbox{(2 5
9)}&\sigma_{1}\mbox{(-7 -5 -3)}=\mbox{(-6 -4 -2)}\\\ \sigma_{1}\mbox{(-7 -6
-5)}=\mbox{(-6 -5 -4)}&\end{array}$

∎

Finally, we should compute the gliding bounds of the e-clauses themselves,
because they may participate in further learning. For this, we shift the
bounds of the conflict clause by the same amount as dictated by the mapping
$\sigma$, while recalling that any step towards zero is a step away from $n$
(or $-n$ if it is a negative literal), and vice a versa.

###### Example 5:

Reconsider $c$ of Example 4. Its bounds are [2,0]. We computed $\sigma_{1}(c)$
by gliding $c$ towards zero by 1. Hence the bounds of $\sigma_{1}(c)$ are
[2$-$1,0$+$1] = [1,1]. ∎

###  III-B A sweep problem

Given natural numbers $m,n,r,k$, the ‘sweep’ problem is to decide whether
there is a {0,1} matrix $X$ of size $m\times n$ such that at least $r$ entries
are ‘1’, and none of its submatrices has a diagonal (from northwest to
southeast) with more than $k$ ‘1’ entries. Formally,

<EMAIL_ADDRESS>cm}}}sweep(X)=max_{\begin{array}[]{l}i_{1}\leq\cdots\leq i_{t}\leq m\\\
j_{1}\leq\cdots\leq j_{t}\leq
n\end{array}}\Sigma_{l=1}^{t}x_{i_{l},j_{l}}\hfil\hskip 42.67912pt\end{array}$

and we require $sweep(X)\leq k$. For example, the following matrix is a
solution for $m=4,n=3,r=6,k=2$.

${\small\left(\begin{tabular}[]{ccc}1&0&1\\\ 1&0&0\\\ 1&1&0\\\ 0&1&0\\\
\end{tabular}\right)}$

An encoding suggested by Knuth in [19] is based on variables $x_{i,j}$
indicating whether entry $i,j$ is ‘1’ for $1\leq i\leq m,1\leq j\leq n$, and
$s_{i,j}^{t}$, which is true if the sweep value of the submatrix
$[(1,1),(i,j)]$ of $X$ is at least $t$, for $i,j$ in the same range and $1\leq
t\leq\min(m,n)$.

We will not describe here the full set of constraints. We will only show that
some of them (in fact, almost all) have gliding symmetry, and hence enable
e-clauses. Recall that constraints that do not have this property fit into the
$\varphi_{1}$ part of (8), and according to Proposition 1 we can still add
e-clauses, as long as the base clause was inferred from $\varphi_{2}$.

First, let us focus on these two constraints:

$s_{i,j}^{t}\rightarrow s_{i+1,j+1}^{t}\quad\qquad s_{i,j}^{t}\wedge
x_{i+1,j+1}\rightarrow s_{i+1,j+1}^{t+1}$ (13)

for $1\leq i<m,1\leq j<n$. Writing these implications as clauses reveal the
gliding symmetry along the diagonals, e.g., for the first of those, the
clauses are $(\neg s_{1,1}^{1}\vee s_{2,2}^{1}),(\neg s_{2,2}^{1}\vee
s_{3,3}^{1}),\ldots$. Two other constraints for this problem that have a
gliding symmetry are $s_{i-1,j}^{t}\rightarrow s_{i,j}^{t}$ and
$s_{i,j-1}^{t}\rightarrow s_{i,j}^{t}$, with similar ranges of $i$ and $j$.
Finally, this problem contains a cardinality constraint, forcing at least $r$
‘1’ entries. Using a sequential counter to encode this constraint, as
suggested by Sinz in [28], gives us another set of constraints, that most of
them (specifically, all except a clause at the beginning and at the end of the
counter) also have a gliding symmetry. This means that we can add them to
$\varphi_{2}$ and therefor increase the number of e-clauses.

Like in the case of Van der Waerden formulas, here too we need to compute the
gliding bounds. The principle is the same, hence we won’t detail it here.

###  III-C The anti-bandwidth problem

Given a graph with nodes $1..n$ and a number $1\leq k\leq n$, the anti-
bandwidth problem (ABP) is to decide whether there is a mapping (‘labeling’)
of each node to a number in the range $0..n$ such that each label is used at
most once, and the smallest difference between labels of neighboring nodes is
at least $k$. This graph-labeling problem has various applications such as
scheduling and radio frequency assignment, and was also used recently in [14]
as a case study for a new type of SAT encoding, called ‘staircase encoding’.
Please see [14] for a survey of ABP-related research.

A natural way to encode this problem into SAT, is to define the set of
variables $\\{x_{i}^{j}\mid 1\leq i\leq n,1\leq j\leq n\\}$, where $x_{i}^{j}$
is true if and only if node $i$ is labeled with label $j$. There are
constraints forcing each node to be labeled with a single label, and each
label being assigned at most once. For our purpose of detecting a potential
for e-clauses beyond symmetry, we focus however on the constraint that forces
the gap between two neighboring nodes to be larger or equal to $k$. For a
given edge $(i,i^{\prime})$, the constraint is that up to one variable from
the set

$\\{x_{i}^{l+\gamma},x_{i^{\prime}}^{l+\gamma}\mid 1\leq l\leq
n-k,0\leq\gamma\leq k\\}$

can be true. For example, if $k=2,n=5$, then we have (in a ‘at most one’
constraint form)

$\begin{array}[]{lll}x_{i}^{1}+x_{i^{\prime}}^{1}+x_{i}^{2}+x_{i^{\prime}}^{2}+x_{i}^{3}+x_{i^{\prime}}^{3}&\leq&1\\\
x_{i}^{2}+x_{i^{\prime}}^{2}+x_{i}^{3}+x_{i^{\prime}}^{3}+x_{i}^{4}+x_{i^{\prime}}^{4}&\leq&1\\\
x_{i}^{3}+x_{i^{\prime}}^{3}+x_{i}^{4}+x_{i^{\prime}}^{4}+x_{i}^{5}+x_{i^{\prime}}^{5}&\leq&1\end{array}$
(14)

The gliding symmetry in (14) is apparent. One thing that is not a priori clear
is whether a solver can learn something from these clauses alone that is not
subsumed by existing clauses. This depends on the exact encoding of these at-
most-one constraints. If it reduces to adding a constraint for each pair of
variables in the constraint, forcing at least one of them to be false, then no
further learning is possible, and hence e-clauses become irrelevant.

###  III-D Bounded model checking and planning

Bounded model checking (BMC) [6] and Planning [18] are old problems that are
routinely solved with SAT solvers, and have essentially the same structure.
The former attempts to find an error in an open synchronous system (i.e., a
system that is controlled by inputs in each step) in its $k$’s step, and the
latter attempts to find a $k$-long set of steps that lead from a given initial
state to a goal state. In both cases $k$ is increased if the formula turns out
to be unsatisfiable, until it becomes satisfiable or intractable in terms of
computational resources.

Let $S$ be a set of Boolean variables that encode the state of the system, and
$S_{i},0\leq i\leq k$ be copies of those variables, representing the state
after $i$ steps, $S_{0}$ being the initial state. Let $I$ denote a predicate
over $S_{0}$ that defines the initial state, $T(S_{i},S_{i+1})$ for $0\leq
i\leq k$ be the transition relation, and $P$ the goal state (in the case of
BMC, $P$ is the negation of the property that is being checked). The SAT
encoding in both problems has the following structure:

$I(S_{0})\wedge\bigwedge_{i\in[0,k-1]}T(S_{i},S_{i+1})\wedge P(S_{k}).$ (15)

The projection of an assignment that satisfies (15) to the inputs, gives us a
trace to a bug in case of BMC, and a plan in case of a planning problem. The
regular structure of this equation can be exploited for detecting isomorphic
subgraphs. In fact, for the case of BMC, this was already done many years ago
in [27], although without the analysis via isomorphism as done here; rather it
showed a direct technique for adding clauses – here called e-clauses– based on
the structure of (15).

The regularity of the big conjunction in (15) represents a gliding symmetry,
similarly to the case of Van der Waerden numbers that we presented before.
Specifically, $T(S_{i},S_{i+1})$ is represented with clauses that are
isomorphic to those representing $T(S_{j},S_{j+1})$ for $0\leq j\leq k-1$, all
of which are in $\varphi$. Hence here we also need to keep gliding bounds for
each clause, and update them following the same principles that were described
in Sec. III-A. Here, however, the formula contains asymmetric parts, namely
$I(S_{0})$ and $P(S_{k})$. We assign them the gliding bounds [0,0], which
guarantees that whenever they are antecedents of a conflict clause, that
clause will not be used for deriving e-clauses, neither at the point that it
was learned, nor in later steps, if this clause participates in resolving new
clauses.

###  III-E Boolean Pythagorean triples

We conclude with an example that shows that e-clauses are not necessarily tied
to gliding symmetry.

Three positive integers $a,b,c$ are called a Pythagorean triple if they
satisfy $a^{2}+b^{2}=c^{2}$. The challenge is:

###### Definition 5:

For a given $n\in N$, can $1..N$ be separated into two sets, such that no set
contains a Pythagorean triple?

As an example, for $n=17$ if we choose the subset of integers that is here
marked with an underline: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17, it proves
that for $n=17$ the answer is yes.

The general question of whether there exists an $n$ for which the answer is
negative was open for many years. The celebrated result of Heule et al. [17] a
few years ago proved, with the help of a SAT solver, that the answer is
positive.

The encoding of the problem in Def. 5 with CNF is very simple: define $n$
variables, where the Boolean values in the satisfying assignment separate the
values naturally to the two requested sets. For example, the encoding for
$n=17$ is

<EMAIL_ADDRESS>cm}}ll}\mbox{(3 4 5)}&\mbox{(-3 -4
-5)}\hfil\hskip 19.91684pt&\mbox{(5 12 13)}&\mbox{(-5 -12 -13)}\\\ \mbox{(6 8
10)}&\mbox{(-6 -8 -10)}\hfil\hskip 19.91684pt&\mbox{(8 15 17)}&\mbox{(-8 -15
-17)}\\\ \mbox{(9 12 15)}&\mbox{(-9 -12 -15)}\hfil\hskip
19.91684pt\end{array}$

Denote by $\varphi_{n}$ this formula for a given $n$. In the discussion that
follows we will overload the multiplication and division signs, ’$\cdot$’ and
’$/$’ to operate on clauses and sets of clauses: the operation is simply
applied to each of the literals. For example, $2\cdot\mbox{(3 4 5)}=\mbox{(6 8
10)}$ and $\mbox{(6 8 10)}/2=\mbox{(3 4 5)}$.

We begin with two simple observations:

###### Observation 1:

Pythagorean triples are closed under multiplication:

$\forall a,b,c,i\in N.\ a^{2}+b^{2}=c^{2}\Rightarrow(a\cdot i)^{2}+(b\cdot
i)^{2}=(c\cdot i)^{2}\;.$

###### Observation 2:

Let $|_{d}$ denote ‘divisible by $d$’. When applied to a set of numbers, then
it means that all the set’s members are divisible by $d$. Then for all $n$,

$\mbox{(a b c)}\in\varphi_{n}\wedge\mbox{(a b
c)}|_{d}\Rightarrow\frac{\mbox{(a b c)}}{d}\in\varphi_{n}\;.$ (16)

The second observation is simply the other side of the first one (dividing
rather than multiplying), but it also states that the divided clause must be
in $\varphi_{n}$. For example, if $n=80$ then $\mbox{(30 72
78)}\in\varphi_{80}$, which implies that also (30 72 78)/2 = (15 36 39)
$\in\varphi_{80}$.

For each clause $c$, we define recursively

$c.gcd=\left\\{\begin{array}[]{ll}gcd(\\{l\mid l\in c\\})&$c$\mbox{ is
original}\\\ gcd(\\{c_{i}.gcd\mid c_{i}\in S\\})&$c$\mbox{ is inferred from
}\\\ &\mbox{a clause set }$S$\end{array}\right.$ (17)

where $gcd()$ is the greatest common divider function. Observe that if $c$ is
original, then $c.gcd$ is the greatest common divider of its own variables,
and otherwise of the variables in the core of original clauses that derived
it, which we will denote by $core(c)$. This recursive definition gives us an
immediate method to implement it in a SAT solver: the base case corresponds to
the original clauses, and the step to the learning that is done during
conflict analysis.

Given a conflict clause $c$, we can see that for $i\in[1,bound(n)]$
($bound(n)$ will be defined shortly), we have

$i\cdot\frac{core(c)}{c.gcd}\subseteq\varphi_{n}\;.$ (18)

This is a direct result of the two observations above: From Observation 2 we
know that $\frac{core(c)}{c.gcd}\subseteq\varphi_{n}$, and from Observation 1
we know that any multiplication of this clause is a Pythagorean triple.
Whether it is part of $\varphi_{n}$ depends on the value of $i$, which brings
us to the problem of computing $bound(n)$. To compute it, we need to know the
largest variable that participates in $core(c)$. For each clause $c$, we
define recursively

$c.maxvar=\left\\{\begin{array}[]{ll}\max(\\{l\mid l\in c\\})&$c$\mbox{ is
original}\\\ \max(\\{c_{i}.maxvar\mid c_{i}\in S\\})&$c$\mbox{ is inferred
}\\\ &\mbox{from a set }$S$\end{array}\right.$

Hence, for each clause $c$, $c.maxvar$ denotes the largest variable that
appears in $core(c)$. In (18) we considered clauses
$i\cdot\frac{core(c)}{c.gcd}$. For these clauses to be part of $\varphi_{n}$,
the following relation should hold:

$i\cdot\frac{c.maxvar}{c.gcd}\leq n\;.$

Isolating $i$ gives us the bound: $bound(n)=\frac{n\cdot c.gcd}{c.maxvar}.$
Finally, observe the implication of (18): since
$i\cdot\frac{core(c)}{c.gcd}\subseteq\varphi_{n}$, then

$\varphi_{n}\models i\cdot\frac{c}{c.gcd},\mbox{ for }i\in[1,bound(n)]\;.$
(19)

This means that $i\cdot\frac{c}{c.gcd}$ can be added safely as e-clauses to
$\varphi_{n}$, without removing solutions. In other words, using the
terminology of Sec. II, each $i\in[1,bound(n)]$ defines us a separate mapping
for a conflict clause $c$:

$\sigma_{i}(c)=i\cdot\frac{c}{c.gcd}\;.$ (20)

##  IV Implementation details

Recall that according to (8) the formula may contain a non-empty set of
clauses $\varphi_{1}$, that cannot participate in generating e-clauses. In our
implementation we mark those clauses at the beginning (such clauses are
expected to be given in a separate input file), and then also each learned
clause that one of its antecedents is marked that way. For simplicity let us
call these clauses non-symmetric and the rest symmetric.

We experimented with two methods of keeping track of this information. The
first is via activation literals and assumptions. One simply adds such a
literal to each non-symmetric clause in the input formula, and activate those
clauses by sending its negation as an assumption to the solver. These
activation literals are _pure_ and hence never disappear during resolution. As
a result, whenever they are used in order to derive a new clause, the
activation literal is part of that new clause as well. Hence, upon learning a
new conflict clause, the presence of an activation literal implies that we
cannot use it for deriving e-clauses. While this is a simple method to
implement, it has a rather significant performance penalty: each learned
clause now includes an additional literal if the non-symmetric part of the
formula is part of its premise. An alternative method that we implemented is
based on altering the solver itself to keep track of dependencies. This is a
non trivial task because logical dependency between clauses is created in many
different parts of a modern solver. In particular, our implementation is based
on Maple_LCM_Dist_ChronoBT [23] (we will abbreviate its name to chrono from
hereon), the winner of the SAT competition in 2018, which in itself is built
on top of multiple generations of optimizations that were added to it over the
years, all the way up to Minisat-2.2 [12]. In particular, dependency is
created during conflict analysis in the process of learning a new clause, but
also during clause minimization, binary-resolution minimization, learnt-clause
simplifications, var elimination and propagation at decision level 0333These
are implemented in the following functions in Chrono: analyze, LitRedundant,
binResMinimize, simplifyLearnt, eliminateVar, propagate. We maintain a single
bit in the header of each clause that determines whether it is symmetric or
not. Since Chrono, like all Minisat-based solvers, do not maintain unit
clauses, we maintain a separate list of variables that their value is
determined at level 0 based on non-symmetric clauses.

Next, we need to maintain problem-specific information that is necessary for
deriving e-clauses. For example, for Van der Waerden formulas, bounded model-
checking and planning problems – see Secs. III-A and III-D – we need to keep
for each clause its gliding bounds. For the Boolean Pythagorean triples
problem – see Sec. III-E – we maintain the greatest common divider (gcd) of
the literals in the clause and all clauses that participated in deriving it,
and the max variable in those clauses. As in the case of the symmetry bit
described above, here too we need to update this information in every location
in which dependency is created.

Our implementation accumulates e-clauses and then adds them to the clause
database at the nearest restart. This is a different strategy than the ones
mentioned in the introduction in the context of symmetric explanation learning
[10] and dynamic symmetry handling [10, 29], where such clauses are added
during BCP, hence affecting the current search branch (we implemented both,
and the results are rather similar, with a small advantage to the technique
described here). To reduce side-effects, upon adding a new e-clause we do
_not_ increase the counter of conflict clauses, since that counter affects
various other heuristics, such as the frequency of applying simplifications
and clause deletion.

The above-mentioned prior works describe various filtering methods: adding
clauses only if they conflict the current state or lead to further
propagation, or, in the case of [29], if the conflict clause itself has a low
LBD.

We will now describe the filtering and deletion strategies that we
implemented. Recall that e-clauses are added at restarts.

####  IV-1 Filtering strategies

We implemented the following filtering strategies:

  * F1

Add an e-clause only if up to $x$ literals, $x$ being a user-defined value,
are not false under the current partial assignment. When $x=0$ it means that
we only add clauses that contradict the current partial assignment, and when
$x=1$ we allow in addition clauses that are asserting under the current
partial assignment.

  * F2

Add an e-clause only if its _partial_ LBD is smaller than a user-defined
value. The LBD is ‘partial’ in the sense that the e-clause may contain
literals that are not assigned under the current partial assignment, so we do
not count them.

  * F3

Add an e-clause only ifs size is under a user-defined value.

  * F4

An explicit bound on the number of added e-clauses.

  * F5

A bound on the number of e-clauses that are being examined with respect to
F1,F2 above, to reach the bound from F4.

The combination that worked best on average in our experiments is F1 with
$x=3$, and F3 with a bound of 20.

####  IV-2 Deletion strategies

We implemented the following deletion strategies:

  * D1

A separate initial activity score for e-clauses.

  * D2

A control of the initial learnt-clause list into which the e-clauses are
inserted. Modern Minisat-based solvers add each learnt clause to one of three
such lists: ‘Local’, ‘Tier2’ and ‘Core’, based on their predicted importance.
‘Local’ is the list of the least important clauses (in Chrono this list is
populated with references to learned clauses with LBD $>6$). During periodic
clause database reductions, half of the clauses in this list are removed. If
clauses are sufficiently active or their LBD becomes smaller, they may move to
‘Tier2’ or ’Core’, which are protected from being reduced. Clauses can also
move back from ‘Tier2’ to ‘Local’ if they become less active.

  * D3

The ratio of clauses to be deleted from the ‘Local’ list. Default is 0.5.

The combination that worked best on average in our experiments is D1 with a
score of 0.8 (comparing to the weight 1 given to normal conflict clauses), D2
with the list ‘Local’, and D3 with the ratio 0.8 (we left this deletion ratio
also for the experiments without e-clauses, for a fair comparison).

##  V Results

We implemented this method for Van der Waerden numbers and Boolean Pythagorean
triples. Since there is no standard benchmark sets for these problems, we
generated instances, and took all of those that can be solved with at least
one configuration in less than 30 min., and with at least one configuration in
more than 1 min. For the Van der Waerden problems, this resulted in 30
benchmarks (16 unsat, 14 sat). The benchmarks, full tables of results, and the
implementation are available from [2]. We used the Hbench benchmarking system
[1] to conduct the experiments and data collection.

In the results tables below, timed-out benchmarks contribute the values they
had at the timeout point to the various columns, other than the par-2 column,
where the timeout is added twice, to be consistent with the ranking method of
the SAT competitions. Our goal was mostly to measure the number of e-clauses
that can be found based on isomorphic subgraphs, beyond what can be found with
dynamic symmetry exploitation. We have evidence from multiple previous works,
e.g., [10, 29, 27] (see Sec. I), that such clauses can help in reducing the
run time. Our results below show not only that indeed many more such clauses
can be generated, but also that when combined with the right filtering and
deletion methods, it reduces the run time on average.

The results for the Van der Waerden problems are summarized in Table I, sorted
by performance. The ‘-waerden’ flag indicates that e-clauses are added as
described in Sec. III-A. The ‘-dyn-sym-exploit’ flag indicates that e-clauses
based on dynamic symmetry exploitation were added. ‘native’ means that the
solver was run in its default configuration (other than D3 – see deletion
strategies in Sec. IV). ‘static-sym-breaking’ indicates that we solved the
formula with static symmetry-breaking constraints, as provided by BreakID,
while the solver is in the same configuration as ‘native’. For these
benchmarks static symmetry breaking turns out to be better than dynamic
symmetry exploitation, based on the same data (even when considering the unsat
cases on their own). When considering unsat formulas only (not shown), static
symmetry breaking is the best of all configurations.

Configuration | Timed- | Time | Time | Conflicts | e-clauses | Over- | Active | Active
---|---|---|---|---|---|---|---|---
| out |  | (par-2) |  |  | head | -E- | -C-
-waerden | 0 | 111.2 | 111.2 | 1,079,719 | 30568 | 6 | 0.017 | 0.015
-static-sym-breaking | 1 | 149.8 | 211.2 | 2110472 | 0 | 0 |  |
(native) | 1 | 190.4 | 251.7 | 2,112,666 | 0 | 0 |  | 0.011
-waerden -dyn-sym-exploit | 2 | 198.5 | 317.7 | 1,963,104 | 50618 | 10 | 0.014 | 0.008
-dyn-sym-exploit | 3 | 233.2 | 418.6 | 2,477,840 | 6,729 | 3 | 0.011 | 0.008
-waerden | 6 | 476.5 | 841.9 | 750,453 | 16,556,216 | 29 | 0.013 | 0.013
-dyn-sym-exploit | 1 | 119.8 | 181.3 | 1,248,573 | 1,290,402 | 13 | 0.008 | 0.011
TABLE I: Average results for the Van der Waerden problem, over 30 benchmarks.
Time is in seconds. The last two rows refer to runs without any filtering of
the e-clauses , which turns out to be better for dynamic symmetry
exploitation.

On average each conflict clause learned while solving these benchmarks results
in over 20 e-clauses with the -waerden flag (this clearly depends on the value
of $n$), and less than 1 with -dyn-sym-exploit. The latter is expected, since
BreakID generates a single generator for these benchmarks (see text after Def.
4). The top part of the table does not reflect these numbers, however, because
it refers to runs in which we applied aggressive filtering as mentioned
before. With these filters, the number of e-clauses added is typically less
than 5% of the total number of clauses. Hence the potential for e-clauses is
large, and perhaps future research into filtering techniques will be able to
exploit this unused potential. The overhead of generating the e-clauses is
marginal (the ‘Overhead’ column). The overhead of running BreakID, a necessary
step for applying both -dynamic-symmetry and -symmetry-breaking, was a few
seconds and not included in the ‘Time’ column.

We can see a run-time reduction of 42% comparing to a native run for the case
of Van der Waerden formulas, and of 55% for the case of Pythagorean triples.
In both cases the technique as described in III-A is better than adding
e-clauses based on data derived from static symmetry, and better than
combining these two sources of data. Cactus plots for both families appear in
Figs. 2 and 3.

We also checked how active the e-clauses are in deriving new clauses. For this
measure we define as e-clauses, recursively, the set of clauses that we add
directly and the clauses that were learned based on at least one e-clause
premise. Activity of clauses is updated in the solver in the usual way, based
on their participation in deriving other clauses. Since clause deletion is
based on this activity, the ratio between the average number of ‘live’ clauses
(i.e., that were not deleted) and the total number of learned clauses is an
indication of how active they are. This ratio for e-clauses and normal
conflict clauses appear in the last two columns of the table. It is surprising
to see that the e-clauses are more active, especially in the context of
deletion strategy D1, namely the fact that we initiate the activity score of
e-clauses with a lower value in comparison to the value given to conflict
clauses.

For the Boolean Pythagorean triples problem, we generated 21 satisfiable
instances (the first unsatisfiable instance takes weeks to solve — see [17])
with the same selection criteria as described above. The results appear in
Table II, also in ascending performance order. Here the native solver turns
out to be improved-upon in each of the configurations, including static
symmetry breaking.

$0$$5$$10$$15$$20$$25$$30$$0$$500$$1{,}000$$1{,}500$$2{,}000$Solved instancesTime-waerden-static-sym-breakingnative-waerden -dyn-sym-exploit-dyn-sym-exploit Figure 2: Results for the Van der Waerden benchmarks. $0$$5$$10$$15$$20$$0$$500$$1{,}000$$1{,}500$$2{,}000$Solved instancesTime-pythagorean-pythagorean -dyn-sym-exploit-static-sym-breaking-dyn-sym-exploit-native Figure 3: Results for the Pythagorean-triples benchmarks. Configuration | Timed- | Time | Time | Conflicts | e-clauses | Over- | Active | Active
---|---|---|---|---|---|---|---|---
| out |  | (par-2) |  |  | head | -E- | -C-
-pythagorean | 1 | 360.1 | 446.5 | 1,973,404 | 60303.3 | 0.2 | 0.006 | 0.006
-pythagorean -dyn-sym-exploit | 3 | 419.5 | 676.6 | 1,864,767 | 55264.4 | 36.0 | 0.007 | 0.006
-static-sym-breaking | 4 | 474.1 | 821.4 | 3,132,118 | 0 | 0 |  |
-dyn-sym-exploit | 3 | 579.1 | 837.4 | 2,558,436 | 388.4 | 50.5 | 0.004 | 0.007
(native) | 3 | 795.6 | 1053.7 | 3,901,308 | 0 | 0 |  | 0.007
-pythagorean | 4 | 578.0 | 1008.9 | 3,045,218.4 | 214,993.7 | 0.4 | 0.004 | 0.054
-dyn-sym-exploit | 9 | 931.7 | 1714.1 | 1,813,843.8 | 3,541,747.0 | 568.9 | 0.005 | 0.007
TABLE II: Results for the Boolean Pythagorean triples problem, over 21
benchmarks. The bottom two configurations are without filtering.

##  VI Conclusions and future work

We presented a general condition for adding what we call e-clauses, right
after conflict analysis. We showed how this technique generalizes ‘symmetry’
and ‘almost symmetry’, and that indeed this method can add far more clauses
than dynamic symmetry exploitation and related methods that are solely based
on such symmetries. We showed several known problems for which this is
relevant, and mentioned cases in which it was already done in the past with
empirical success.

There are three lines of future work that we consider important. First, it is
important to classify additional problems as having the property that they are
amenable to adding e-clauses, and check whether it can assist in accelerating
their solving. Second, we foresee a dedicated SAT solver that maintains and
reasons about _clause generators_. That is, instead of adding many e-clauses
as normal clauses, just keep the base learned clause with its bounds. It can
be faster than the alternative of adding all e-clauses and does not suffer
from the necessity to delete most of them. In a sense, this way the e-clauses
are generated lazily, on demand, and then immediately erased. There are many
implementation details that need to be developed for this. For example, one
can add the generator to the watch list of all the literals that would have
watched one of its generated e-clauses. In BCP, that literal tells us how to
apply the unit implication rule to the generator. The reason clause can be
maintained as a pair of a reference to the generator and an instantiation
index. Many other details still need to be worked out.

A third direction, is to control the BCP order, such that it works first on
‘normal’ clauses and only if it terminates without a conflict, continue to
propagate through the e-clauses, based on the assumption that the latter are
less likely to cause a conflict at the current branch. One can also envision a
SAT solver that splits BCP on normal and e-clauses between two threads. A
possible high-level architecture is one in which the main thread, $T$, works
on ‘normal’ clauses and then on e-clauses, and the other, $T_{e}$, in the
other direction. The first that finds a conflict terminates the other, or,
alternatively, the solver chooses the better conflict clause based on its LBD
and backtracking level.

## References

  * [1] Hbench.  https://strichman.net.technion.ac.il/hbench/.
  * [2] Statistics.  https://technionmail-my.sharepoint.com/:f:/g/personal/ofers_technion_ac_il/ElPLTu98GFNGidn8MHqydHYBzKLkJe1WFKS0-g8s78wV0w?e=l7Id5A.
  * [3] Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah.  Solving difficult instances of boolean satisfiability in the presence of symmetry.  IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 22(9):1117–1137, 2003.
  * [4] Rolf Backofen and Sebastian Will.  Excluding symmetries in constraint-based search.  Constraints An Int. J., 7(3-4):333–349, 2002.
  * [5] B. Benhamou, T. Nabhani, R. Ostrowski, and M. R. Saidi.  Enhancing clause learning by symmetry in sat solvers.  In 2010 22nd IEEE International Conference on Tools with Artificial Intelligence, volume 1, pages 329–335, 2010.
  * [6] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu.  Symbolic model checking without BDDs.  In Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS, pages 193–207. Springer-Verlag, 1999.
  * [7] Geoffrey Chu, Maria Garcia de la Banda, Christopher Mears, and Peter J. Stuckey.  Symmetries, almost symmetries, and lazy clause generation.  Constraints An Int. J., 19(4):434–462, 2014.
  * [8] James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks, and Amitabha Roy.  Symmetry-breaking predicates for search problems.  In Luigia Carlucci Aiello, Jon Doyle, and Stuart C. Shapiro, editors, Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96), Cambridge, Massachusetts, USA, November 5-8, 1996, pages 148–159. Morgan Kaufmann, 1996.
  * [9] J. Devriendt, B. Bogaerts, B. d. Cat, M. Denecker, and C. Mears.  Symmetry propagation: Improved dynamic symmetry breaking in sat.  In 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, volume 1, pages 49–56, 2012.
  * [10] Jo Devriendt, Bart Bogaerts, and Maurice Bruynooghe.  Symmetric explanation learning: Effective dynamic symmetry handling for SAT.  In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, Proceedings, volume 10491 of LNCS, pages 83–100. Springer, 2017.
  * [11] Jo Devriendt, Bart Bogaerts, Maurice Bruynooghe, and Marc Denecker.  Improved static symmetry breaking for SAT.  In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 104–122. Springer, 2016.
  * [12] Niklas Eén and Niklas Sörensson.  An extensible SAT-solver.  In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing (SAT), volume 2919 of LNCS, pages 502–518. Springer, 2003.
  * [13] Torsten Fahle, Stefan Schamberger, and Meinolf Sellmann.  Symmetry breaking.  In Toby Walsh, editor, Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, volume 2239 of Lecture Notes in Computer Science, pages 93–107. Springer, 2001.
  * [14] Katalin Fazekas, Markus Sinnl, Armin Biere, and Sophie N. Parragh.  Duplex encoding of staircase at-most-one constraints for the antibandwidth problem.  In Emmanuel Hebrard and Nysret Musliu, editors, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings, volume 12296 of Lecture Notes in Computer Science, pages 186–204. Springer, 2020.
  * [15] Ian P. Gent, Warwick Harvey, and Tom Kelsey.  Groups and constraints: Symmetry breaking during search.  In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 415–430. Springer, 2002.
  * [16] Ian P. Gent and Barbara M. Smith.  Symmetry breaking in constraint programming.  In Werner Horn, editor, ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence, Berlin, Germany, August 20-25, 2000, pages 599–603. IOS Press, 2000.
  * [17] Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek.  Solving and verifying the boolean pythagorean triples problem via cube-and-conquer.  In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228–245. Springer, 2016.
  * [18] H. Kautz and B. Selman.  Planning as satisfiability.  In Proc. of the $10^{th}$ European Conf. on AI, pages 359–363, 1992.
  * [19] Donald Knuth.  The Art of Computer Programming: Satisfiability, volume 4b, Fascicle 6.  2015\.
  * [20] Michal Kouril and Jerome L. Paul.  The van der waerden number _W_(2, 6) is 1132.  Exp. Math., 17(1):53–61, 2008.
  * [21] Balakrishnan Krishnamurthy.  Short proofs for tricky formulas.  Acta Informatica, 22(3):253–275, 1985.
  * [22] Roland Martin.  The challenge of exploiting weak symmetries.  In Brahim Hnich, Mats Carlsson, Fran(c)ois Fages, and Francesca Rossi, editors, Recent Advances in Constraints, Joint ERCIM/CoLogNET International Workshop on Constraint Solving and Constraint Logic Programming, CSCLP 2005, Uppsala, Sweden, June 20-22, 2005, Revised Selected and Invited Papers, volume 3978 of Lecture Notes in Computer Science, pages 149–163. Springer, 2005.
  * [23] Alexander Nadel and Vadim Ryvchin.  Chronological backtracking.  In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 111–121. Springer, 2018\.
  * [24] Jean-Francois Puget.  On the satisfiability of symmetrical constrained satisfaction problems.  In Henryk Jan Komorowski and Zbigniew W. Ras, editors, Methodologies for Intelligent Systems, 7th International Symposium, ISMIS ’93, Trondheim, Norway, June 15-18, 1993, Proceedings, volume 689 of Lecture Notes in Computer Science, pages 350–361. Springer, 1993.
  * [25] Karem Sakallah.  Symmetry and Satisfiability, chapter 10, pages 289–338.  IOS press, 2009.
  * [26] Buser Say, Jo Devriendt, Jakob Nordström, and Peter J. Stuckey.  Theoretical and experimental results for planning with learned binarized neural network transition models.  In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 917–934. Springer, 2020.
  * [27] Ofer Shtrichman.  Tuning SAT checkers for bounded model checking.  In E.A. Emerson and A.P. Sistla, editors, Proc. $12^{th}$ Intl. Conference on Computer Aided Verification (CAV’00), LNCS. Springer-Verlag, 2000.
  * [28] Ofer Strichman.  Lecture notes: Decision procedures for fragments of first-order logic.  (unpublished), 2005.
  * [29] Rodrigue Konan Tchinda and Clémentin Tayou Djamégni.  Enhancing static symmetry breaking with dynamic symmetry handling in CDCL SAT solvers.  Int. J. Artif. Intell. Tools, 28(3):1950011:1–1950011:32, 2019\.