An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers

1 Introduction

Modern Conflict-Driven Clause Learning (CDCL) SAT solvers are routinely used as core solving engines in many real-world applications. Their ability to solve challenging problems comes from the combination of different ingredients: variable selection heuristics, Boolean constraint propagation, clause learning, restarts, clause database management, data structures, preprocessing and inprocessing.

Formula simplification techniques applied during preprocessing have proven useful in enabling efficient SAT solving for real-world application domains (e.g. [Bacchus and Winter, 2003; E´en and Biere, 2005; Piette et al., 2008]). The most successful preprocessing techniques include variants of bounded variable elimination, addition or elimination of redundant clauses, detection of subsumed clauses and suitable

∗Research partially supported by the National Natural Science Foundation of China (Grants no. 61370183, 61370184, 61472147), the Generalitat de Catalunya grant AGAUR 2014-SGR-118, and the MINECO-FEDER project RASO TIN2015-71799-C2-1-P.

†Corresponding author combinations of them. They aim mostly at reducing the number of clauses, literals and variables in the input formula.

More recently, some solvers have significantly boosted their performance by interleaving formula simplification techniques with CDCL search. Among such inprocessing techniques [J¨arvisalo et al., 2012], we mention local and recursive clause minimization [Beame et al., 2004; S¨orensson and Biere, 2009], which remove redundant literals from learnt clauses immediately after their creation; clause distillation in a concurrent context [Wieringa and Heljanko, 2013]; and onthe-fly clause subsumption [Han and Somenzi, 2009; Hamadi et al., 2009], which efficiently removes clauses subsumed by the resolvents derived during clause learning. Nevertheless, there is a common belief that clause simplification techniques that bring substantial gains in preprocessing do not increase significantly the performance of solvers when they are applied to learnt clauses during the search [Biere, 2011; Wotzlaw et al., 2013].

Given the impact of clause learning on the resolution of practical instances, the objective of this paper is to devise and implement a new inprocessing learnt clause minimization approach able to remove redundant literals from learnt clauses for CDCL solvers. Our approach is based on Boolean constraint propagation, or more precisely unit (clause) propagation, which is notably time-consuming on large instances. Hence, in what follows, we must carefully decide how to deal with the following issues: (1) when should the clause minimization procedure be activated? (2) which learnt clauses should be minimized? and (3) how should unit propagation be applied?. By adequately answering these three questions, the proposed approach reaches a good trade-off between effectiveness and efficiency. Observe that such an approach was missing in the literature, explaining the fact that the winners of the 2016 SAT competition did not use unit propagation to minimize learnt clauses.

We evaluated our approach on five of the best performing CDCL SAT solvers: Glucose [Audemard and Simon, 2009], COMiniSatPS [Oh, 2016], MapleCOMSPS [Liang et al., 2016c], MapleCOMSPS LRB [Liang et al., 2016b] and TC Glucose [Moon and Mary, 2016]. The experimental results show that the proposed approach allows them to solve a remarkable number of additional instances coming from the hard combinatorial and application categories of the 2014 and 2016 SAT competitions.

We quote a statement of two leading SAT solver developers [Audemard and Simon, 2012] to better appreciate the significance of our contributions:

"We must also say, as a preliminary, that improving SAT solvers is often a cruel world. To give an idea, improving a solver by solving at least ten more instances (on a fixed set of benchmarks of a competition) is generally showing a critical new feature. In general, the winner of a competition is decided based on a couple of additional solved benchmarks."

The previous statement was also quoted in [Liang et al., 2016a] to appreciate the advance brought about by the CHB branching heuristic in CDCL solvers.

The paper is organized as follows: Section 2 gives some basic concepts about SAT and CDCL solvers. Section 3 presents some related works on inprocessing and preprocessing clause minimization. Section 4 describes the new learnt clause minimization approach, as well as how it is implemented in different CDCL solvers. Section 5 reports on the experimental investigation. Section 6 contains the concluding remarks.

2 Preliminaries

Let V = {x1, . . . , xn} be a set of propositional variables. A literal is a propositional variable x or its negation x. A clause is a disjunction of literals. The size of a clause refers to the number of literals it contains. A unit clause contains exactly one literal. A Conjunctive Normal Form (CNF) formula is a conjunction of clauses. A CNF formula is also represented by the set of its clauses, and a clause by the set of its literals. A clause C ′ subsumes a clause C iff C ′ ⊂ C.

Let ρ : V → {0, 1} be a truth assignment. The assignment ρ satisfies a literal x (x) iff ρ(x) = 1 (ρ(x) = 0), satisfies a clause iff it satisfies any of its literals, and satisfies a CNF formula iff it satisfies all its clauses. A CNF formula F is satisfiable iff there is at least one satisfying assignment. The empty clause (□) is always unsatisfiable, and represents a conflict or a failure. SAT is the problem of deciding whether a given CNF formula is satisfiable. Two formulas are logically equivalent iff they are satisfied by the same assignments. A literal l is redundant in a clause C of a formula F if removing l fromC results in a formula logically equivalent to F.

Given a CNF formula F and a literal l, we define F|l to be the CNF formula resulting from F after removing the clauses containing an occurrence of l and all the occurrences of l. We recursively define Boolean constraint propagation, or more precisely Unit Propagation (UP), using the following two rules: (R1) UP(F) = F if F does not contain any unit clause; and (R2) UP(F) = UP(F|l) if there is a unit clause {l} in F. In the latter case, we say that the literal l is asserted by UP, and it must hold that ρ(l) = 1. The literal l is deduced or asserted by UP(F) if the unit clause {l} is obtained by applying R2. When UP(F ∪ {l}) is computed, we say that l is propagated in F .

In the sequel, we use UP(F) to denote the CNF formula obtained from F after repeatedly applying R2 until there is no unit clause or the empty clause is derived. Concretely, UP(F) = □ if repeatedly applying R2 derives the empty clause. Otherwise, UP (F ) denotes the CNF formula in which all unit clauses have been propagated using R2.

A CDCL solver [Marques-Silva and Sakallah, 1999; Moskewicz et al., 2001] performs a non-chronological backtrack search in the space of partial truth assignments. Concretely, the solver repeatedly picks a decision literal li and applies unit propagation in F ∪{l1, l2, . . . , li} (i.e., computes UP(F∪{l1, l2, . . . , li}) until the empty formula or the empty clause are derived. If the empty clause is derived, the reasons are analyzed and a clause (nogood) is learnt using a particular method, usually the First UIP (Unique Implication Point) scheme [Zhang et al., 2001]. The learnt clause is then added to the clause database.

Let F be a CNF formula, let li be the ith decision literal picked by a CDCL solver, and let Fi = UP(F ∪ {l1, l2, . . . , li}). We say that li and all the literals asserted when computing UP(Fi-1 ∪ {li}) belong to level i. Literals asserted in UP(F) do not depend on any decision literal and form level 0. When UP deduces the empty clause and a learnt clause is extracted from the conflict analysis, the solver cancels the literal assertions in the reverse order until the level where the learnt clause contains one non-asserted literal, and continues the search from that level after propagating the nonasserted literal. Under certain conditions, the solver cancels the literal assertions until level 0 and restarts the search from level 0. Since too many learnt clauses slow down the solver and may overflow the available memory, the solver periodically removes a subset of learnt clauses using a particular clause deletion strategy.

The literals of a learnt clause C are partitioned w.r.t. their assertion level. The number of sets in the partition is called the Literal Block Distance (LBD) of C. As Audemard and Simon (2009) showed, LBD measures the quality of learnt clauses. Clauses with small LBD values are considered to be more relevant. The best performing CDCL solvers of the recent SAT competitions use LBD as a measure of the quality of learnt clauses to decide which clauses must be removed or retained. Moreover, solvers like Glucose and its derivatives use the LBD of recent learnt clauses to decide when a restart must be triggered.

3 RelatedWork on Clause Minimization

Clause minimization (see e.g. [E´en and Biere, 2005; Han and Somenzi, 2007; Piette et al., 2008; S¨orensson and Biere, 2009; Wotzlaw et al., 2013; Marques-Silva, 2000; Han and Somenzi, 2009; Hamadi et al., 2009; Wieringa and Heljanko, 2013]) both before and during the search is crucial for the performance of CDCL SAT solvers for two reasons: (i) shorter clauses need less memory and, more importantly, (ii) shorter clauses are easier to become unit, and thus increase the power of unit propagation.

The most effective approach to remove redundant literals in learnt clauses probably is recursive clause minimization [S¨orensson and Biere, 2009], which can be specified using the notion of involved literal. Let C = l1 ∨ l2 ∨ · · · ∨ lk be a newly created learnt clause. Then, (i) all literals in C are involved; and (ii) for any other literal l, if there is a clause C ′ = l′1 ∨l′2 ∨. . .∨l′k′ ∨l such that l′1 , l′2 , . . ., l′k′ are involved, then l is involved. Recursive clause minimization tests each literal li of C. If there is a clause C ′ = l′1 ∨ l′2 ∨ . . . ∨ l′k′ ∨ li such that l′1 , l′2 , . . ., l′k′ are involved, then li is removed from C. MiniSAT 1.13 implements recursive clause minimization in a very ingenious way and applies it to each new learnt clause. This approach is now part of many SAT solvers, and frequently removes more than 30% of literals.

Another effective inprocessing clause minimization approach is based on binary implication graphs [Heule et al., 2011]. Given a CNF formula F , the algorithm first performs a depth-first search over the binary implication graph to assign a time stamp to each literal in the graph. It then uses these time stamps to discover and remove various kinds of redundancy, including redundant literals in learnt clauses. The algorithm is linear in the total number of literals in F and is realized in a function named Stamp in Lingeling [Biere, 2010] and MapleCOMSPS LRB. As an inprocessing, the function is executed upon some restarts to minimize learnt clauses.

In solvers such as Glucose and MapleCOMSPS, a restriction of the resolution rule is applied to minimize a newly created learnt clause C = l1 ∨ l2 ∨ · · · ∨ lk whose LBD or size is smaller than a prefixed limit. The first literal l1 of C is called the asserting literal. For any i > 1, if l1 ∨ li is a clause in F, then Glucose and MapleCOMSPS remove li from C.

Conflict analysis consists in performing successive resolution steps from a conflicting clause. At each step, a new resolvent is derived from two clauses C ′ and C ′′ , where C ′ is the conflicting clause or a previous resolvent, and C ′′ is an existing clause. If C ′′ = l ∨ C and C ′ = l ∨D, where l is a literal, and C and D are disjunction of literals with D ⊆ C, the resolvent of C ′ and C ′′ is C and subsumes C ′′ , meaning that l is redundant in C ′′ and can be removed from C ′′ . This approach allows to minimize both original clauses and learnt clauses during the search and was proposed independently in [Han and Somenzi, 2009] and [Hamadi et al., 2009]. It was implemented in CryptoMinisat 2.5.0 [Soos, 2010] for on-thefly clause improvement.

Preprocessing clause minimization can devote more time to each clause and still improve the performance of solvers. Piette et al. (2008) applied the following rules in a vivification procedure after sorting the literals of a clause C = l1 ∨ l2 ∨ · · ·∨lk of the input formula F using a MOMS-style [Jeroslow and Wang, 1990] ordering:

1. If for some i ∈ {1, 2, . . . , k - 1} and some j > i, UP((F \ {C}) ∪ {l1, l2, . . . , li}) deduces lj , then F ← (F \ {C}) ∪ {l1 ∨ l2 ∨ . . . ∨ li ∨ lj}.
2. If for some i ∈ {1, 2, . . . , k - 1} and some j > i, UP((F \ {C}) ∪{l1, l2, . . . , li}) deduces lj, then F ← (F \{C})∪{l1∨l2∨. . .∨li∨· · ·∨lj-1∨lj+1∨· · ·∨lk}.
3. If for some i ∈ {1, 2, . . . , k - 1}, UP((F \ {C}) ∪ {l1, l2, . . . , li}) = □, then extract a nogood Cl from the conflict using the First UIP scheme. If Cl ⊂ C or |Cl| < |C| then F ← (F \ {C}) ∪ Cl, otherwise F ← (F \ {C}) ∪ {l1 ∨ l2 ∨ . . . ∨ li}.

Independently, Han and Somenzi (2007) proposed a similar approach called distillation.

Vivification and distillation are usually applied during preprocessing, because they need many time-consuming unit propagations. One exception is CryptoMinisat, which implements a limited distillation as inprocessing. In the context of parallel solvers, Wieringa and Heljanko (2013) use a concurrent thread to repeatedly select and minimize the best learnt clause (according to some criteria such as clause size or LBD) among the newest 1000 learnt clauses using unit propagation.

Nevertheless, to the best of our knowledge, none of the awarded CDCL solvers in the 2016 SAT Competition uses a distillation or vivification approach to minimize learnt clauses. In particular, the solver Riss6, the silver medal winner of the main track, disables a vivification based learnt clause minimization used in Riss 5.05, because it turned out to be ineffective for formulas of more recent years according to [Manthey et al., 2016]. In fact, it is generally believed that inprocessing clause minimization based on unit propagation can hardly be made effective for CDCL solvers. Wotzlaw et al. (2013) applied distillation to minimize the 100 most active clauses during the search, and concluded that inprocessing distillation is generally not as effective as preprocessing distillation, as well as that developing effective inprocessing techniques is non-trivial and requires in-depth knowledge about how different techniques can be combined and integrated efficiently into the solvers.

4 Minimizing Learnt Clauses During Search

The main objective of this paper is to devise and implement an effective and efficient inprocessing approach to minimize learnt clauses using unit propagation. This inprocessing was missing in the literature, as is illustrated by the fact that the winners of the 2016 SAT competition did not use unit propagation to minimize learnt clauses. We first describe the general principle used to efficiently minimize learnt clauses, and then present its implementation in Glucose, TC Glucose, COMiniSatPS, MapleCOMSPS and MapleCOMSPS LRB.

4.1 General Principle

In order to make learnt clause minimization effective and efficient, we have to answer the following questions:

1. When should we minimize the learnt clauses? It seems clear enough that learnt clause minimization should be activated at level 0 to ensure that the minimization is independent of any branching decision. In other words, it should be activated upon a restart. So, the relevant questions are: should we activate learnt clause minimization for every restart? If not, how do we determine the restarts upon which we activate learnt clause minimization?
2. Should we minimize each learnt clause? If not, which learnt clauses should be minimized?
3. Clause minimization based on unit propagation clearly depends on the ordering selected to propagate the literals. What is the best order in which the literals of a learnt clause should be propagated during learnt clause minimization?

The most satisfactory answers to these questions depend on other techniques implemented in the solver. Nevertheless, we want to argue the following general principle for guiding the implementation of learnt clause minimization:

Algorithm 1: minimization(F, L, nbNewLearnts, σ), a generic learnt clause minimization algorithm

Input: F : A CNF formula; L: a set of learnt clauses such that L ∩ F = ∅; nbNewLearnts: the number of clauses learnt since the last execution of function minimizeL; σ: the number of times function minimizeL was executed so far.

Output: A set of learnt clauses. begin 1 if liveRestart(nbNewLearnts, σ) then 2 L ← minimizeL(F, L); /* call Algorithm 2 */ 3 nbNewLearnts ← 0; σ + +; 4 return L; 5 end 6

1. Clause minimization should not be activated at each restart. In fact, the number of newly learnt clauses per restart may not be sufficient for unit propagation to easily deduce a conflict. So, we adopt the clause reduction strategy of Glucose to activate learnt clause minimization. More precisely, we define function liveRestart(nbNewLearnts, σ) to determine if learnt clause minimization has to be activated at the beginning of a restart. In the function, nbNewLearnts and σ are global variables representing, respectively, the number of clauses which were learnt since the last learnt clause minimization, and the number of learnt clause minimizations performed so far.
2. Chanseok Oh (2016) empirically showed that learnt clauses with high LBD values are not very useful to solve practical SAT instances. Indeed, the LBD of a learnt clause is correlated to the minimum number of decisions needed to make the clause failed, meaning that it is much harder to reduce the LBD of a learnt clause than to reduce its size. Moreover, clauses with high LBD are generally long, needing more unit propagations to be minimized. In Section 5, we will give empirical evidence showing that minimizing clauses with high LBD is very costly and useless. So, we should minimize learnt clauses with small LBD values. More precisely, we define a function liveClause(C) to determine if a learnt clause C has to be minimized according to its LBD.
3. A function sort(C) is defined to sort the literals before minimizing the learnt clause C.

Algorithm 1 realizes this general principle and is called at the beginning of each restart. Function minimizeL(F, L) is defined in Algorithm 2. We will precisely define function liveRestart(nbNewLearnts, σ) later when we implement Algorithm 1 in a solver.

Algorithm 2 works as follows:

1. Let C = l1 ∨ l2 ∨ · · · ∨ lk be a learnt clause in L such that liveClause(C) is true. If UP(F∪{l1, l2, . . . , li}) = □, then F ∪ {l1, l2, . . . , li} is unsatisfiable and the clause l1 ∨ l2 ∨ · · · ∨ li is a logical consequence of F and can be added to F to subsume C without affect-

Algorithm 2: minimizeL(F,L): minimizing a set of learnt clauses

ing satisfiability. Let C ′ = {l′1 , l′2 , . . . , l′i-1 }. Function conf lAnalysis(F, L, C ′ ∪{li}, R) retraces the implication graph from the conflicting clause R derived by UP until the literals in C ′∪{li}, in order to collect the literals in C ′ ∪ {li} from which there is a path to the conflicting clause R in the implication graph. The function returns a disjunction of the negation of the collected literals. Note that Function conf lAnalysis(F, L, C ′ ∪ {li}, R) does not use the first UIP scheme, which is different from Rule 3 in the vivification approach in [Piette et al., 2008]. Algorithm 2 (line 7) applies UP(F ∪L∪C ′ ∪{li}) incrementally for efficiency reasons: li is propagated in the formula returned by UP(F ∪ L ∪ C ′ ) after checking if li or li is not asserted. UP(F ∪ L ∪ C ′ ∪ {li}) is implemented using the unit propagation function and the watched literal data structures of the solver.

1. If UP(F ∪ {l1, l2, . . . , li-1, li}) = □, then C ′′ = l1 ∨ l2 ∨ · · · ∨ li-1 ∨ li is a logical consequence of F. The resolvent of C = l1 ∨ l2 ∨ · · · ∨ lk (k ≥ i) and C ′′ does not contain li and subsumes C. So, Algorithm 2 does not add li to the new clause C ′ in this case. Actually, Algorithm 2 (line 10) computes UP(F ∪ L ∪ C ′ ∪ {li}) by checking if UP(F ∪ L ∪ C ′ ) deduces li, instead of propagating li, for efficiency reasons.

The implementation of Algorithm 2 in a solver needs the definition of functions liveClause(C) and sort(C), which will be discussed later. A common constraint we impose is that if a learnt clause C has been minimized in a previous call of Algorithm 2, liveClause(C) returns false. In this way, a learnt clause is minimized at most once in our approach.

4.2 Minimizing Learnt Clauses in Glucose and TC Glucose

Glucose is a very efficient CDCL solver developed from Minisat [E´en and S¨orensson, 2003]. It was habitually awarded in SAT competitions between 2009 and 2014, and is the base solver of many other awarded solvers.

Glucose was the first solver which incorporated the LBD measure in the clause learning mechanism and adopted an aggressive strategy for clause database reduction. We used Glucose 3.0, in which the reduction process is fired once the number of clauses learnt since the last reduction reaches f irst + 2 × inc × σ, where f irst = 2000 and inc = 300 are parameters, and σ is the number of database reductions performed so far. The learnt clauses are first sorted in decreasing order of their LBD values, and then the first half of learnt clauses are removed except for the binary clauses, the clauses whose LBD value is 2, and the clauses that are reasons of the current partial assignment. Note that the reduction process is not necessarily fired at level 0.

Glucose 3.0 also features a fast restart mechanism which is independent of the clause database reduction. Roughly speaking, Glucose restarts the search from level 0 when the average LBD value in recent learnt clauses is high compared with the average LBD value of all the learnt clauses.

Solver TC Glucose is like Glucose 3.0 but it uses a tie-breaking technique for VSIDS, and the CHB branching heuristic [Liang et al., 2016a] instead of the VSIDS branching heuristic for small instances. It was the best solver of the hard combinatorial category in the 2016 SAT Competition.

Learnt clause minimization in Glucose and TC Glucose is implemented by defining the three functions in Algorithm 1 and Algorithm 2 as follows:

Function liveRestart(nbNewLearnts, σ) returns true iff the learnt clause reduction process was fired in the preceding restart. In other words, the learnt clause minimization in Glucose and TC Glucose follows their learnt clause database reduction, after which only the first half of learnt clauses remains.

Function liveClause(C) returns true if C has not yet been minimized and belongs to the second half of learnt clauses after sorting the clauses in decreasing order of their LBD values.

Function sort(C) returns C without changing the order of its literals. This order is roughly the reverse order in which these literals are involved to deduce a literal in the conflicting level according to the First UIP scheme.

Algorithm 1 is executed before every restart. It calls Algorithm 2 if liveRestart(nbNewLearnts, σ) returns true.

4.3 Minimizing Learnt Clauses in COMiniSatPS, MapleCOMSPS andMapleCOMSPS LRB

COMiniSatPS is a SAT solver created by applying a series of small diff patches to MiniSAT 2.2.0. Its initial prototypes (SWDiA5BY and MiniSat HACK xxxED) won six medals in the 2014 SAT Competition and the 2014 Configurable SAT Solver Challenge. MapleCOMPS and MapleCOMSPS LRB are based on COMiniSatPS, and were the winners of the main track and the application category in the 2016 SAT Competition, respectively.

The clause database reduction policy of COMiniSatPS, MapleCOMSPS and MapleCOMSPS LRB is quite different from that of Glucose. In these solvers, the learnt clauses are divided into three subsets: (1) clauses whose LBD value is smaller than or equal to a threshold t1 are stored in a subset called CORE; (2) clauses whose LBD value is greater than t1 and smaller than or equal to another threshold t2 are stored in a subset called TIER2; and (3) the remaining clauses are stored in a subset called LOCAL. If a clause in TIER2 is not involved in any conflict for a long time, it is moved to LOCAL.

Periodically, the clauses of LOCAL are sorted in increasing order of their activity in recent conflicts, and the learnt clauses in the first half are removed (except for the clauses that are reasons of the current partial assignment).

The three solvers interleave Glucose-style restart phases with no restart or Luby restart phases.

Learnt clause minimization in COMiniSatPS, MapleCOMSPS and MapleCOMSPS LRB is implemented by defining the three functions in Algorithm 1 and Algorithm 2 as follows (recall that Algorithm 1 is executed before each restart):

Function liveRestart(nbNewLearnts, σ) returns true iff nbNewLearnts, the number of clauses learnt since the last learnt clause minimization, is greater than or equal to α+2× β × σ. We empirically fixed α=1000, β=1000 for the three solvers. Note that function liveRestart(nbNewLearnts, σ) does not follow the clause database reduction in any of the three solvers.

Function liveClause(C) returns true iff C has not yet been minimized and belongs to CORE or TIER2.

Function sort(C) returns C without changing the order of its literals.

5 Experimental Investigation

We implemented the learnt clause minimization approach described in Section 4 in solvers Glucose 3.0, TC Glucose, COMiniSatPS (COMSPS for short), MapleCOMSPS (Maple for short) and MapleCOMSPS LRB (MapleLRB for short). The resulting solvers 1 are named Glucose+, TC Glucose+, COMSPS+, Maple+ and MapleLRB+, respectively. Besides, we created the solvers MapleLRB/noSp and MapleLRB+/noSp by disabling in MapleLBR and MapleLRB+, respectively, the inprocessing technique of [Heule et al., 2011], based on binary implication graphs, that implements function Stamp (noSp means that function Stamp is removed in MapleLRB/noSp and MapleLRB+/noSp).

The test instances include the application and hard combinatorial tracks of the 2014 and 2016 SAT competitions, and the community attachment formulas proposed in [Gir´aldezCru and Levy, 2015]. The experiments were performed on a computer with Intel Westmere Xeon E7-8837 processors at 2.66 GHz and 10 GB of memory under Linux. The cutoff time is 5000 seconds for each instance and each solver.

Table 1 compares the solvers Glucose, Glucose+, COMSPS, COMSPS+, Maple, Maple+, MapleLRB, MapleLRB+, MapleLRB/noSp and MapleLRB+/noSp on instances of the application category of the 2014 and 2016 SAT competitions.

1 Available at http://home.mis.u-picardie.fr/˜cli/

Our learnt clause minimization consistently improves the performance of all the solvers. In particular, MapleLRB was the best solver in this category in the 2016 Competition, but it solved only 4 instances more than the 4th and the 5th solvers of this category. Our approach allows MapleLRB+ to solve 15 instances more than MapleLRB.

Figure 1 shows a sample of scatter plots comparing MapleLRB+ and MapleLRB on 3 benchmark families of the application category of the 2016 SAT competition. A family consists of instances with similar names. A point (x, y) in the plots corresponds to an instance, where x (y) represents the solving time in seconds of MapleLRB+ (MapleLRB). A point (x, y) where x = 5000 (y = 5000) means that the instance was not solved by MapleLRB+ (MapleLRB) within a cutoff time of 5000s.

Table 1 also compares our inprocessing approach with the inprocessing approach of [Heule et al., 2011], by means of four solvers: MapleLRB, MapleLRB+, MapleLRB/noSp and MapleLRB+/noSp. The only difference of these four solvers is specified in their names:

MapleLRB+: with our approach and with Stamp, the function implementing the inprocessing approach of [Heule et al., 2011];

MapleLRB+/noSp: with our approach but without Stamp;

MapleLRB: without our approach but with Stamp;

MapleLRB/noSp: without our approach and without Stamp.

The inprocessing approach of [Heule et al., 2011] implemented in MapleLRB allows MapleLRB to solve 3 (2) instances of 2014 (2016) more than MapleLRB/noSp, which has disabled that inprocessing. However, our approach is more effective, allowing MapleLRB+/noSp to solve 16 (14) instances of 2014 (2016) more than MapleLRB/noSp, and MapleLRB+ to solve 14 (15) instances of 2014 (2016) more than MapleLRB.

Figure 2 shows the cactus plots of the four solvers on the application instances of the 2014 SAT competition (top) and of the 2016 SAT competition (bottom). The two solvers using our approach perform clearly better than the two solvers using the approach of [Heule et al., 2011]. Note that the inprocessing approach of [Heule et.al. 2011] is also used in Lingeling and subsumes (at least partly) many inprocessing techniques.

# of Solved Instances

Table 2 compares Maple, Maple+, TC Glucose, TC Glucose+, MapleLRB, MapleLRB+, MapleLRB/noSp and MapleLRB+/noSp on the hard combinatorial instances of the 2014 and 2016 SAT competitions. Observe that the instances of the 2016 SAT Competition are very special, because the best solver for these instances (TC Glucose) performs significantly less well than the other solvers on the 2014 instances. The performance of Maple+, TC Glucose+ and MapleLRB+ is similar to that of Maple, TC Glucose and MapleLRB, respectively, on the 2016 instances. However, their performance is significantly better than that of Maple, TC Glucose and MapleLRB on the 2014 instances.

Note that all the solvers in Table 1 and Table 2 implement the following inprocessing techniques: the clause minimization based on binary clause resolution of Glucose and the recursive learnt clause minimization of MiniSat. MapleLRB and MapleLRB+ include, in addition, the inprocessing approach of [Heule et al., 2011]. The results show that our approach is compatible with all these techniques.

Table 3 compares different implementations of the learnt clause minimization in Glucose and MapleLRB on application instances of the 2014 SAT Competition, by varying the liveRestart(nbNewLearnts, σ), liveClause(C) and sort(C) functions.

Glucose+/α-β: it is like Glucose+ but does not follow the learnt clause database reduction of Glucose any more. Instead, liveRestart(nbNewLearnts, σ) returns true iff nbNewLearnts ≥ α + 2 × β × σ.

Glucose+H lbd: it is like Glucose+ but liveClause(C) is true iff C was never minimized before and is in the first half of learnt clauses when these clauses are sorted in decreasing order of their LBD value. In other words, the learnt clauses with higher LBD are minimized in Glucose+H lbd.

Glucose+∆: it is like Glucose+ but liveClause(C) is true iff C was never minimized before and is in the last ∆ fraction of learnt clauses when these clauses are sorted in decreasing order of their LBD value. Glucose+ is in fact Glucose+1/2.

MapleLRB+/Core: it is like MapleLRB+, but it minimizes every non-yet-minimized clause in CORE upon every restart. It minimizes the clauses in TIER2 as in MapleLRB+.

Low2highLevel, High2lowLevel, Low2highActivity, High2lowActivity, Random and Reverse: all these solvers are like MapleLRB+, except that function sort(C) is different. In solver Low2highLevel (Low2highActivity), literals in C are ordered from small level (activity) to high level (activity). In solver High2lowLevel (High2lowActivity), literals in C are ordered from high level (activity) to small level (activity). The level of a literal in C refers to the level of its last assertion. In solver Random, literals in C are randomly ordered. In solver Reverse, literals in C are reversed.

Table 3 shows the number of (Total, Sat, Unsat) instances solved by each solver within 5000s and exhibits some statistics about their runtime behavior. Column 5 (Impact) gives the clause size minimization measured as (a - b)/a, where a (b) is the total number of literals in the minimized clauses before (after) the minimization. Column 6 (Cost) gives the cost of the learnt clause minimization measured as the ratio of the total number of unit propagations performed by Algorithm 2 to the total number of other propagations performed in the search. Column 7 (LiveC) gives the ratio of the number of clauses minimized to the total number of learnt clauses. All data are averaged over the solved instances among the 300 application instances of the 2014 SAT Competition.

Several observations can be made from Table 3.

• All the described implementations of learnt clause minimization, except for the solvers Reverse and Glu-

cose+H lbd, improve their original solver, which provides evidence of the robustness of our approach.

• Both MapleLRB+ and MapleLRB+/Core minimize all the clauses in CORE but at different times. The superior performance of MapleLRB+ over MapleLRB+/Core might be explained as follows: When MapleLRB+ minimizes a clause in CORE, there are usually more learnt clauses in the clause database, allowing unit propagation to deduce more easily the empty clause.
• Propagating the literals of C in the original order is the best option, whereas propagating the literals in the reverse order is the worst option. Recall that the original order of C is roughly the reverse order in which these literals are involved to deduce a literal in the conflicting level according to the First UIP scheme.
• Minimizing clauses with high LBD is very costly and useless, because Glucose+H lbd is significantly worse than Glucose.
• The cost of the approach in Glucose+∆ is relatively small, because the solver just removed half of the learnt clauses when learnt clause minimization was activated, which is not the case for other solvers.
• Glucose+ and MapleLRB+ offer the best trade-off between cost and impact, explaining their superior performance.

It is known that industrial SAT instances exhibit community structure [Ans´otegui et al., 2012; Newsham et al., 2014] and the LBD of a learnt clause is related to the community structure [Ans´otegui et al., 2015]. We analyze our approach using the community attachment formulas proposed in [Gir´aldez-Cru and Levy, 2015]. In these instances, variables are partitioned into communities and the community of a variable can be easily determined. We generated and solved 100 instances at each point with the same parameters as in Table 1 of [Gir´aldez-Cru and Levy, 2015] (modularity Q = 0.9, 0.8 or 0.7, clause size k = 3, number of communities c = 40, clause to variable ratio r′ = 4.06, 4.11 or 4.13, and number of variables n = 5000, 2000, or 1200), using the generator in [Gir´aldez-Cru and Levy, 2015]. Recall that formulas with higher modularity exhibit clearer community structure.

The impact of our approach on the size, the LBD and the number of communities of a learnt clause is measured as ratio = (value before reduction - value after reduction)/value before reduction, and is averaged over the 100 instances at each point. As shown in Table 4 with the data from the resolution of the community attachment formulas and the application instances of the 2014 SAT competition by MapleLRB+, the impact of our approach on the clause size (size red ratio) is significantly higher than the impact on the LBD (lbd red ratio) and on the number of communities (comm red ratio) of a clause. This means that reducing the LBD and the number of communities of a clause is harder than reducing its size. The same observation applies to the application instances of the 2014 SAT competition.

Moreover, the impact of our approach on the number of communities is very low for instances with high modularity. This phenomenon might be explained as follows: to minimize a learnt clause C, our approach has to deduce the empty clause by successively propagating the negation of the literals of C. In an instance with modularity 0.9, the number of communities in C is roughly the number of decisions needed to make C failed. So, Algorithm 2 probably has to propagate the negation of at least one literal in each community of C to deduce the empty clause. Consequently, the reduced clause C ′ probably contains the same number of communities as C.

6 Conclusions

We described a new inprocessing approach to minimize learnt clauses based on applying Boolean constraint propagation to a reduced number of learnt clauses when a restart is triggered under certain conditions, controlled using three functions whose exact definition depends on other techniques in the solver. The approach is simple and can be easily implemented in a CDCL SAT solver. We implemented it in five of the best performing state-of-the-art CDCL solvers, and conducted an empirical evaluation on instances of recent SAT competitions. The results provide evidence of the significance and the robustness of the contributions of this paper. According to Audemard and Simon (2012), we are in front of a new critical feature of SAT solvers, because the proposed approach was able to solve up to 16 additional instance of a same category of the SAT Competition. We believe that future SAT solvers will incorporate our new inprocessing technique.