Learning Rate Based Branching Heuristic for SAT Solvers (Презентации лекций), страница 4

We modified the base solver by replacing the VSIDS branchingheuristic with ERWA. We then created two additional solvers, one with the RSRextension and another with both the RSR and locality extensions. We ran these3 solvers over the entire benchmark and report the number of instances solvedby these solvers within the time limit in Table 1. ERWA solves a total of 1212instances, ERWA with the RSR extension solves a total of 1251 instances, andERWA with the RSR and locality extensions (i.e., LRB) solves a total of 1279instances.

See Figure 1 for a cactus plot of the solving times.BenchmarkStatusSATUNSATBOTHSAT2009 Hard CombinatorialUNSATBOTHSAT2011 ApplicationUNSATBOTHSAT2011 Hard CombinatorialUNSATBOTHSAT2013 ApplicationUNSATBOTHSAT2013 Hard CombinatorialUNSATBOTHSAT2014 ApplicationUNSATBOTHSAT2014 Hard CombinatorialUNSATBOTHSATTOTAL (excluding duplicates) UNSATBOTH2009 ApplicationERWA85122207986516310598203954514012589214113972101118219387731606385741212ERWAERWA+ RSR + Locality+ RSR(LRB)8485120121204206991016869167170105103101982062018893616514915813313295952282271101161081102182261081167777185193929187891791806326546196251251 1279Table 1. Comparison of our extensions to ERWA on the base CDCL solver (MiniSat 2.2with aggressive LBD-based clause deletion). The entries show the number of instancessolved for the given solver and benchmark, the higher the better.6.3Experiment: LRB vs VSIDS vs CHBIn this experiment, we compare LRB with VSIDS [24] and CHB [19].

Our basesolver is MiniSat 2.2 which already implements VSIDS. We then replaced VSIDSin the base solver with LRB and CHB to derive 3 solvers in total, with theonly difference being the branching heuristic. We ran these 3 solvers on theentire benchmark and present the results in Table 2. LRB solves a total of 1279instances, VSIDS solves a total of 1179 instances, and CHB solves a total of 1235instances. See Figure 1 for a cactus plot of the solving times.6.4Experiment: LRB and Learning RateIn this experiment, we measure the efficacy of the 5 branching heuristics fromTable 1 and Table 2 at maximizing the LR.

For each instance in the benchmark,we solve the instance 5 times with the 5 branching heuristics implemented inthe base solver. For each branching heuristic, we track all the observed rewards(i.e., LR) and record the mean observed reward at the end of the run, regardlessif the solver solves the instance or not. We then rank the 5 branching heuristicsby their mean observed reward for that instance. A branching heuristic gets arank of 1 (resp. 5) if it has the highest (resp. lowest) mean observed rewardfor that instance.

For each branching heuristic, we then average its ranks overBenchmarkStatusSAT2009 ApplicationUNSATBOTHSAT2009 Hard CombinatorialUNSATBOTHSAT2011 ApplicationUNSATBOTHSAT2011 Hard CombinatorialUNSATBOTHSAT2013 ApplicationUNSATBOTHSAT2013 Hard CombinatorialUNSATBOTHSAT2014 ApplicationUNSATBOTHSAT2014 Hard CombinatorialUNSATBOTHSATTOTAL (excluding duplicates) UNSATBOTHLRB8512120610169170103982019365158132952271161102261167719391891806546251279VSIDS83125208100661669599194884813612786213115731881059419991591506265531179CHB8911920810367170106962021024714913779216122962181157318890761666735621235Table 2.

Apple-to-apple comparison between branching heuristics (LRB, CHB, andVSIDS) in a version of MiniSat 2.2 with aggressive LBD-based clause deletion. Theentries show the number of instances in the benchmark the given branching heuristicsolves, the higher the better. The LRB version (we dub as MapleSAT), outperformsthe others.the entire benchmark and report these numbers in Table 3. The experimentshows that LRB is the best heuristic in terms of maximizing the reward LR(corresponding to a rank closest to 1) in almost every category.

In addition, theexperiment shows that the RSR and locality extensions increase the observedrewards relative to vanilla ERWA. Somewhat surprisingly, VSIDS and CHB onaverage observe higher rewards (i.e., LR) than ERWA, despite the fact thatVSIDS and CHB are designed without LR as an explicit objective. This perhapspartly explains the effectiveness of those two heuristics.6.5Experiment: LRB vs State-Of-The-Art CDCLIn this experiment, we test how LRB-enchanced CryptoMiniSat competes againstthe state-of-the-art solvers CryptoMiniSat [29], Glucose [4], and Lingeling [6]which all implement VSIDS. We modified CryptoMiniSat 4.5.3 [29] by replacingVSIDS with LRB, leaving all else unmodified. We ran unmodified CryptoMiniSat, Glucose, and Lingeling, along with the LRB-enchanced CryptoMiniSat onthe benchmark and report the results in Table 4.

LRB improved CryptoMiniSaton 6 of the 8 benchmarks and solves 59 more instances overall.BenchmarkStatusSAT2009 ApplicationUNSATBOTHSAT2009 Hard CombinatorialUNSATBOTHSAT2011 ApplicationUNSATBOTHSAT2011 Hard CombinatorialUNSATBOTHSAT2013 ApplicationUNSATBOTHSAT2013 Hard CombinatorialUNSATBOTHSAT2014 ApplicationUNSATBOTHSAT2014 Hard CombinatorialUNSATBOTHSATTOTAL (excluding duplicates) UNSATBOTHLRB2.412.132.252.432.182.332.252.142.202.572.572.572.332.022.192.511.992.242.272.242.252.431.812.112.452.122.28ERWA3.794.164.013.304.183.663.613.823.723.473.723.563.604.163.853.573.923.753.684.344.013.514.383.963.534.083.81ERWA + RSR VSIDS3.422.513.322.903.362.743.033.293.483.223.213.263.022.773.223.493.123.132.983.463.323.543.113.493.162.493.073.393.122.892.913.032.654.262.783.653.212.503.202.823.212.663.032.782.693.822.853.313.102.723.103.413.103.07CHB2.872.492.652.951.942.533.352.332.852.531.852.273.412.372.952.982.182.583.352.402.883.262.302.763.202.302.74Table 3.

The average ranking of observed rewards compared between different branching heuristics in MiniSat 2.2 with aggressive LBD-based clause deletion. The lower thereported number, the better the heuristic is at maximizing the observed reward relativeto the others.5000VSIDSERWACHBERWA + RSRLRB45004000Time (s)35003000250020001500100050000200400600800100012001400# of Solved InstancesFig. 1. A cactus plot of the 5 branching heuristics in MiniSat 2.2 with aggressiveLBD-based clause deletion. The benchmark consists of the 4 most recent SAT Competition benchmarks (2014, 2013, 2011, 2009) including both the application and hardcombinatorial categories, excluding duplicate instances.

A point (x, y) on the plot isinterpretted as: y instances in the benchmark took less than x seconds to solve for thebranching heuristic. The further right and further down, the better.BenchmarkStatusSAT2009 ApplicationUNSATBOTHSAT2009 Hard CombinatorialUNSATBOTHSAT2011 ApplicationUNSATBOTHSAT2011 Hard CombinatorialUNSATBOTHSAT2013 ApplicationUNSATBOTHSAT2013 Hard CombinatorialUNSATBOTHSAT2014 ApplicationUNSATBOTHSAT2014 Hard CombinatorialUNSATBOTHSATTOTAL (excluding duplicates) UNSATBOTHCMS with LRB CMS with VSIDS Glucose858783140143138225230221102959071657017316016010697941221291272282262218686805749441431351241151091041201151112352242151161141151141011062302152211071029911812712022522921989857912210093211185172619598575738700685135712981260Lingeling801412219883181941342288866154100122222114117231101141242891192085897821371Table 4. Apple-to-apple comparison between four state-of-art solvers: CryptoMiniSat(CMS) with LRB heuristic, CMS with VSIDS, Glucose, and Lingeling.

The table showsthe number of instances solved per SAT Competition benchmark, categorized as SATor UNSAT instances. CMS with LRB (we dub as MapleCMS) outperforms CMS withVSIDS, Glucose, and is very close to matching Lingeling.7Related WorkThe Chaff solver introduced the VSIDS branching heuristic in 2001 [24]. Although many branching heuristics have been proposed [16, 7, 28, 15, 22, 17],VSIDS and its variants remain as the dominant branching heuristic employedin modern CDCL SAT solvers. Carvalho and Marques-Silva used rewards basedon learnt clause length and backjump size to improve VSIDS [10].

More precisely, the bump value of VSIDS is increased for short learnt clauses and/or longbackjumps. Their usage of rewards is unrelated to the definition of rewards inthe reinforcement learning and multi-armed bandits context. Lagoudakis andLittman used reinforcement learning to dynamically switch between a fixed setof 7 well-known SAT branching heuristics [18]. Their technique requires offlinetraining on a class of similar instances. Loth et al. used multi-armed banditsfor directing the growth of the search tree for Monte-Carlo Tree Search [21].The rewards are computed based on the relative depth failure of the tree walk.Fröhlich et al. used the UCB algorithm from multi-armed bandits to select thecandidate variables to define the neighborhood of a stochastic local search forthe theory of bitvectors [14]. The rewards they are optimizing is to minimize thenumber of unsatisfied clauses.

Liang et al. also applied ERWA as a branchingheuristic called CHB [19]. As stated earlier, CHB is neither an optimization norlearning algorithm since the rewards are computed on past events.8Conclusions and Future WorkIn this paper, we provide three main contributions, and each has potential forfurther enhancements.Contribution I: We define LR as a metric for the branching heuristic to optimize. LR captures the intuition that the branching heuristic should assignvariables which are likely to generate a high quantity of learnt clauses with noregards to the “quality” those clauses [2].

A new metric that captures qualityshould encourage better clause learning. Or perhaps branching heuristics canbe stated as a multi-objective optimization problem where a good heuristicwould balance the tradeoff between quality and quantity of learnt clauses.Additionally, we would like to stress that the starting point for this researchwas a model of CDCL SAT solvers as an interplay between branching heuristic and clause learning. The branching heuristic guides the search, and hasgreat impact on the clauses that will be learnt during the run of the solver.In the reverse direction, clause learning provides feedback to guide branchingheuristics like VSIDS, CHB, and LRB.