Exponential Recency Weighted Average Branching Heuristic for SAT Solvers (Презентации лекций), страница 3

The first run was with the default unmodified solver (which uses VSIDS as its branching heuristic) and the second run was with a modified version of thesolver using CHB instead of VSIDS. The evaluation compares which solver, unmodified with VSIDS or modifiedwith CHB, solved more instances. Each run was executedon StarExec (Stump, Sutcliffe, and Tinelli 2014), a platformdesigned for evaluating logic solvers. The StarExec platformuses the Intel Xeon CPU E5-2609 at 2.40GHz with 10240KB cache and 24 GB of main memory, running on Red HatEnterprise Linux Workstation release 6.3, and Linux kernel2.6.32-431.1.2.el6.x86 64.The modified solvers changed only the branching heuristic by replacing VSIDS with CHB. We left everything elsein the solvers untouched, and the solvers’ parameters are leftto their defaults.

We made no attempt to tune the solvers’ parameters to work well with CHB. Additionally, the modifiedsolvers reused the existing data structures such as the existing priority queue data structures for finding the variableranked highest by VSIDS/CHB.2013Crafted2014App2014CraftedTOTALSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHMiniSatwith CHB131 (+13.9%)59 (0.0%)190 (+9.2%)106 (0.0%)92 (+48.4%)198 (+17.9%)113 (+27.0%)49 (-12.5%)162 (+11.7%)84 (+15.1%)67 (+52.3%)151 (+29.1%)434 (+13.3%)267 (+20.8%)701 (+16.1%)Table 1: The table presents the number of solved instancesby unmodified MiniSat (with VSIDS) versus MiniSat withCHB on SAT 2013 and 2014 handcrafted and applicationbenchmarks.

Additionally, the difference between the twosolvers is given as a percentage. For example, MiniSat withCHB solves 16.1% more instances than unmodified MiniSatover the entire benchmark.Results: SAT Competition 2013 and 2014First, CHB was evaluated on all 1200 instances from theapplication and hand-crafted categories of the SAT Competition 2013 and 2014 benchmarks. The instances from thehand-crafted category are designed to be challenging forSAT solvers. Each run of a solver was given 5000 secondsand 7.5 GB of memory to solve an instance, as per the rulesof SAT Competition 2013.

Tables 1 and 2 show how CHBsolved more instances on this large benchmark than VSIDS.The results show a big increase in the number of solvedsatisfiable instances in MiniSat and Glucose. MiniSat is avery popular solver, however it has not won any recent SATcompetitions unlike Glucose. Yet MiniSat with the one addition of CHB solved 436 satisfiable instances over the entirebenchmark, considerably more than the 394 solved satisfiable instances by unmodified Glucose (with VSIDS).

CHBsolves more satisfiable instances than VSIDS for both categories and both years. CHB also dramatically increases thenumber of solved unsatisfiable instances by 29 for MiniSat.Glucose with CHB solved 16 more unsatisfiable instances.Figure 1 shows the cactus plot of the running times, astandard diagram in SAT literature for comparing the performance of solvers. Lines further down and to the right onthe plot are better. The plot shows a significant improvementof CHB over VSIDS on the SAT Competition instances.To put this into context, the solver Minsat blbd (Chen2014) won first place in the SAT Competition 2014 by solving the most satisfiable instances in the application trackand Lingeling (Biere 2010) won that track for 2013.

On theStarExec platform, Minsat blbd solved 106 satisfiable instances in the 2014 application track, whereas MiniSat with2013App2013Crafted2014App2014CraftedTOTALSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHSATUNSATBOTHUnmodifiedGlucose103103206113104217991162157989168394412806Glucosewith CHB115 (+11.7%)115 (+11.7%)230 (+11.7%)119 (+5.3%)106 (+1.9%)225 (+3.7%)103 (+4.0%)106 (-8.6%)209 (-2.8%)86 (+8.9%)101 (+13.5%)187 (+11.3%)423 (+7.4%)428 (+3.9%)851 (+5.6%)Table 2: The table presents the number of solved instancesby unmodified Glucose (with VSIDS) versus Glucose withCHB on SAT 2013 and 2014 handcrafted and applicationbenchmarks.

Additionally, the difference between the twosolvers is given as a percentage. For example, Glucose withCHB solves 5.6% more instances than unmodified Glucoseover the entire benchmark.5000MinisatMinisat with CHBGlucoseGlucose with CHB4500400035003000Time (s)2013AppUnmodifiedMiniSat115591741066216889561457344117383221604250020001500100050000100200300400500600700800900# of Solved InstancesFigure 1: Cactus plot of the running times on the SAT Competition 2013 and 2014 benchmarks. A point (x, y) meansthat there are x instances where each one can be solvedwithin y seconds with the given solver.

A line further to theright means the solver solved more instances. A line furtherdown means it solved instances faster.90000Related WorkMinisatMinisat with CHBGlucoseGlucose with CHB8000070000Time (s)600005000040000300002000010000005101520253035# of Solved InstancesFigure 2: Cactus plot of the running times on the stepreduced SHA-1 and MD5 first preimage attacks.

Refer toFigure 1 for an explanation on how to interpret cactus plots.CHB solved 113 instances as noted in Table 1. Likewise forthe 2013 application track, Lingeling solved 122 satisfiableinstances, whereas MiniSat with CHB solved 131 instances.Results: SAT-based CryptanalysisWe also evaluated the CHB branching heuristic over 10 instances each of 21/22/23-step-reduced (resp.

27/28/29-stepreduced) encodings of a first preimage attack on SHA-1(resp. MD5) for a total of 60 instances. SHA-1 and MD5are cryptographic hash functions and are considered preimage resistant. That is, given an output of the hash function,it is believed to be computationally infeasible to computean input that produces that output. In this benchmark, onlya subset of the hash function steps are encoded, as the firstpreimage attack on the whole function is still intractable.Each instance fixed the Boolean variables corresponding tothe hash function’s output to a random value.

The satisfyingassignment of the Boolean variables, corresponding to thehash function’s input, is a message that hashes to the specified output. Hence, the satisfiying assignment produced by aSAT solver is a successful first preimage attack on the stepreduced hash function.Each run of a solver was given 24 hours and 10 GB ofmemory to solve each instance. Figure 2 shows the runningtimes of CHB versus VSIDS in solving the step-reducedSHA-1 and MD5 cryptographic functions. MiniSat withCHB solved 3 more instances of 23-step-reduced SHA-1,and 1 more instance of 28-step-reduced MD5 than unmodified MiniSat (with VSIDS). Glucose with CHB solved 3more instances of 21-step-reduced SHA-1 and 2 more instances of 22-step-reduced SHA-1 than unmodified Glucose(with VSIDS).In conclusion, CHB-enhanced CDCL solvers significantly outperformed VSIDS-based ones on a large, realworld benchmark.Marques-Silva and Sakallah invented the CDCL technique (Marques-Silva and Sakallah 1999), the dominant approach for solving practical SAT problems efficiently.

TheVSIDS branching heuristic, the dominant branching heuristic employed in modern CDCL SAT solvers, was originallyproposed by the authors of the Chaff solver (Moskewicz etal. 2001). Lagoudakis and Littman took 7 well-known SATbranching heuristics (MAXO, MOMS, MAMS, JeroslawWang, UP, GUP, SUP) and used reinforcement learning toswitch between the heuristics dynamically during the run ofthe solver (Lagoudakis and Littman 2001). Their techniquerequires offline training on a class of similar instances.

Thealgorithm proposed in this paper differs in that it learns toselect good variables rather than learning to select a goodbranching heuristic from a fixed-set. Additionally, CHB requires no offline training.Future WorkThe connection between branching heuristics and reinforcement learning opens many new opportunities for future improvements to branching heuristics and SAT solving in general. We detail some of our future work below that buildson the foundation laid by this paper. Modern CDCL SATsolvers maintain lots of state features such as the partial assignment, trail, learnt clause database, saved phases, etc.

Thetechnique proposed in this paper is based on the multi-armedbandit setting, and it can be extended to a full Markov decision process by conditioning the choice of variables on someof the solvers’ state features. More research is needed to finda stateful model that works well in practice by balancing thetrade-off between the gain in information due to states andthe cost of increased model complexity.We modeled our branching heuristic on ERWA, a technique used to solve the bandit problem. However, perhapsa more powerful model will capture both the branchingheuristic and clause learning. It is evident that the branchingheuristic and clause learning drive each other, so a modelcapturing both aspects can lead to algorithms that not onlychoose better branching variables, but also learn higher quality clauses. It is clear that such a model is outside the bandit framework, due to the additional feedback from clauselearning to the branching heuristic in the form of learntclauses.