Towards Learned Clauses Database Reduction
Strategies Based on Dominance Relationship

arXiv:1705.10898v1 [cs.AI] 31 May 2017

Jerry Lonlac1,2 and Engelbert Mephu Nguifo1
1

Clermont Auvergne University, CNRS, LIMOS, F-63000 Clermont-Ferrand, France
2
Clermont Auvergne University, CNRS, GEOLAB, F-63000 Clermont-Ferrand
{jerry.lonlac konlac, engelbert.mephu nguifo}@uca.fr

Abstract. Clause Learning is one of the most important components
of a conflict driven clause learning (CDCL) SAT solver that is effective
on industrial instances. Since the number of learned clauses is proved
to be exponential in the worse case, it is necessary to identify the most
relevant clauses to maintain and delete the irrelevant ones. As reported
in the literature, several learned clauses deletion strategies have been
proposed. However the diversity in both the number of clauses to be
removed at each step of reduction and the results obtained with each
strategy creates confusion to determine which criterion is better. Thus,
the problem to select which learned clauses are to be removed during the
search step remains very challenging. In this paper, we propose a novel
approach to identify the most relevant learned clauses without favoring
or excluding any of the proposed measures, but by adopting the notion of
dominance relationship among those measures. Our approach bypasses
the problem of the diversity of results and reaches a compromise between
the assessments of these measures. Furthermore, the proposed approach
also avoids another non-trivial problem which is the amount of clauses
to be deleted at each reduction of the learned clause database.

1

Introduction

The SAT problem, i.e., the problem of checking whether a Boolean formula in
conjunctive normal form (CNF) is satisfiable or not, is central to many domains
in computer science and artificial intelligence including constraint satisfaction
problems (CSP), automated planning, non-monotonic reasoning, VLSI correctness checking, etc. Today, SAT has gained a considerable audience with the
advent of a new generation of solvers able to solve large instances encoding
real-world problems. These solvers, often called modern SAT solvers [17, 11] or
CDCL (Conflict Driven Clause Learning) SAT solvers have been shown to be
very efficient at solving real-world SAT instances. They are built by integrating
four major components to the classical (DPLL) procedure [9]: lazy data structures [17], activity-based variable selection heuristics (VSIDS-like) [17], restart
policies [13], and clause learning [20, 17]. Although a nice combination of these
components contributes to improve the efficiency of modern SAT solvers [16],
clause learning is known as the most important component [18]. The global idea

of clause learning is that during the unit propagation process, when a current
branch of the search tree leads to a conflict, moderns SAT solvers learn a conflict
clause that helps unit propagation to discover one of the implications missed at
an earlier level. This conflict clause expresses the causes of the conflict and is
used to prune the search space. Clause learning, also known in the literature as
Conflict Driven Clause Learning (CDCL), refers now to the most known and
used First (UIP) learning scheme, first integrated in the SAT solver Grasp [19]
and efficiently implemented in zChaff [17]. Most of the SAT solvers integrate this
strong learning scheme. Since at each conflict, CDCL solvers learn a new clause
that is added to the learned clauses database, and the number of learned clauses
is proved to be exponential in the worse case, it is necessary to remove some
learned clauses to maintain a database of polynomial size. Therefore, removing
too many clauses can make learning inefficient, and keeping too many clauses
also can alter the efficiency of unit propagation.
Managing the learned clauses database was the subject of several studies [17,
19, 11, 2, 3, 14]. These strategies were proposed with the objective to maintain a
learned clause database of reasonable size by eliminating clauses deemed irrelevant to the subsequent search. The general principle of these strategies is that,
at each conflict, an activity is associated to the learned clauses (static strategy). Such heuristic-based activity aims to weight each clause according to its
relevance to the search process. In the case of dynamic strategies, such clauses activities are dynamically updated. The reduction of the learned clauses database
consists in eliminating inactive or irrelevant clauses. Although all the learned
clause deletion strategies proposed in the literature are shown to be empirically
efficient, identifying the most relevant clause to maintain during the search process remains a challenging task. Our motivation in this work comes from the
observation that the use of different relevant-based deletion strategies gives different performances. Our goal is to take advantage of several relevant learned
clauses deletion strategies by seeking a compromise between them through a
dominance relationship.
In this paper, we integrate a user-preference point of view in the SAT process. To this end, we integrate into the SAT process the idea of skyline queries
[7], dominant patterns [21], undominated association rules [8] in order to learn
clauses in a threshold-free manner. Such queries have attracted considerable attention due to their importance in multi-criteria decision making. Given a set
of clauses, the skyline set contains the clauses that are not dominated by any
other clause.
Skyline processing does not require any threshold selection function, and
the formal property of domination satisfied by the skyline clauses gives to the
clauses a global interest with semantics easily understood by the user. This
skyline notion has been developed for database and data mining applications,
however it was unused for SAT purposes. In this paper, we adapt this notion to
the learned clauses management process.
The paper is organized as follows. We first present some effective relevantbased learned clauses deletion strategies used in the literature. Then, our learned

clauses deletion strategy based on the dominance relationship between different
strategies is presented in section 3. Finally, before the conclusion, experimental
results demonstrating the efficiency of our approach are presented.

2

On the learned clauses database management strategies

In this section, we present some efficient learned clauses relevance measures
exploited in the most SAT solvers of the literature.
The most popular CDCL SAT solver Minisat [11] considers as relevant the
clauses the most involved in recent conflict analysis and removes the learned
clauses whose involvement in recent conflict analysis is marginal. Another strategy called LBD for Literal Block Distance was proposed in [2]. LBD based measure is also exploited by most of the best state-of-the-art SAT solver (Glucose,
Lingeling [6] ) and whose efficiency has been proved empirically. LBD based
measure uses the number of different levels involved in a given learned clause
to quantify the quality of the learned clauses. Hence, the clauses with smaller
LBD are considered as more relevant. In [3], a new dynamic management policy
of the learned clauses database is proposed. It is based on a dynamic freezing
and activation principle of the learned clauses. At a given search state, using
a relevant selection function based on progress saving (PSM), it activates the
most promising learned clauses while freezing irrelevant ones. In [14], a new
criterion to quantify the relevance of a clause using its backtrack level called
BTL for BackTrack Level was proposed. From experiments, the authors observed that the learned clauses with small BTL values are used more often in
the unit propagation process than those with higher BTL values. More precisely,
the authors observed that the learned clauses with BTL value less than 3 are
always used much more than the remaining clauses. Starting from this observation, and motivated by the fact that a learned clause with smaller BTL contains
more literals from the top of the search tree, the authors deduce that relevant
clauses are those allowing a higher backtracking in the search tree (having small
BTL value). More recently, several other learned clauses database strategies were
proposed in [15, 1]. In [15], the authors explore a number of variations of learned
clause database reduction strategies, and the performance of the different extensions of Minisat solver integrating their strategies is evaluated on the instances
of the SAT competitions 2013/2014 and compared against other state-of-the-art
SAT solvers (Glucose, Lingeling) as well as against default Minisat. From the
performances obtained in [15], the authors have shown that size-bounded learning strategies proposed more than fifteenth years ago [19, 4, 5] is not over and
remains a good measure to predict the quality of learned clauses. They show
that adding randomization to size bounded learning is a nice way to achieve
controlled diversification, allows to favor the short clauses, while maintaining a
small fraction of large clauses necessary for deriving resolution proofs on some
SAT instances. This study opens many discussions about the learned clauses
database strategies and raises questions about the effectiveness proclaimed by
other strategies of the state-of-the-art [11, 2]. In [1], the authors use the com-

munity structure of industrial SAT instances to identify a set of highly useful
learned clauses. They show that augmenting a SAT instance with the clauses
learned by the solver during its execution does not always mean to make the
instance easy. However, the authors show that augmenting the formula with a
set of clauses based on the community structure of the formula improves the
performance of the solver in many cases. The different performances obtained
by each strategy suggests that the question on how to predict efficiently the
”best” learned clauses is still open and deserves further investigation.
On the other hand, it is important to note that the efficiency of most of these
state-of-the-art learned clauses management strategies heavily depends on the
cleaning frequency and on the amount of clauses to be deleted each time. Generally, all the CDCL SAT solvers using these strategies exactly delete half of the
learned clauses at each learned clauses database reduction step. For example, the
CDCL SAT solver Minisat [11] and Glucose [2] delete half of the learned clauses
at each cleaning. Therefore, the efficiency of this amount of learned clauses to
delete (e.g the half) at each cleaning step of the learned clauses database has not
been demonstrated theoretically, but instead experimentally. For our knowledge,
there are not many studies in the literature on how to determine the amount
of clauses to be deleted each time. This paper proposes an approach to identify the relevant learned clauses during the resolution process without favoring
any of the best reported relevant measures and which frees itself of the amount
of clauses to be removed at each time: the amount of learned clauses to delete
corresponds at each time to the number of learned clauses dominated by one
particular learned clause of the set of the current learned clauses which is called
in the following sections, the reference learned clause.

3

Detecting undominated learned Clauses

We present now our learned clauses relevant measure based on dominance relationship. We first motivate this approach with a simple example, and then
propose an algorithm allowing to identify the relevant clauses with some technical details.
3.1

Motivating example

Let us consider the following relevant strategies: LBD [2], SIZE (which consider
as relevant the clause of the short size) and the relevant measure use by minisat
[11] that we denote here CVSIDS. Suppose that we have in the learned clauses
database, the clauses c1 , c2 and c3 with:
– SIZE(c1 ) = 8, LBD(c1 ) = 3, CV SIDS(c1 ) = 1e100 ;
– SIZE(c2 ) = 6, LBD(c2 ) = 5, CV SIDS(c2 ) = 1e200 ;
– SIZE(c3 ) = 5, LBD(c3 ) = 4, CV SIDS(c3 ) = 1e300 .

The question we ask is the following: which one is relevant? In [2], the authors
consider the clause c1 which has the most smallest LBD measure as the most

relevant. In contrast, the authors of [15] and [12] prefer the clause c3 while the
preference of the authors of Minisat [11] leads to the clause c3 . Our approach
copes with the particular preference at one measure by finding a compromise
between the different relevant measures through the dominance relationship.
Hence, for the situation described above, only the clause c2 is irrelevant because
it is dominated by the clause c3 on the three given measures.
3.2

Formalization

During the search process, the CDCL SAT solvers learn a set of clauses which are
stored in the learned clauses database ∆, ∆ = {c1 , c2 , ..., cn }. At each cleaning
step, we evaluate these clauses with respect to a set M = {m1 , m2 , ..., mk } of
relevant measures. We denote m(c) the value of the measure m for the clause c,
c ∈ ∆, m ∈ M. Since the evaluation of learned clauses varies from a measure
to another one, using several measures could lead to different outputs (relevant
clauses with respect to a measure). For example, if we consider the motivating
example, c1 is the best clause with respect to the LBD measure whereas it
is not the case according to the evaluation of SIZE measure which favors c3
. This difference of evaluations is confusing for any process of learned clauses
selection. Hence, we can utilize the notion of dominance between learned clauses
to address the selection of relevant ones. Before, formulating the dominance
relationship between learned clauses, we need to define it at the level of measure
values. To do that, we define dominance value as follows:
Definition 1 (dominance value). Given a learned clauses relevant measure
m and two learned clauses c and c′ , we say that m(c) dominates m(c′ ), denoted by
m(c)  m(c′ ), iff m(c) is preferred to m(c′ ). If m(c)  m(c′ ) and m(c) 6= m(c′ )
then we say that m(c) strictly dominates m(c’), denoted m(c) ≻ m(c′ ).
Definition 2 (dominance clause). Given two learned clauses c, c′ , the dominance relationship according to the set of learned clauses relevant measures M
is defined as follows:
– c dominates c′ , denoted c  c′ , iff m(c)  m(c′ ), ∀m ∈ M.
– If c dominates c′ and ∃m ∈ M such that m(c) ≻ m(c′ ), then c stritly dominates c′ and we note c ≻ c′ .
To discover the relevant learned clauses a naive approach consists in comparing each clause with all other ones. However, the number of learned clauses
is proved to be exponential which makes pairwise comparisons costly. In the
following, we show how to overcome this problem by defining at each cleaning
step of learned clauses database, a particular learned clause denoted by τ that
we call here current reference learned clause which is an undominated clause of
∆ according to the set of learned clauses relevant measures M. At each cleaning
step, all the learned clauses dominated by τ will be considered as the irrelevant
learned clauses and thus deleted from the learned clauses database.

To define current reference learned clause, we need a new relevant measure
based on all the learned clauses relevant measures of M. We call this new measure Degree of compromise, in short DegComp defines as follows:
Definition 3 (Degree of compromise). Given a learned clause c, the degree
of compromise of c with respect to the set of learned clauses relevant measures
Pn \
m (c)
\
M is defined by DegComp(c) = i=1 i , where m
i (c) corresponds to the
|M|

normalized value of the clause c on the measure mi .
In fact, in practice, measures are heterogeneous and defined within different
scales. For example the values of the learned clauses relevant measures in [11]
are very high, in exponential order while the values of the relevant measures in
[2] are smallest ones. Hence, in order to avoid that the measures with the higher
values make marginal the measures with smallest values in the computation of
the comprise degree of a given learned clauses, it is recommended to normalize
the measures values. In our case here, we choose to normalize all the measures
in the interval [0, 1]. More precisely, each value of measure m(c) of any learned
[ within [0, 1]. The normalization of a given
clause c must be normalized into m(c)
measure m is performed depending on its domain and the statistical distribution
of its active domain. We recall that the active domain of a measure m is the set
of its possible values. It is worth mentioning, the normalization of a measure
does not modify the dominance relationship between two given values. If
we consider the learned clause c1 given in the motivating example in the section
3.1, with its three values : DegComp(c1 ) =
1
1e100

\ 1 )+LBD(c
\1 )+SIZE(c
\ 1)
CV SDIS(c
,
3

then,

3
8
+ nV ars()
+ nV ars()
3

we have, DegComp(c1 ) =
, with nV ars() the number of
variables of the Boolean formula.
After giving the necessary definitions (current reference learned clause and
Degree of compromise), the following lemma offers a swifter solution rather than
pairwise comparisons, to find relevant clauses based on dominance relationship.
Lemma 1 Let c be a learned clause having the minimal degree of compromise
with respect to the set of learned clauses relevant measures M, then c is an
undominated clause.
Proof 1 Let c be a learned clause having the minimal degree of compromise with
respect to the set of learned clauses relevant measures M, we suppose that there
exists a learned clause c′ that strictly dominates c, which means that ∀m ∈ M,
m(c′ )  m(c) and ∃m′ ∈ M, m′ (c′ ) ≻ m′ (c). Hence, we have DegComp(c′ ) <
DegComp(c). The latter inequality contradicts our hypothesis, since c has the
minimal degree of compromise with respect to M.
Property 1 Let M the set of learned clauses relevant measures, ∀c, c′ , c” three
learned clauses, if c ≻ c′ and c′ ≻ c” then c ≻ c”.
During the search process, at each cleaning step of the learned clauses database,
we first find the learned clause cM in having the minimal degree of compromise

with respect to M. Then, we delete from the learned clauses database all the
clauses dominated by cM in.
Searching for all undominated clauses during each cleaning step can be time
consuming, such that we only compute the undominated clauses with respect to
the reference learned clause during each reduction step.

3.3

Algorithm

In this section, after presenting the general scheme of a deletion strategy of
learned clauses (reduceDB(∆)) adopted by most of the reported solvers, we
propose an algorithm allowing to discover relevant learned clauses by using dominance relationship.
Algorithm 1 depicts the general scheme of a learned clause deletion strategy
(reduceDB(∆)). This algorithm first sorts the set of learned clauses according
to the defined criterion and then deletes half of the learned clauses. In fact, this
algorithm take a learned clauses database of size n and outputs a learned clauses
database of size n/2. This is different from our approach which first searches
the learned clause having the smallest degree of compromise (called reference
learned clause) and then removes all the learned clauses that it dominates. The
algorithm 2 depicts our learned clause deletion strategy. It is important to note
that the clauses whose size (number of literals) and LBD are less than or equal
to 2 are not concerned by the dominance relationship. These learned clauses are
considered as more relevant and are maintained in the learned clauses database.
Hence, the minDegComp function of our algorithm 2 looks the learned clause
of minimal degree of compromise among the learned clauses of size and LBD
greater than 3.
Algorithm 1: Deletion Strategy: reduceDB function
Input: ∆: The learned clauses database of size n
Output: ∆ The new learned clauses database of size n/2
1 sortLearntClauses() ;
/* by the defined criterion */
2 limit = n/2;
3 ind = 0;
4 while ind < limit do
5
clause = ∆[ind] ;
6
if clause.size() > 2 and clause.lbd() > 2 then
7
removeClause() ;
8
else
9
saveClause() ;
10
ind + +;
11 return ∆ ;

Algorithm 2: reduceDB-Dominance-Relationship
Input: ∆: The learned clauses database; M: a set of relevant measures
Output: ∆ The new learned clauses database
1 cMin = minDegComp(M) ;
/* cMin the clause having minimal
degree of compromise according to M */
2 ind = 0;
3 while ind < |∆| do
4
c = ∆[ind] ;
/* a learned clause */
5
if c.size() > 2 and c.lbd() > 2 and dominates(cMin, c, M) then
6
removeClause() ;
7
else
8
saveClause() ;
9
ind + +;
10 return ∆ ;
11
12
13
14
15
16
17
18

4

Function dominates(cMin: a clause, c: a clause, M)
i = 0;
while i < |M| do
m = M[i] ;
/* a relevant measure */
if m(c)  m(cM in) then
return F ALSE ;
i + +;
return T RU E ;

Experiments

For our experiments, we use three relevant measures for the dominance relationship to assess the efficiency of our approach. Notice that the user can choose to
combine different other measures. We use SIZE [12], LBD [2] and CV SIDS [11]
measures. All these measures have been proved effective in the literature [11, 2,
15]. It is possible to use more relevant measures, but it should be noted that by
adding a measure to M, the number of relevant learned clauses maintained may
decrease or increase. The decrease can be explained by the fact that a learned
clause can be dominated with respect to a set of measures M and undominated
with respect to M′ , such that M ⊂ M′ . For example, if two learned clauses
c and c′ are undominated with respect to M, there is a possibility that one of
them dominates the other by removing one measure. The increase can be explained by the fact that a learned clause can be dominated with respect to M
and undominated with respect to M′ . For example, consider a learned clause
c which dominates another learned clause c′ with respect to M, by adding a
measure m to M, such that m(c′ ) ≻ m(c), then c′ is no longer dominated by c.
We run the SAT solvers on the 300 instances taken from the last SAT-RACE
2015 and on the 300 instances taken from the last SAT competition 2016. All
the instances are preprocessed by SatElite [10] before running the SAT solver.

The experiments are made using Intel Xeon quad-core machines with 32GB of
RAM running at 2.66 Ghz. For each instance, we used a timeout of 1 hour
of CPU time for the SAT-RACE, and 10000s for the SAT Competition. We
integrate our approach in Glucose and made a comparison between the original
solver and the one enhanced with the new deletion learned clause strategy using
dominance relationship called DegComp-Glucose.
4.1

Number of solved instances and CPU time

Table 1 presents results on SAT-RACE. We use the source code of Glucose 3.0
with the measure LBD (written LBD-Glucose or Glucose in what follows). We
then replace LBD by each of the other measures : SIZE-Glucose that considers
the shortest clauses as the most relevant, CV SIDS-Glucose that maintains the
learned clauses most involved in recent conflict analysis, and finally our proposal
DegComp-Glucose. Table 1 shows the comparative experimental evaluation of
the four measures as well as M inisat 2.2. In the second column of Table 1, we give
the total number of solved instances (#Solved). We also mention, the number of
instances proven satisfiable (#SAT) and unsatisfiable (#UNSAT) in parenthesis.
The third column shows the average CPU time in seconds (total time on solved
instances divided by the number of solved instances). On the SAT-RACE 2015,
our approach DegComp-Glucose is more efficient than the others in terms of the
number of solved instances (see also Figure 1). In fact the original solver Glucose
solves 236 instances while it is enhanced with our dominance approach as 12
more instances are solved. In fact, solving such additional number of instances is
clearly significant in practical SAT solving. The CV SIDS-Glucose solver solves
4 more instances than Glucose 3.0. M inisat 2.2 is the worst solver among the
five solvers.
Solvers
#Solved (#SAT - #UNSAT) Average Time
M inisat 2.2
209 (134 - 75)
585.19 s
SIZE-Glucose
230 (131 - 99)
533.86 s
CV SIDS-Glucose
240 (140 - 100)
622.23 s
LBD-Glucose
236(136 - 100)
481.66 s
DegComp-Glucose
248 (146 - 102)
571.31 s
Table 1. Comparative evaluation on SAT-RACE-2015.

Table 2 shows 5 instances of the SAT-RACE 2015 solved by our approach
but not solved by LBD-Glucose, SIZE-Glucose, nor CV SIDS-Glucose. The
time used to solve those instances may also explain the increase of the average
running time of DegComp-Glucose. In addition we also find that there is none
instance solved by all the other solvers and not solved by our approach (as
detailed later). This shows on the one hand that the application of dominance
between different relevant measures does not degrade the performance of all the

solvers but instead takes advantage of the performance of each relevant measure,
considering the SAT-RACE dataset.
Instances
LBD SIZE CVSIDS DegComp
jgiraldezlevy.2200.9086.08.40.8
93.71 s
manthey DimacsSorterHalf 37 3 2642.88 s
14packages-2008seed.040
1713.46 s
manthey DimacsSorter 37 3
2673.39 s
jgiraldezlevy.2200.9086.08.40.2
3195.03 s
Table 2. Instances solved by DegComp-Glucose and not solved by the others on
SAT-RACE.

Figure 1 shows the cumulated time results i.e. the number of instances (xaxis) solved under a given amount of time in seconds (y-axis). This figure gives
for each technique the number of solved instances (#instances) in less than t
seconds. It confirms the efficiency of our dominance relationship approach. From
this figure, we can observe that DegComp-Glucose is generally faster than all the
other solvers, even if the average running time of LBD-Glucose is the lowest one
(see Table 1). Although DegComp-Glucose needs additionnal time to compute
the dominance relationship, the quality of the remained clauses on SAT-RACE
helps to improve the time needed to solved the instances.

4000

Minisat
Glucose
Size-Glucose
CVSIDS-Glucose
DegComp-Glucose

3500

time (seconds)

3000
2500
2000
1500
1000
500
0
50

100

150

200

250

#instances

Fig. 1. Evaluation on SAT-RACE-2015

Table 3 presents results on the instances of the SAT Competition 2016. Here
LBD-Glucose and CV SIDS-Glucose solve one more instance than DegCompGlucose which remains competitive, and solves the greatest number of satisfiable

Solvers
#Solved (#SAT - #UNSAT) Average Time
M inisat 2.2
138 (65 - 73)
1194.85 s
SIZE-Glucose
156 (67 - 89)
1396.73 s
CV SIDS-Glucose
165 (67 - 98)
1368.99 s
LBD-Glucose
165 (68 - 97)
1142.33 s
164 (69 - 95)

DegComp-Glucose

1456.34 s

Table 3. Comparative evaluation on SAT-Competition-2016.

10000

Minisat
Glucose
Size-Glucose
CVSIDS-Glucose
DegComp-Glucose

9000
8000

time (seconds)

7000
6000
5000
4000
3000
2000
1000
0
0

20

40

60

80

100

120

140

160

180

#instances

Fig. 2. Evaluation on SAT competition 2016

instances. Figure 2 presents the cumulated time results on the instances of the
SAT competition 2016. It comes out from this second dataset that LBD-Glucose
is more efficient than the others including our approach which remains competitive wrt the number of solved instances.
This outcome gives credit to the NO FREE Lunch theorem [22]. We also
think that the aggregated function may not be unique for all the datasets, such
that it is necessary to explore the efficient combination of the prefered measures.
4.2

Common solved instances

In table 4, the intersection between two relevant measures gives the number
of common instances solved by each measure. For example, LBD and SIZE
solved 219 instances in common, while 234 instances are solved by LBD and
DegComp. We can see than our approach solves the largest number of instances
in common with each of the aggregated measures. More precisely, the number
of common instances solved with another measure is lower than the number of
common instances solved with our approach.
To get more details, Table 5 gives the number of instances commonly solved
by the considered relevant measures. This table allows to see the number of

M easures LBD SIZE CVSIDS DegComp
LBD
SIZE
CVSIDS
DegComp

236
219 230
233 221

240

234
225
238
248

Table 4. Common solved Instances from SAT-RACE-2015.

common instances solved by one, two, three or four measures. For example,
there are 218 common instances solved by the four deletion strategies, while 44
instances are not solved by none of them. We can observe that 1, 1, 5, and 5 are
the number of instances solved alone by respectively LBD and CV SIDS, SIZE
and DegComp. Moreover, there is no instance solved by the three strategies
(LBD, SIZE and CV SIDS) and not solved by our approach DegComp.

M easures
LBD
¬ LBD

SIZE
¬SIZE
SIZE
¬SIZE

DegComp
¬DegComp
CVSIDS ¬CVSIDS CVSIDS ¬CVSIDS
218
1
0
0
1
1
1
1
3
3
0
5
3
5
1
44

Table 5. Detailed of common instances with SAT-RACE.

4.3

Combined measures

Table 6 gives the number of instances solved with our dominance approach wrt
the measures used in the dominance relations. From this table, we can see that
the number of instances solved by using two measures (instead of three) in the
dominance relationship is always lower than the number of instances solved (248)
by using three measures.
M easures LBD SIZE CVSIDS DegComp
LBD
SIZE
CVSIDS
DegComp

236
223 230
239 242

240
248

Table 6. Combining two measures on SAT-RACE-2015.

4.4

Percentage of deleted clauses

During our experiments, we compute at each reduction step of instance resolution, the percentage of deleted clauses i.e the number of dominated clauses
(which are the removed) over the total number of learned clauses during this
step. This allows to obtain an average percentage of deleted learned clauses per
solved instance. By taking all the solved instances of the SAT-RACE 2015, the
average of the average percentage of deleted learned clauses is equal to 0.36 with
a standard deviation of 0.16.
Figures 3 and 4 plot for each solved instance of the SAT-RACE 2015 (X-axis),
the average percentage of deleted learned clauses (red curve with left-Y-axis)
against respectively the total resolution time and the average resolution time
(green curve with right-Y-axis). For each solved instance, the average resolution
time is obtained by dividing its total resolution time by the number of reductions
made before solving the instance.
The (red) curve of the average percentages of deleted learned clauses exhibits
a high variation of the percentages of reduction from 0.11 to 0.89, with an average
value equals to 0.36 with a standard deviation of 0.16. It comes out from this
figure that the average percentage of deleted learned clauses is less than 50% on
200 instances among 248 solved instances. Our current strategy which uses only
one undominated clause at each step is satisfactory wrt the running time, even if
it can be possible to extend this stategy to a reduction with many undominated
clauses. The curve of the average percentages of deleted learned clauses also
shows 17 instances having the average percentage of deleted learned clauses
equal to 0. These 17 instances correspond to the instances solved by the solver
without having to reduce the learned clauses database.
Figure 3 shows on the one hand, the instances whose resolution times are
small but with a high average percentage of deleted learned clauses, and on the
other hand, the instances whose resolution times are high but with a low average
percentage of deleted learned clauses. The same remark is also valid with figure
4 where we use the average resolution time instead of the total resolution time.
This clearly shows that the number of deleted learned clauses at each reduction step is not the only component that impacts the resolution time. Other key
components of modern CDCL SAT solver such as the restart policies [13] and
the activity-based variable selection heuristics [17] also have an influence on the
resolution time.
It should be noted that if the solver Glucose keeps all the learned clauses (no
learned clauses deleted) throughout the resolution process, it solves only 203
instances on the SAT-RACE 2015 instances in 1 hour (33 instances less than the
original solver and 45 instances of less than the solver integrating our dominance
approach). On the instances of the 2016 SAT competition, keeping all the learned
clauses during the resolution process, the solver glucose solves only 131 in 10000
seconds (34 instances less than the original solver and 33 instances of less than
the solver integrating our approach).

average_percentage_of_deleted_clauses
resolution_time

0.8

4000
3500

0.7

3000

0.6
2500
0.5
2000
0.4
1500

time (seconds)

average_percentage_of_deleted_clauses

0.9

0.3
1000

0.2

500

0.1
0
0

50

100
150
instances

200

0
250

Fig. 3. Average percentage of deleted clauses and resolution time for each
instance.
average_percentage_of_deleted_clauses
average_resolution_time

0.8

60

50
0.7
0.6

40

0.5
30
0.4
0.3

20

average_time (seconds)

average_percentage_of_deleted_clauses

0.9

0.2
10
0.1
0
0

50

100
150
instances

200

0
250

Fig. 4. Average percentage of deleted clauses and average resolution time
for each instance.

This confirms the need to eliminate certain learned clauses (those deemed
irrelevant) during the resolution process, and otherwise the interest of the learned
clauses removal problem in CDCL SAT solvers.

5

Conclusion and Future Works

In this paper, we propose an approach that addresses the learned clauses database
management problem. We have shown that the idea of dominance relationship
between relevant measures is a nice way to take profit of each measure. This

approach is not hindered by the abundance of relevant measures which has been
the issue of several works. The proposed approach avoids another non-trivial
problem which is the amount of learned clauses to be deleted at each reduction
step of the learned clauses database. The experimental results show that exploiting the dominance relationship improves the performance of CDCL SAT solver,
at least on the SAT-RACE 2015. For the case of SAT-Competition, we still have
to find a good dominance relation. The instances categories might also be an
issue which should be explored.
To the best of our knowledge, this is the first time that dominance relationship has been used in the satisfiability domain to improve the performance of
a CDCL SAT solver. Our approach opens interesting perspectives. In fact, any
new relevant measure of learned clauses can be integrated into the dominance
relationship.

Acknowledgements
The authors would like to thank Auvergne-Rhône-Alpes region and European
Union for their financial support through the European Regional Development
Fund (ERDF). The authors would also like to thank CRIL (Lens Computer
Science Research Lab) for providing them computing server and the authors of
Glucose solver for making available the source code of their solver.

References
1. Carlos Ansótegui, Jesús Giráldez-Cru, Jordi Levy, and Laurent Simon. Using
community structure to detect relevant learnt clauses. In SAT 2015, pages 238–
254, 2015.
2. G. Audemard and L. Simon. Predicting learnt clauses quality in modern sat solvers.
In IJCAI’09, pages 399–404, 2009.
3. Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure, and Lakhdar Sais. On
freezing and reactivating learnt clauses. In SAT’2011, pages 188–200, 2011.
4. Roberto J. Bayardo and Daniel P. Miranker. A complexity analysis of spacebounded learning algorithms for the constraint satisfaction problem. In In Proceedings of the Thirteenth National Conference on Artificial Intelligence, pages
298–304, 1996.
5. Roberto J. Bayardo, Jr. and Robert C. Schrag. Using CSP look-back techniques
to solve real-world SAT instances. In AAAI, pages 203–208, 1997.
6. A. Biere. Lingeling and friends entering the sat challenge 2012. In A. Balint,
A. Belov, A. Diepold, S. Gerber, M. Jarvisalo, , and C. Sinz (editors), editors,
Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions, pages
33–34, University of Helsinki, 2012. vol. B-2012-2 of Department of Computer
Science Series of Publications B.
7. Stephan Börzsönyi, Donald Kossmann, and Konrad Stocker. The skyline operator.
In Proceedings of the 17th International Conference on Data Engineering, April 26, 2001, Heidelberg, Germany, pages 421–430, 2001.

8. Slim Bouker, Rabie Saidi, Sadok Ben Yahia, and Engelbert Mephu Nguifo. Mining
undominated association rules through interestingness measures. International
Journal on Artificial Intelligence Tools, 23(4), 2014.
9. Martin Davis, Gearge Logemann, and Donald W. Loveland. A machine program
for theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
10. Niklas Eén and Armin Biere. Effective preprocessing in sat through variable and
clause elimination. In SAT’05, pages 61–75, 2005.
11. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In SAT 2003, pages
502–518, 2003.
12. Eugene Goldberg and Yakov Novikov. Berkmin: A fast and robust sat-solver.
Discrete Applied Mathematics, 155(12):1549 – 1561, 2007.
13. Carla P. Gomes, Bart Selman, and Henry A. Kautz. Boosting combinatorial search
through randomization. In AAAI/IAAI, pages 431–437, 1998.
14. Long Guo, Saı̈d Jabbour, Jerry Lonlac, and Lakhdar Sais. Diversification by clauses
deletion strategies in portfolio parallel SAT solving. In ICTAI 2014, pages 701–708,
2014.
15. Saı̈d Jabbour, Jerry Lonlac, Lakhdar Sais, and Yakoub Salhi. Revisiting the learned
clauses database reduction strategies. CoRR, abs/1402.1956, 2014.
16. Hadi Katebi, Karem A. Sakallah, and João P. Marques Silva. Empirical study of
the anatomy of modern sat solvers. In SAT 2011, pages 343–356, 2011.
17. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad
Malik. Chaff: Engineering an efficient sat solver. In 38th Design Automation
Conference (DAC’01), pages 530–535, 2001.
18. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning sat
solvers with restarts. In (CP’09), pages 654–668, 2009.
19. João P. Marques Silva and Karem A. Sakallah. Grasp - a new search algorithm for
satisfiability. In International Conference on Computer-Aided Design (ICCAD’96),
pages 220–227, 1996.
20. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for
propositional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999.
21. Arnaud Soulet, Chedy Raı̈ssi, Marc Plantevit, and Bruno Crémilleux. Mining
dominant patterns in the sky. In ICDM 2011, pages 655–664, 2011.
22. David Wolpert and William G. Macready. No free lunch theorems for optimization.
IEEE Trans. Evolutionary Computation, 1(1):67–82, 1997.

