Jerry Lonlac
email: jerry.lonlac_konlac@uca.fr

Engelbert Mephu Nguifo

On the power of top-k undominated learnt clauses for Modern SAT Solvers

Keywords: Satisfiability, Clause Learning, CDCL SAT Solver, Dominance Relationship

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 increase the difficulty 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 results diversity and reaches a compromise between the measures assessments. Furthermore, the proposed approach also avoids another non-trivial problem which is the number of deleted clauses at each reduction of the learned clause database.

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 generation of solvers able to solve large instances encoding real-world problems. These solvers, often called modern SAT solvers [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF][START_REF] Eén | An extensible sat-solver[END_REF] 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 into the classical Davis, Putnam, Logemann and Loveland procedure, commonly called DPLL [START_REF] Davis | A machine program for theoremproving[END_REF]: lazy data structures [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF], activity-based variable selection heuristics (VSIDS-like) [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF], restart policies [START_REF] Gomes | Boosting combinatorial search through randomization[END_REF], and clause learning [START_REF] Silva | GRASP: A search algorithm for propositional satisfiability[END_REF][START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF]. Although a nice combination of these components contributes to improve the efficiency of modern SAT solvers [START_REF] Katebi | Empirical study of the anatomy of modern sat solvers[END_REF], clause learning is known as the most important component [START_REF] Pipatsrisawat | On the power of clause-learning sat solvers with restarts[END_REF].

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 [START_REF] Silva | Grasp -a new search algorithm for satisfiability[END_REF] and efficiently implemented in zChaff [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF]. 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 reasonable 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 [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF][START_REF] Silva | Grasp -a new search algorithm for satisfiability[END_REF][START_REF] Eén | An extensible sat-solver[END_REF][START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF][START_REF] Audemard | On freezing and reactivating learnt clauses[END_REF][START_REF] Guo | Diversification by clauses deletion strategies in portfolio parallel SAT solving[END_REF]. 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. 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.

Other works from the literature on the clause learning component have instead focused on the minimization of the learned clause. These works aim mostly at reducing the number literals from learned clauses [START_REF] Biere | Preprocessing and inprocessing techniques in SAT[END_REF][START_REF] Wotzlaw | Effectiveness of preand inprocessing for cdcl-based SAT solving[END_REF][START_REF] Sörensson | Minimizing learned clauses[END_REF][START_REF] Beame | Towards understanding and harnessing the potential of clause learning[END_REF][START_REF] Jabbour | Extending resolution by dynamic substitution of boolean functions[END_REF]. In this way, more recently, in [START_REF] Luo | An effective learnt clause minimization approach for CDCL SAT solvers[END_REF], the authors propose a new in-processing learned clause minimization approach able to remove redundant literals from learned clauses for CDCL solvers. This approach is based on Boolean constraint propagation, or more precisely unit (clause) propagation, which is time-consuming on large instances. The integration of this approach in the state-of-the art best SAT solvers allows to solve a large number of additional instances coming from the hard combinatorial and application categories of the 2014 and 2016 SAT competitions. The SAT solver Maple LCM Dist winner of the last 2017 SAT competition on the Main Track instances implements this minimization approach.

By considering the impact of clause learning on the practical resolution of SAT instances, 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 [START_REF] Börzsönyi | The skyline operator[END_REF], dominant patterns [START_REF] Soulet | Mining dominant patterns in the sky[END_REF], undominated association rules [START_REF] Bouker | Mining undominated association rules through interestingness measures[END_REF] 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.

In our previously related work [START_REF] Lonlac | Towards learned clauses database reduction strategies based on dominance relationship[END_REF], we propose to search at each reduction step of the learned clauses database, the current reference learned clause [START_REF] Lonlac | Towards learned clauses database reduction strategies based on dominance relationship[END_REF] (top-1 undominated learned clauses in this paper) according to a set of relevant measures and to delete all the learned clauses dominated by this clause. In this paper, we extend this idea by considering instead k current reference learned clause i.e the top-k undominated learned clauses at each cleaning step and delete all the learned clauses dominated by at least one of the top-k undominated learned clauses.

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 4. Finally, before the conclusion, experimental results demonstrating the efficiency of our approach are presented.

Around SAT Problem

Let L be a propositional language of formulas F L built in the standard way, using usual logical connectives ¬, ∨, ∧, →, ⇒, ⇔, and a set of propositional variables. Using linear Tseitin encoding [START_REF] Tseitin | On the complexity of derivations in the propositional calculus[END_REF], any Boolean formula f ∈ F L can be translated to CN F (f ), a formula in conjunctive normal form. A CNF formula is a conjunction (∧) of clauses, where a clause is a disjunction (∨) of literals.

A literal is a propositional variable (l) or a negated propositional variable (¬l).

The literals l and ¬l are called complementary literals. A unit clause is a clause containing only one literal (called unit literal). An empty clause, noted ⊥, is interpreted as false (unsatisfiable), whereas an empty CNF formula, noted , is interpreted as true (satisfiable). A CNF formula Φ can also be seen as a set of clauses, and a clause as a set of literals. The size of the formula Φ corresponds to the value c∈Φ |c| where |c| is the number of literals in the clause c. An assignment I of is a function which associates a value I(x) ∈ {f alse, true} to some of the variables of Φ. I is complete if it assigns a value to every variable of Φ, and partial otherwise. A model of a formula is an assignment that makes the formula true. The SAT problem consists in determining if a Boolean formula expressed in CNF admits a model or not.

SAT is the NP-complete decision problem for which the largest amount of research effort has been expended for the development of sophisticated algorithms with highly-optimized implementations. Most of the SAT algorithms are highly complex and empirical studies allows to assess and compare their performance.

An SAT competition organized each year allows both an objective assessment of these SAT algorithms and a promotion of new SAT solvers. However, one solver can be better than others at solving some SAT instances from a given class, but dramatically worse on other instances. There is no solver effective on all SAT instances class, different solvers perform best on different instances. Thus, from this observation, rather than following the traditional approach of choosing the best solver for a given class of instances, some works on SAT build the portfolios algorithm [START_REF] Gomes | Algorithm portfolios[END_REF][START_REF] Kadioglu | ISAC -instance-specific algorithm configuration[END_REF][START_REF] Malitsky | Non-model-based algorithm portfolios for SAT[END_REF][START_REF] Nikolic | Simple algorithm portfolio for SAT[END_REF][START_REF] Leyton-Brown | A portfolio approach to algorithm selection[END_REF][START_REF] Xu | Satzilla: Portfolio-based algorithm selection for SAT[END_REF][START_REF] Xu | The design and analysis of an algorithm portfolio for SAT[END_REF] that selects solvers on a per-instance basis using empirical hardness models for runtime prediction [START_REF] Hutter | Algorithm runtime prediction: Methods & evaluation[END_REF].

These empirical hardness models are usually built using machine learning techniques. A predictor of an algorithm's runtime on a given problem instance use the set of features of the instance and the algorithms past performance [START_REF] Leyton-Brown | Learning the empirical hardness of optimization problems: The case of combinatorial auctions[END_REF][START_REF] Nudelman | Understanding random SAT: beyond the clauses-to-variables ratio[END_REF].

In order to do this, instances are grouped into classes based on their features, and the best algorithm is calculated for each class. Thereafter, given an input instance, its features are computed and it is assigned to a class (using the prediction model previously built), and it is solved by the corresponding solver assigned to that class. In recent years, there have been some works to better characterize the SAT instances in order to effectively classify them [START_REF] Ansótegui | The community structure of SAT formulas[END_REF][START_REF] Newsham | Impact of community structure on SAT solver performance[END_REF]. In fact, the set of features used to build the classifiers of SAT instances plays a crucial role. In [START_REF] Ansótegui | Structure features for SAT instances classification[END_REF], the authors use some structure features of industrial SAT instances to build some classifiers of industrial SAT families of instances. The effectiveness of these classifiers is measured by comparing them to other sets of SAT features commonly used in portfolio SAT solving approaches. In [START_REF] Giráldez-Cru | A modularity-based random SAT instances generator[END_REF], it is proved that the ratio between the run-times needed by a CDCL solver and by a random-specialized solver is related to the scale-free structure of the boolean formula.

The international SAT competition series stimulate the development of efficient implementations leading to increasingly complex solvers with several number of parameters. These parameters allow solvers to be customized to a particular family of SAT instances. However, in the SAT competitions, solvers are run using a single default parameter setting supplied by the authors for all benchmark instances in a given track, this poses a problem for a practical use of SAT who only cares about performance on one particular application and can invest some time into tuning solver parameters for this application. So, a new Configurable SAT solver Competition (CSSC) [START_REF] Hutter | The configurable SAT solver challenge (CSSC)[END_REF] has been designed in order to evaluate solver performance for each SAT instance after having configured its parameters. The CSSC takes into account the fact that effective algorithm configuration procedures can automatically customize solvers for a given distribution of benchmark instances. More precisely, for each type of SAT instances and each SAT solver, an automated fixed-time offline configuration phase determines parameter settings of solver optimized for high performance on this type of SAT instances. Then, the performance of solver on the type of instance is evaluated with these settings, and the solver with the best performance wins.

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 [START_REF] Eén | An extensible sat-solver[END_REF] 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 [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF]. LBD based measure is also exploited by most of the best state-of-the-art SAT solvers (Glucose, Lingeling [START_REF] Biere | Lingeling and friends entering the sat challenge[END_REF] ) 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 [START_REF] Audemard | On freezing and reactivating learnt clauses[END_REF], 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 [START_REF] Guo | Diversification by clauses deletion strategies in portfolio parallel SAT solving[END_REF], 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 [START_REF] Jabbour | Revisiting the learned clauses database reduction strategies[END_REF][START_REF] Ansótegui | Using community structure to detect relevant learnt clauses[END_REF]. In [START_REF] Jabbour | Revisiting the learned clauses database reduction strategies[END_REF], 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 [START_REF] Jabbour | Revisiting the learned clauses database reduction strategies[END_REF], the authors have shown that size-bounded learning strategies proposed more than fifteenth years ago [START_REF] Silva | Grasp -a new search algorithm for satisfiability[END_REF][START_REF] Bayardo | A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem[END_REF][START_REF] Bayardo | Using CSP look-back techniques to solve real-world SAT instances[END_REF] 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. In [START_REF] Ansótegui | Using community structure to detect relevant learnt clauses[END_REF], the authors use the community 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 easy the resolution of the instance.

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 [START_REF] Eén | An extensible sat-solver[END_REF] and Glucose [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF] 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.

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.

Motivating example

Let us consider the following relevant strategies: LBD [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF], SIZE (which consider as relevant the clause of the short size) and the relevant measure use by minisat [START_REF] Eén | An extensible sat-solver[END_REF] that we denote here CVSIDS. Suppose that we have in the learned clauses database, the clauses c 1 , c 2 and c 3 with:

• SIZE(c 1 ) = 8, LBD(c 1 ) = 3, CV SIDS(c 1 ) = 1e 100 ; • SIZE(c 2 ) = 6, LBD(c 2 ) = 5, CV SIDS(c 2 ) = 1e 200 ; • SIZE(c 3 ) = 5, LBD(c 3 ) = 4, CV SIDS(c 3 ) = 1e 300 .
The question we ask is the following: which one is relevant? In [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF], the authors consider the clause c 1 which has the most smallest LBD measure as the most relevant. In contrast, the authors of [START_REF] Jabbour | Revisiting the learned clauses database reduction strategies[END_REF] and [START_REF] Goldberg | Berkmin: A fast and robust sat-solver[END_REF] prefer the clause c 3 while the preference of the authors of Minisat [START_REF] Eén | An extensible sat-solver[END_REF] leads to the clause c 3 . 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 c 2 is irrelevant because it is dominated by the clause c 3 on the three given measures.

Formalization

During the search process, the CDCL SAT solvers learn a set of clauses which are stored in the learned clauses database ∆, ∆ = {c 1 , c 2 , ..., c n }. At each cleaning step, we evaluate these clauses with respect to a set M = {m 1 , m 2 , ..., m k } 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, c 1 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 c 3 . 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: , where m i (c) corresponds to the normalized value of the clause c on the measure m i .

Following the same idea, and in order to avoid keep too much learned clauses in the learned clauses database at each reduction step, we propose a variant of our dominance strategy that considers k Reference Learned Clauses (in short k-RLC) instead one that we called here 1-RLC. More precisely, k-RLC strategy is defined as follows: at each reduction step, we delete from the learned clauses database all the clauses dominated by at least one of the k first undominated learned clauses according to the set of learned clauses relevant measures.

In fact, in practice, measures are heterogeneous and defined within different scales. For example the values of the learned clauses relevant measures in [START_REF] Eén | An extensible sat-solver[END_REF] are very high, in exponential order while the values of the relevant measures in [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF] 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 Let us precise that, the value domain of all measures should be in accordance i.e either lower values are better or higher values are better. For example, if we consider the learned clause c 1 , and the three relevant measures LBD, SIZE and CV SIDS, we take 1 CV SIDS(c1) value as the normalized value of the clause c 1 on the measure CV SDIS. In fact, CV SIDS higher value is better, whereas LBD and SIZE values are better. As CV SIDS higher value is better,

1 CV SDIS(c1)
smaller value is so better also. In this way, the measures become comparable over clauses.

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. Proof 3. Trivial by using the proposition 1.

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 [START_REF] Goldberg | Berkmin: A fast and robust sat-solver[END_REF], LBD [START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF] and CV SIDS [START_REF] Eén | An extensible sat-solver[END_REF] measures. All these measures have been proved effective in the literature [START_REF] Eén | An extensible sat-solver[END_REF][START_REF] Audemard | Predicting learnt clauses quality in modern sat solvers[END_REF][START_REF] Jabbour | Revisiting the learned clauses database reduction strategies[END_REF]. 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 [START_REF] Eén | Effective preprocessing in sat through variable and clause elimination[END_REF] 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 k-RLC-Glucose. To determine the best upper bound size k, we run k-RLC-Glucose with k = 1, 3, 5 and 6.

Number of solved instances and CPU time

Table 1 presents results on SAT-RACE-2015. We use the source code of Glucose that deletes from the learned clauses database all the clauses dominated by the k first undominated learned clauses ranked in the increasing order of their degree of compromise. 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 k-RLC-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 10 (respectively 12) more instances are solved by k-RLC-Glucose From this figure, we can observe that k-RLC-Glucose (for the values k = 3, 6) is generally faster than all the other solvers, even if the average running time of LBD-Glucose is slightly better (see Table 1). Although 3-RLC-Glucose needs additional 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. Table 2 shows 6 instances of the SAT-RACE 2015 solved by our approach best version 6-RLC-Glucose in less than 2200 seconds but not solved by LBD-Glucose, SIZE-Glucose, nor CV SIDS-Glucose in 3600seconds. The time used to solve those instances may also explain the increase of the average running time of 6-RLC-Glucose. In addition we also find that there is none instance solved by all the other solvers and not solved by 6-RLC-Glucose (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 2015 dataset. solver k-RLC-Glucose remains competitive and solves more instances than the original solver Glucose for k = 3, 6. The figure 2 presents the cumulated time results on the instances of the SAT competition 2016. It comes out from this second dataset that 3-RLC-Glucose is slightly faster than LBD-Glucose.

LBD-Glucose is more efficient than the other solvers. A more fine analysis of the figure 2 shows that 3-RLC-Glucose is generally more faster on the instances solved in less than 3000 seconds while LBD-Glucose is generally more faster on the instances solved between 3000 seconds and 5000 seconds. This can be explained by the fact that sometimes during the resolution step, very few learned clauses are dominated, thereby our solver keeps too much in the learned clauses database.

This outcome gives credit to the NO FREE Lunch theorem [START_REF] Wolpert | No free lunch theorems for optimization[END_REF]. 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 preferred measures.

RAN D-Glucose solves only 121 instances, 48 instances less than 3-RLC-

Glucose.

Table 4 shows 6 instances of the SAT Competition 2016 solved by our approach best version 3-RLC-Glucose among which 5 instances are solved in less than 5000 seconds but not solved by LBD-Glucose, SIZE-Glucose, nor CV SIDS-Glucose. This confirms as on the instances of the SATRACE 2015 that our dominance approach does not degrade the performance of all the solvers but instead takes advantage of the performance of each relevant measure.

Instances

Common solved instances

In Table 5, 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 235 instances are solved by LBD and 6-RLC. 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. The table 6 gives the result of the intersection of the results between two relevant measures on the instances of the SAT competition 2016. For a given relevant measure, we can see that the number of common instances solved with another measure is less than or equal to the number of common instances solved with our approach k-RLC-Glucose for k = 3. To get more details, Table 7 gives the number of instances commonly solved by the considered relevant measures on the instances of the SAT-RACE-2015.

M easures

M easures

This table allows to see the number of common instances solved by one, two, three or four measures. For example, there are 218 common instances solved by the four deletion strategies, while 43 instances are not solved by none of them.

We can observe that 0, 3, 4, and 6 are the number of instances solved alone by respectively LBD and CV SIDS, SIZE and 6-RLC. Moreover, there is no instance solved by the three strategies (LBD, SIZE and CV SIDS) and not solved by our approach 6-RLC. The table 8 gives more details on the number of instances commonly solved by the considered relevant measures on the instances of the SAT competition 2016. From this table, we observe that 150 common instances solved by the four deletion strategies and 123 instances not solved by none of them. It is important to note on these instances of the SAT competition 2016 no instance is solved by the three strategies (LBD, SIZE and CV SIDS) and not solved by our 3-RLC approach while 6 instances are solved by 3-RLC and not solved by none other measure.

M easures 6-RLC ¬6-RLC CVSIDS ¬CVSIDS CVSIDS ¬CVSIDS LBD SIZE 218 1 0 0 ¬SIZE 14 2 1 0 ¬ LBD SIZE 1 4 2 4 ¬SIZE 1 6 3 43
M easures 3-RLC ¬3-RLC CVSIDS ¬CVSIDS CVSIDS ¬CVSIDS LBD SIZE 150 1 0 2 ¬SIZE 10 0 1 1 ¬ LBD SIZE 1 1 0 1 ¬SIZE 0 6 3 123
Table 8: Detailed of common instances with SAT competition 2016.

Combined measures

Table 9 gives on the number of instances of the SAT-RACE 2015 solved with our dominance approach w.r.t the measures used in the dominance relations.

From this table, we can see that the number of instances solved by using our approach (two or three measures in the dominance) is always greater than the number of instances solved by using each measure alone. We also note 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. time by the number of reductions made before solving the instance. We look these statistics on our best version 6-RLC-Glucose.

M easures

On the Figures 3 and4, the (red) curve of the average percentages of deleted learned clauses exhibits a high variation of the percentages of reduction from 0.15 to 0.95, with an average value equals to 0.37 and 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 217 instances among 248 solved instances.

Our current strategy which uses k (k = 6 for these statistics) undominated learned clauses 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. In contrast, on the Figure 4 where we use the average resolution time instead of the total resolution time, we remark that the instances with the high average percentage of deleted learned clauses have generally the small average resolution times. However, this figure shows some instances with the small average percentage of deleted learned clauses and whose the average resolution times are small.

This clearly shows that the number of deleted learned clauses at each reduction step is important, but is not the only component that impacts the resolution time. Other key components of modern CDCL SAT solver such as the restart policies [START_REF] Gomes | Boosting combinatorial search through randomization[END_REF] and the activity-based variable selection heuristics [START_REF] Moskewicz | Chaff: Engineering an efficient sat solver[END_REF] also have an influence on the resolution time. ing knowledge: for a quickly solving, some instances need the deletion of high number of learned clauses at each reduction step, in contrast, others instances need the deletion of small number of learned clauses. The information is that, we should find the strategies allowing the solver to identify alone at each reduction step both the number of learned clauses to delete and the different clauses to delete. This perfectly fits with the ideas developed in this paper.

For the instances of the SAT competition 2016, the curve of the average percentages of deleted learned clauses exhibits a very high variation of the percentages of reduction from 0.09 to 0.89, with an average value equals to 0.34 and a standard deviation of 0.18. We can observe from the figures 5 and 6 that about 85% of the instances are solved by deleting less than 50% of learned clauses at each reduction step. Compared to the resolution of the instances of the SAT-RACE 2015, our approach keeps more much of learned clauses at each reduction step. However the fact that the total number of clauses that were deleted has changed (37% of the learned clauses removed on the SAT-RACE 2015 and 34% removed on the SAT competition 2016) is not the cause of the small improvement on the instances of the SAT competition 2016, but it is well due to our dominance criterion. In fact, on the instances of the SAT-RACE 2015 (respectively SAT competition 2016) changing the remove half to remove 37% or less than 37% of the learned clauses database (respectively 34% or less than 34%) does not give a similar achievement (see the figures 7 and 8). The goal of this experiment is to see the impact of the quantity of learned clauses to be deleted at each cleaning step on the performance of solver.

As our proposed approach removes approximately an average 36% of learned clauses at each cleaning step, we run each of the three solvers with the quantity of learned clauses to be deleted set to 10%, 20%, 30% and 40% instead of 50%.

The figure 7 (respectively figure 8) shows that for each of the three deletion 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.

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 advantage of each measure. At each reduction step of the learned clauses database, we propose to select the top-k current undominated learned clauses (the k first undominated Reference Learned Clauses) according to a set of relevant learned clauses measures, and to delete all the clauses dominated by at least one of the top-k current undominated learned clauses. 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 by dynamically determining the number of learned clauses to delete at each cleaning step. A general algorithm for our approach is proposed and evaluated on the instances of the the SAT-RACE 2015 and the SAT competition 2016. The experimental results show that exploiting the dominance relationship improves the performance of CDCL SAT solver on these instances. The improvements are more significant on the instances of the SAT-RACE 2015. For the case of SAT-Competition where our approach achieve a small improvement, we must explore the effects of other key components of CDCL SAT solvers on our dominance approach. 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.

Definition 1 (

 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) = 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 that we call here current Reference Learned Clause (in short RLC) 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 the current Reference Learned Clause (in short RLC) 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 M is defined by DegComp(c) = |M | i=1 mi(c) |M |

3 ,

 3 in the interval [0, 1]. More precisely, each value of measure m(c) of any learned clause c must be normalized into m(c) within [0, 1]. The normalization of a given 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 c 1 given in the motivating example in the section 4.1, with its three values : DegComp(c 1 ) = CV SIDS(c1)+ LBD(c1)+ SIZE(c1) 3 , then, we have, DegComp(c 1 ) = with nV ars() the number of variables of the Boolean formula.

Lemma 1 .Proof 1 .Property 1 .Property 2 .Proof 2 .Algorithm 1 : 1 limit = n/2; 2 ind = 0; 3 while ind < limit do 4 clause = ∆[ind] ; 5 if 6 removeClause 11 Proposition 1 .Property 3 .

 1112211234561113 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. 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. In our k-RLC dominance strategy, the k first undominates learned clauses are the k first learned clauses ranked in the increasing order of their degree of compromise. It is important to note that at each reduction step the k first undominates learned clauses are not necessary the k first learned clauses in the learned clauses database ranked in the increasing order of their degree of compromise. Let M be the set of learned clauses relevant measures, ∀c, c , c" three learned clauses, if c c and c c" then c c". 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 k reference learned clauses during each reduction step. During the search process, at each cleaning step of the learned clauses database, We compare all the remaining learned clauses with each of the current reference learned clauses. Thus, for each learned clause, we perform at least 1 comparison and at most k comparisons with the k current reference learned clauses to determine if the clause is dominated and then deleted or if the clause is not dominated and therefore conserved. Given a learned clause database ∆ = {c 1 , c 2 , ..., c n }, k the number of the current Reference Learned Clauses, the time complexity of our k-RLC dominance approach is linear in the worst case. Let ∆ = {c 1 , c 2 , ..., c n } be a a learned clause database, k the number of the current Reference Learned Clauses. For the k-RLC dominance approach, each learned clause is at most compared to the k first undominated learned clauses. So we can make at most k × n comparisons to detect all the learned clauses not dominated by none of the k first reference learned clauses.4.3. AlgorithmIn 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 takes 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 sorts the set of learned clauses according to the degree of compromise of each clause and then removes all the learned clauses that are dominated by at least one of the first k undominated learned clauses. Algorithm 2 depicts our learned clause deletion strategy. It is important to note that our dominance relationship approach does not remove learned clauses whose size (number of literals) and LBD are less than or equal to 2. These clauses are considered as more relevant and are maintained in the learned clauses database. Deletion Strategy: reduceDB function Input: ∆: The learned clauses database of size n Output: ∆ The new learned clauses database of size n/2 sortLearntClauses() ; /* by the defined criterion */ clause.size() > 2 and clause.lbd() > 2 then The k Reference Learned Clauses considered by the algorithm 2 correspond to the k first undominated learned clauses ranked in the increasing order of their degree of compromise. Let ∆ = {c 1 , c 2 , ..., c n } be a learned clause database and k the number of the considered Reference Learned Clauses. Let u be the number of undominated learned clauses after applying the algorithm 2. We have k ≤ u ≤ |∆|.

Glucose 3 .

 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, RAN D-Glucose that randomly deletes learned clauses and finally our proposal k-RLC-

for k = 3 (

 3 respectively k = 6). In fact, solving such additional numbers 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 solves only 209 instances. As randomization of clause deletion sometimes pay [39], we quantify the performance gap between our strategy and the random deletion-based one called here RAN D-Glucose. The solver RAN D-Glucose is obtained as follows: at each conflict, the activity of the learned clause c is set to random value irand(random seed, |V F |), where irand(random seed, |V F |) return a number between 0 and |V F | and V F denotes the set of variables occurring in the boolean formula F. We used exactly the random function of Glucose with the same random seed to allow reproducible results. We can see as reported in the

Figure 1

 1 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.

Figure 1 :

 1 Figure 1: Evaluation on SAT-RACE-2015

Figure 2 :

 2 Figure 2: Evaluation on SAT competition 2016

5. 4 .

 4 Percentage of deleted clausesDuring 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 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, we compute for each version of our solver the average of the average percentage of deleted learned clauses (AverageDeleted). We give also the average of the maximum percentage of deleted learned clauses (AverageDeletedMax) and the average of the minimum percentage of deleted learned clauses (AveragDeletedMin). The results are presented in

Figure 3 :Figure 4 :

 34 Figure 3: Average percentage of deleted clauses and resolution time for each instance of the SAT RACE-2015 with 6-RLC-Glucose solver .

Figure 5 :Figure 6 :

 56 Figure 5: Average percentage of deleted clauses and resolution time for each instance of the SAT competition 2016 with 3-RLC-Glucose solver.

  strategies (LBD, SIZE and CV SIDS), even by removing less than fifty percent of the learned clauses at each reduction, the performances of Glucose solver are not improved on the SAT-RACE 2015 instances (respectively SAT competition 2016). This clearly shows the benefit of our dominance relationship on these instances.

Figure 7 :

 7 Figure 7: Number of solved instances per percentage of deleted learned clauses on the instances of the SAT-RACE-2015

Figure 8 :

 8 Figure 8: Number of solved instances per percentage of deleted learned clauses on the instances of the SAT competition 2016

Table 1 :

 1 Comparative evaluation on SAT-RACE-2015.

	Solvers	#Solved (#SAT -#UNSAT) Average Time
	M inisat 2.2	209 (134 -75)	585.19 s
	RAN D-Glucose	174 (99 -75)	608.82 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
	1-RLC-Glucose	238 (138 -100)	481.72 s
	3-RLC-Glucose	246 (144 -102)	523.46 s
	5-RLC-Glucose	245 (144 -101)	542.29 s
	6-RLC-Glucose	248 (145 -103)	532.05 s

table 1 that RAN D-Glucose is the worst solver among the five solvers, it solves 174 instances, 72 (respectively 74) instances of less than our solver k-RLC-Glucose for k = 3 (respectively k = 6). This shows the interest of our dominance relationship approach on the instances of the SAT-RACE 2015.

Table 3

 3 presents results on the instances of the SAT Competition 2016. Here

	Instances	LBD SIZE CVSIDS	6-RLC
	jgiraldezlevy.2200.9086.08.40.8	-	-	-	80.57 s
	jgiraldezlevy.2200.9086.08.40.149	-	-	-	393.51 s
	jgiraldezlevy.2200.9086.08.40.2	-	-	-	1599.86 s
	manthey DimacsSorterHalf 37 3	-	-	-	1763.42 s
	manthey DimacsSorter 37 3	-	-	-	1770.69 s
	hwmcc10-*-pdtvisns3p00-tseitin	-	-	-	2146.03 s

LBD-Glucose and CV SIDS-Glucose solve the same number of instances. Our

Table 2 :

 2 Instances solved by 6-RLC-Glucose and not solved by the others on SAT-RACE 2015.

Table 3 :

 3 Comparative evaluation on SAT-Competition-2016.

Table 4 :

 4 Instances solved by 3-RLC-Glucose and not solved by the others on SAT-

		LBD SIZE CVSIDS	3-RLC
	barman-pfile08-032.sas.ex.15	-	-	-	5.01 s
	partial-10-19-s	-	-	-	1248.47 s
	ak128modasbg2asisc	-	-	-	1021.06 s
	par32-3-c	-	-	-	2206.07 s
	gss-24-s100	-	-	-	4753.82 s
	eq.atree.braun.13.unsat	-	-	-	6683.69 s
	Competition-2016.

Table 5 :

 5 Common solved Instances from SAT-RACE-2015.

		LBD SIZE CVSIDS 6-RLC
	LBD	236			235
	SIZE	219	230		224
	CVSIDS	233	221	240	234
	6-RLC				248

Table 6 :

 6 Common solved Instances from SAT competition 2016.

		LBD SIZE CVSIDS 3-RLC
	LBD	165			161
	SIZE	153	156		153
	CVSIDS	161	151	165	161
	3-RLC				169

Table 7 :

 7 Detailed of common instances with SAT-RACE 2015.

Table 9 :

 9 Combining two measures on SAT-RACE-2015.

		LBD SIZE CVSIDS 6-RLC-Glucose
	LBD	236
	SIZE	238	230
	CVSIDS	245	246	240
	6-RLC-Glucose			248
	The results of the table 10 confirm the results of the table 9 of the SAT
	RACE-2015 in the sense that the number of instances of the SAT competition
	2016 solved by using two measures (160 by using SIZE and LBD measures,

Table 10 :

 10 Combining two measures on SAT competition 2016.

Table 11 (

 11 respectively Table12) for the instances of the SAT-RACE

	2015 (respectively SAT competition 2016). We can see that on the instances of
	the SAT-RACE 2015, our best version 6-RLC-Glucose deletes in average 37%
	of learned clauses at each reduction step, with a standard deviation of 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 (overall solving 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

Table 11 :

 11 Average of the average (respectively maximum and minimum) percentage of deleted learned clauses on SAT-RACE-2015.

	Solvers	AverageDeleted	AverageDeletedMax	AverageDeletedMin
	1-RLC-Glucose	0.30	0.70	0.08
	3-RLC-Glucose	0.34	0.71	0.08
	5-RLC-Glucose	0.37	0.71	0.09
	6-RLC-Glucose	0.37	0.71	0.09

Table 12 :

 12 Average of the average (respectively maximum and minimum) percentage of deleted learned clauses on SATcompetition 2016.

Acknowledgements

The authors would like to thank Auvergne-Rhô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.