Weight-Enhanced Diversification in Stochastic Local Search for Satisfiability

1 Introduction

Stochastic Local Search (SLS) for Satisfiability (SAT) has obtained significant progress in recent years through the development of many powerful solvers such as G2WSAT [Li and Huang, 2005], VW2 [Prestwich, 2005], gNovelty+[Pham et al., 2008], TNM [Wei and Li, 2009] , Sparrow [Balint and Fr¨ohlich, 2010], and CCASat [Cai and Su, 2012]. However, their success has been restricted mostly to randomly generated SAT instances. The results from recent SAT competitions 1 reveal that SLS algorithms are unable to match the performance of systematic solvers on large structured problems. These problems are normally highly constrained than randomly generated problems. Consequently, it becomes harder to navigate the search space due to the large numbers of local minima. In other words, SLS solvers can easily get trapped in a local minimum and takes a long time to escape from it.

1 http://www.satcompetition.org

As a result, the search diversification (i.e. its ability to cover different areas in the search space) on these problems is significantly reduced.

A typical approach to improve diversification in local minima is to perform a RandomWalk [McAllester et al., 1997]: randomly select an unsatisfied clause and then flip a random variable in that clause. Recently, Novelty Walk (that uses the Novelty[McAllester et al., 1997] heuristic to select the variable) has become a popular method for improving diversification and so has been integrated in many well-known SAT solvers such as TNM and gNovelty+. It is worthy to note that the way Novelty selects a variable from a randomly selected false clause is different to RandomWalk. By ranking all variables in the clause w.r.t a scoring function, it flips the best variable most of the time but will occasionally flip the second best variable with some noise probability.

In this paper, we introduce new heuristics to improve the effectiveness of Novelty Walk in terms of reducing search stagnation. These heuristics are used to select (i) an unsatisfied clause and then (ii) a variable to be flipped thereof. We use weights (based on statistical information collected during the search) to focus the diversification phase onto specific areas of interest. Our interests in this case are long-term unsatisfied clauses and variables that have been flipped only few times. With a given probability β, we select the most frequently unsatisfied clause instead of a totally random one as Novelty does. Amongst all the variables appearing in the selected clause, we then select the least flipped variable for the next move. By doing this, we intend to explore diverse areas of the search space.

We applied our weight-enhanced diversification heuristics on the ternary chain problem to examine their diversification and trap-escaping capability. We also evaluated our heuristics on benchmarks that are real world industrial problems and have complex structures. Moreover, we compared the performance of our resulting solver with other well-known solvers on the benchmarks used in SAT 2011 competition. Our experimental results show that our new method significantly improves the performance of gNovelty+ and thus outperforms other local search SAT solvers on both structured and random satisfiability benchmarks.

The rest of the paper is organised as follows: Section 2 reviews stochastic local search for SAT, Section 3 describes our weight-enhanced diversification algorithm, Section 4 presents our experimental results and analyses, and lastly Section 5 concludes the paper.

2 Stochastic Local Search for Satisfiability

Most SLS-based SAT solvers operate in two modes: intensification (or greedy) mode and diversification (or trap-escaping) mode. In the intensification mode, they choose the variable with the highest score to get as close to the solution as possible w.r.t. the scoring function. Thus, selecting the right scoring function to be used in the intensification mode is a key performance-controlling factor for SLS-based solvers. Typically, there are two types of scoring functions: non-weighted or weighted versions.

A popular non-weighted scoring function is based on the simple count of currently unsatisfied clauses [McAllester et al., 1997]:

where Cls(c) indicates whether a clause c is false or not under the current assignment. In order words, Cls(c) = 1 if c is currently unsatisfied, otherwise Cls(c) = 0. Similarly, Clsv (c) shows whether clause c remains false if variable v is flipped. Clearly, the score of flipping a variable v is defined as the decrease in the number of unsatisfied clauses after v is flipped. This scoring scheme is used by many SLS solvers such as GSAT [Selman et al., 1992], G2WSAT [Li and Huang, 2005], TNM [Wei and Li, 2009].

Under a weighted scheme, a scoring function can be de-

where Wgh(c) is the weight of a clause c. Examples of modern SLS solvers that use clause-weighted scoring functions are gNovelty+ [Pham et al., 2008], Sparrow [Balint and Fr¨ohlich, 2010], and CCASat [Cai and Su, 2012]).

Alternatively, a weighted scoring function can also be simply defined as

where the weight VarWgh(v) of a variable v is normally defined as the number of times v has been flipped. VW2 [Prestwich, 2005] is the first SLS solver that relies solely on this variable-weighted score to prioritise and select variables.

The diversification mode is activated when a SLS solver reaches a local minimum, i.e. an area where the scoring function becomes meaningless for filtering good potential moves. Therefore, the search cannot proceed in a greedy fashion at a local minimum. Random Walk and Novelty Walk [McAllester et al., 1997] are the two popular choices to help SLS solvers escape from local minima. Additionally, there are other diversification boosting methods such as variable weighting [Prestwich, 2005] or clause weighting [Thornton et al., 2004; Pham et al., 2008], which have been used mostly in variable selection.

The Hybrid [Wei et al., 2008] and TNM [Wei and Li, 2009] algorithms exploit variable weights to regulate two different noise heuristics, but do not directly use these weights in the selection of variables during the diversification phase. Sparrow, the winner of the SAT 2011 competition, uses its own probabilistic scoring function based on wscore. CCASat [Cai and Su, 2012], the winner of the 2012 SAT Challenge, uses the configuration checking concept to restrict the greedy selection of variables. Recently, [Pham et al., 2012; Duong et al., 2012; 2012] introduced the new pseudo-conflict concept to prevent the search from visiting previously encountered local minima.

2.1 gNovelty+

In Algorithm 1, we provide the pseudo-code of gNovelty+ [Pham et al., 2008] to illustrate how a SLS solver switches from its intensification mode to its diversification mode and vice versa. gNovelty+ is a hybrid of PAWS [Thornton et al., 2004] and G2WSAT [Li and Huang, 2005].

In its greedy mode, gNovelty+ selects the most promising variable v to flip [Pham et al., 2008]. 2 Initially, the weights of all clauses are set to 1. If no promising variable can be found, the weights of all unsatisfied clauses will be increased by 1 (Line 13). Within a smoothing probability sp, the weights of all weighted clauses c (i.e. whose Wgh(c) is greater than 1) are decreased by 1 (Line 13) [Pham et al., 2008]. Using this clause-weighted scoring scheme, gNovelty+ always aims to select the variable v that after flipped will lead to the maximum reduction in the weighted sum of all false clauses. In other words, gNovelty+ tends to satisfy clauses that have remained unsatisfied for a long time.

When no promising variable exists, gNovelty+ switches to its diversification mode. In this mode, it invokes WeightedNovelty, a weighted version of Novelty, to help lessen its greediness in selecting variables. As sketched out in Algorithm 2, the set of candidate variables is limited to those that appear in a randomly selected clause c. Note that in Line 3, WeightedNovelty uses the weighted score wscore(v) to rank all variables v in clause c instead of the normal score(v) score

2 A promising variable has its wscore > 0.

Algorithm 2: WeightedNovelty(p)

1 c = randomly select an unsatisfied clause; 2 for all variables in clause c do 3 find the best and second best variables based on wscore, breaking ties in favour of the least recently flipped variable; 4 end 5 if within probability p then 6 return the second best variable; 7 else return the best variable; 8 ;

as the original Novelty does. With probability p, WeightedNovelty will select the second best variable within clause c rather than returning the best one. Note that gNovelty+ only adjusts the clause weights after WeightedNovelty completes its cycle. Once promising variables become available, gNovelty+ will switch back to its intensification mode.

3 Weight-Enhanced Diversification

In most SLS solvers, clause weights are only used for computing wscore and ranking variables. To the best of our knowledge, no SLS solver has used clause weights for selecting clauses in the diversification mode. In fact, their diversification method (which is usually either Random Walk or Novelty Walk) normally selects an unsatisfied clause randomly. Nevertheless, a clause weight records no-good information about how often that clause has been false at local minima. Similarly, a variable weight stores no-good information about how often a variable has been flipped. In its diversification phase, VW1 uses variable weights to break ties beside its scoring function [Prestwich, 2005]. The tiebreaking prefers the variable having the least weight (i.e. the least often flipped variable). In contrast, VW2 uses variable weights to adjust its dynamic scoring function rather than to break ties. This study is motivated by the desire to investigate the use of weighting-based enhancement in the diversification phase. Firstly, we use clause weights to select clauses in the trap escaping phase. Secondly, we use variable weights to break ties in the scoring function. Below we introduce our weight-enhanced heuristics to improve the diversification of SLS solvers, especially gNovelty+.

3.1 Clause-Weighting Enhancement

In the diversification phase, our new heuristic greedily selects an unsatisfied clause based on the clause weights. With probability β, it selects an unsatisfied clauses randomly. Otherwise, with probability (1-β), it selects an unsatisfied clause with the maximum clause weight. The aim of selecting a clause with the highest weight is to make an attempt to satisfy the clause that is most often falsified at a local minimum. Satisfying such a clause may help the search escape from the current trap. The positive aspect of using the diversification noise β is the flexibility in switching back and forth between greediness and randomness. This allows the solver to occasionally move away from being too greedy.

The new NoveltyGC is outlined in Algorithm 3. Notice that Line 1 in Algorithm 2 has been replaced by Lines 1-4 in Algorithm 3. Once the false clause c is selected, the algorithm will compute the wscore(v) to find the best and second

Algorithm 3: NoveltyGC(β, p)

1 if within probability β then 2 c = randomly select an unsatisfied clause; 3 else c = select an unsatisfied clause with the highest clause weightWgh(c); 4 ; 5 for all variables in clause c do 6 find the best and second best variables based on wscore, breaking ties based on a diversification criterion; 7 end 8 if within probability p then 9 return the second best variable; 10 else return the best variable; 11 ;

best variables w.r.t. the score. If two variables have the same score, normally ties are broken by selecting the least recently flipped variable (Line 3 in Algorithm 2). In the next section, we will describe other diversification criteria to break such ties (Line 6 in Algorithm 3).

3.2 Variable-Weighting Enhancement

As mentioned above, Novelty uses variable age as its diversification criterion. A variable age is computed as the number of flips since that variable was last flipped [McAllester et al., 1997]. In other words, the older the variable, the more likely it will be selected. Many SLS solvers (e.g. gNovelty+, PAWS, CCASat, and Sparrow) use variable ages to break ties in their diversification phase.

In this study, we use variable weights as an alternative diversification criterion. In this case, ties are broken by selecting the variable v with less weight VarWgh(v), which records the number of times v has been flipped. By doing so, the algorithm prefers to direct the search to the area that involves the least frequently flipped variables. The use of this kind of variable weights has reportedly improved diversification more than variable ages do [Prestwich, 2005].

Finally, we also investigate the use of both variable weights and variable ages in a combined fashion: break ties by selecting the variable with smaller variable weight, then break further ties by preferring the older variable. It was reported that a selective combination of variable properties (e.g. variable age, different types of scores) can boost the performance of local search solvers that originally use only a single variable property [Tompkins and Hoos, 2010]. However, the drawback of these solvers is that they require appropriate configuration of many parameters.

3.3 Implementation

In order to study the effect of our new weight-enhanced heuristics, we integrated these new changes into gNovelty+. The new algorithm gNovelty+GC (where GC stands for 'greedy clause selection') is illustrated in Algorithm 4. The obvious difference is gNovelty+GC now uses NoveltyGC (Line 12) instead of the old WeightedNovelty heuristic (as in Line 12 in Algorithm 1). In addition, we altered gNovelty+GC in Line 10 so that it will break ties in the intensification phase using the same diversification criterion as NoveltyGCdoes in the diversification phase.

In summary, there are three different diversification criteria: variable age, variable weight, and their combination. In

Algorithm 4: gNovelty+GC(Θ, β, sp)

order to distinguish the three variants of gNovelty+GC, we name them respectively as gNovelty+GCa, gNovelty+GCw, and gNovelty+GCwa based on the diversification criterion being used. However, for space constraints and convenience, we may also denote them by GCa, GCw, and GCwa in the result tables or figures.

4 Experimental Results

We first evaluated the gNovelty+GC variants on ternary chain instances to study their diversification capability over other known algorithms. Afterwards, they were tested on verification benchmarks from real world problems. Finally, to compare with the state of the art results, experiments were run with the SAT 2011 Competition benchmarks and the solvers TNM, VW2, EagleUP [Gableske and Heule, 2011], sattime2011 [Li and Li, 2012], Sparrow and CCASat. Note that Sparrow and CCASat are respectively the winners of SAT competitions in 2011 and 2012 on the random track. Experiments were conducted on Griffith University Gowonda HPC Cluster equipped with a number of Intel(R) Xeon(R) CPUs X5650 @2.67GHz.

4.1 Experiments on Ternary Chains

Ternary chain is an artificial problem that deliberately simulates chains of variable dependencies in structured problems. It is employed to study the diversification capability of local search algorithms in [Prestwich, 2002; Wei and Selman, 2002]. A ternary chain has only one solution where all variables are true. Therefore, flipping any variable from true to false is likely to move away from the solution. For this characteristic, local search algorithms will easily become trapped. The formulation of a ternary chain with N variables is defined as follows:

In this experiment, we compare gNovelty+GC(β = 0.5) against gNovelty+and other popular solvers such as PAWS, VW2, Sparrow and CCASat. The results are depicted in Figure 1. Figure 1(a) shows the success rate of solvers on ternary chains of size [10,100]. Figures 1(b) and 1(c) present the run times (in seconds) taken to solve ternary chains of size [10,100] and [100,1000], respectively. Each solver was ran 100 times on each instance with a timeout of 20 seconds.

As seen in Figure 1, it was apparent that VW2, gNovelty+ and gNovelty+GC performed significantly better than other solvers. gNovelty+ and VW2 solved all ternary chains successfully due to variable weighting and clause weighting. It is very clear from Figure 1 that gNovelty+GCa is actually no different with gNovelty+. However, gNovelty+GCw, which takes advantage of gNovelty+ and VW2, performed better than these two algorithms. Notice that gNovelty+GCwa, being a compromise between gNovelty+GCa and gNovelty+GCw, was slightly better than gNovelty+GCa, but worse than gNovelty+GCw.

4.2 Experiments on Verification Problems

The experiments were conducted on three real world verification problems: cbmc, swv and sss-sat-1.0. The first two instance sets are software verification problems: (i) 39 cbmc instances generated by a bounded model checking tool and (ii) 75 swv instances generated by the CALYSTO checker. 3 The third one is Velev's sss-sat-1.0 which contains 100 instances encoding verification of super-scalar microprocessors. 4 Even though these instance sets can be easily solved by the complete solver PICOSAT [Biere, 2008], they are currently a remarkable challenge for SLS solvers [Tompkins et al., 2011]. The experiments on these datasets were conducted by running the solvers 50 times on each instance with a timeout of 600s.

In Figure 2, we compared gNovelty+GCa with the original gNovelty+ , sattime2011 (being the best SLS solver and ranked 4th overall on crafted instances in the SAT 2011 competition), and Sparrow (being the best solver for random instances in the SAT 2011 competition). As we can see from this figure, gNovelty+GCa performed significantly better than all these three solvers.

The full empirical results are detailed in Table 1 in terms of three criteria: success rates, run times (in seconds), and flip counts (in millions). Data for VW2, Sparrow and CCASat were partially omitted as their flip counters were overflowed. The run times and flip counts for each problem set are the averages of the median data on each instance in that set. In general, our results show that the three gNovelty+GC variants outperformed other solvers in all three criteria. Among these variants, gNovelty+GCw is the best for cbmc and swv. Especially, gNovelty+GCw is five times faster than two other variants on cbmc instances in terms of CPU time. In contrast, gNovelty+GCw was no match to the other two variants on the sss-sat-1.0 dataset. Indeed, it is the worst variant in all three criteria. Although gNovelty+GCwa was not the best solver among three variants in any dataset, it performed very steadily. Overall, it had the best success rate on all three datasets (being 100%, 49% and 99% for cbmc, swv and ssssat-1.0 respectively). Moreover, it achieved reasonable average run time compared to the other solvers.

3 The test instances of cbmc and swc are available at http://people.cs.ubc.ca/davet/papers/sat10-dave-instances.zip

4 http://www.miroslav-velev.com/sat benchmarks.html

4.3 Experiments on SAT2011 Benchmarks

We compared the performance of gNovelty+GC variants against other solvers on the SAT 2011 benchmarks. Each solver was ran 10 times on each instance with a timeout of 600s. The full results are reported in Tables 2 and 3 in terms of success rates, run times (in seconds), and flip counts (in millions). 5 Data for VW2, Sparrow and CCASat were partially omitted as their flip counters were overflowed. The run times and flip counts for each problem set are the averages of the median data on each instance in that set.

5 Because many instances were too hard to solve, we reported only instances that were solved at least once by a tested solver.

We also plotted the run times of gNovelty+GCa against gNovelty+, sattime2011 and Sparrow in Figure 2. As illustrated in that figure, gNovelty+GCa was significantly better over gNovelty+ on both structured and random instances. Moreover, it outperformed Sparrow in both datasets and achieved comparably equal performance with sattime2011.

Overall, Tables 2 and 3 show that all gNovelty+GC variants outperformed gNovelty+, Sparrow and VW2 in all problem sets. However, some variants performed worse than other solvers in terms of success rate on certain datasets. For example, on application instances, gNovelty+GCa and gNovelty+GCwa were on par with TNM and sattime2011 in terms of success rate (25%) and run times. However, they were not as good as CCASat (38%) in terms of success rate. gNovelty+GCw with the success rate of 50% was the best solver on application instances.

On crafted instances, sattime2011 and gNovelty+GCwa had the best success rate (72%), but in terms of CPU time, sattime2011 was better. Furthermore, the other two variants with the success rate of 68% and 67% were considerably better than many other solvers. However, the three best solvers were TNM, sattime2011 and CCASat, whose success rates were respectively 73%, 75%, and 73% on large random instances. The three gNovelty+GC variants only achieved the success rates of 39%, 25% and 23% respectively. On medium random instances, they achieved steadily good results with 100% success rate. In terms of CPU time, all gNovelty+GC

variants were significantly better than the other solvers except TNM and sattime2011.

4.4 Discussions

Table 4 presents the parameter settings for gNovelty+GC variants tuned by ParamILS, a local search optimisation tool for parameterised algorithms [Hutter et al., 2009].

As seen from Table 4, the smooth probability sp of structured instances are very low. For example, on cbmc and ssssat-1.0, it is 0 for all variants, meaning that no clause weight was reduced. In contrast, it has a higher value on SAT 2011 dataset. This means the clause weight smoothing was needed occasionally. The majority of β values is low (≤ 30%), meaning the solvers were more greedy in picking false clauses. This demonstrates the essence of greedy clause selection.

In addition, our weight-based clause selection biases the search towards satisfying clauses that have been unsatisfied more often. This is confirmed when comparing the distribution of clause lengths of the original instance and that of the set of unsatisfied clauses being selected. Using our heuristic, the two distributions are different, but are very similar when selecting clauses randomly. We also found that the distribution of clause lengths over the set of selected clauses is significantly skewed towards unit clauses on SAT2011 application instances in comparison to such distribution on BMC instances. This strong bias gives a hint on why our heuristic is less efficient on application instances.

5 Conclusion And Future work

This paper presented a method to enhance diversification of SLS solvers by leveraging the advantage of clause weights and variable weights. The first contribution of this paper is a technique to balance between greediness and randomness in clause selection at local minima. The second contribution is the employment of variable weights as a diversification criterion in breaking ties. The results on real world structured instances and the SAT 2011 competition datasets showed that significant enhancement was achieved by greedily selecting clauses. Furthermore, our new heuristics which utilise both types of weights significantly boost the performance of gNovelty+ . Another finding of this work is that the gNovelty+GCwa version is a good compromise of gNovelty+GCw and gNovelty+GCa . Based on the analysis of parameter settings, it is recommended that the smoothing probability on gNovelty+GC should have a small value for structured instances but a high value for random instances.

In the future, we plan to investigate adaptation of the diversification factor β as the search progresses. We also intend to apply NoveltyGC on a wide range of SLS solvers.