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

A decade and a half after it was initially proposed, VSIDS and its variants continue to be the dominantbranching heuristics among competitive SAT solvers suchas Glucose (Audemard and Simon 2009a), Lingeling (Biere2010), and CryptoMiniSat (Soos 2010).The VSIDS Branching HeuristicAll branching heuristics can be characterized as rankingfunctions that maintain a map from variables in an inputformula to floating point numbers. Abstractly speaking, thebranching heuristic maintains this map in decreasing orderof values assigned to the variables. The VSIDS branchingheuristic maintains a floating point number, often called activity, for each Boolean variable.

Whenever a learnt clauseis added to the clause database by the CDCL SAT solver,the activities of all the variables present in the learnt clauseare dynamically incremented by 1, also called the bump.The activities of all variables are periodically multiplied bya floating point constant between 0 and 1, also called thedecay. Modern variations of VSIDS typically bump all variables present in the clauses used by conflict analysis, notjust the learnt clause variables, and decay after every conflict (Sorensson and Een 2005). VSIDS picks the unassignedvariable with the highest activity to branch on.Exponential Recency Weighted Average (ERWA)Exponential recency weighted average (ERWA) is a simpletechnique to estimate a moving average incrementally bygiving more weight to the more recent outcomes.

Considera stream of outcomes x1 , x2 , x3 , ..., xn . We can compute anexponentially decaying weighted average of the outcomeswith Equation 1.x̄n =nXwi xi where wi = α(1 − α)n−i(1)i=1Here α ∈ [0, 1] is a factor that determines the rate at whichthe weights decay.

To reduce the computational overhead,the moving average can be computed incrementally by updating with Equation 2 after each outcome.x̄n+1 = (1 − α)x̄n + αxn+1(2)ERWA has been used in the context of bandit problems (i.e., single state reinforcement learning problems) toestimate the expected reward of different actions in nonstationary environments (Sutton and Barto 1998). In banditproblems, there is a set of arms (or actions) and the agentmust select which arm to play at each time step in order tomaximize its long term expected reward. Since it does notknow the distribution of rewards for each arm, it faces an important exploration/exploitation tradeoff.

It needs to exploreby trying each arm in order to estimate the expected rewardof each arm and it needs to exploit by selecting arms withhigh expected reward. ERWA is a simple technique to estimate the empirical average of each arm. In the context of thebranching heuristic we propose in this paper, we use ERWAto estimate the moving average of the “score” of each variable in the input formulas, in an online and dynamic fashion,during the entire run of the solver. Inspired by the banditframework, we treat each variable as an arm and estimate ascore for each variable that reflects the frequency and persistence of the variable in generating conflicts in the past.The CHB Branching HeuristicIn this section, we describe our branching heuristic CHB inthe context of a CDCL solver. Algorithm 1 shows the pseudocode of a simple CDCL solver with CHB as the branching heuristic, and we will refer to the line numbers of thisalgorithm where relevant.

CHB maintains a floating pointnumber for each Boolean variable called the Q score, initialized to 0 at the start of the search. Whenever a variablev is branched on, propagated, or asserted, the Q score is updated using Equation 3 (line 18) where α is the step-size andrv is the reward value.Q[v] = (1 − α)Q[v] + αrv(3)As is typical with exponential recency weighted average,the step-size decreases over time (Sutton and Barto 1998).The step-size is initialized to α = 0.4 at the start of thesearch and decreases by 10−6 every conflict to a minimum of0.06, and stays there for the run of the solver (line 26).

Notethat the Glucose solver implements a similar idea, where thedecay factor used by VSIDS decreases over time (Audemardand Simon 2013).rv is the reward value, just as in the bandit problem. Alow (resp. high) reward value decreases (resp. increases) thelikelihood of picking v to branch on.

The reward value isbased on how recently variable v appeared in conflict analysis. Let numConf licts be an integer variable that keepstrack of how many conflicts have occured so far (line 21) andlastConf lict be a mapping from each variable to an integer.Initally, lastConf lict[v] = 0 for each variable v. Whenever a variable x is present in the clauses used by conflictanalysis, lastConf lict is updated by lastConf lict[x] =numConf licts (line 34).

The reward value used by CHB isdefined in Equation 4 (line 17).rv =multipliernumConf licts − lastConf lict[v] + 1(4)Here, multiplier is either 1.0 or 0.9. If branching, propagating, or asserting the variable that triggered the update of Q encounters a conflict after propagation, thenmultiplier = 1.0 (line 12). Otherwise, multiplier = 0.9(line 14).The intuition of the reward value is similar to the intuition of VSIDS, that is to favor variables that appear recently in conflict analysis (Audemard and Simon 2009b).Additionally, the multiplier gives extra reward for producing a conflict. Based on our experience, this reward function gives good performance for CHB in practice. Empirically we have some unpublished evidence that, all else being equal, branching heuristics that have higher rate of conflict clause generation per unit time are more effective thanones that have lower rate.

Leveraging this observation, wedesigned the reward function to maximize the rate of learntclause generation per unit time.During branching, CHB selects the greediest play possible by branching on the unassigned variable v with thehighest Q score (line 42). The algorithm always exploitsand this does not appear to be an issue in practice sincethe problem itself forces exploration in two ways. First, ifthe algorithm greedily branches on variable v, then it cannotbranch on v again until the solver undoes v through backtracking/restarting since v is now assigned and the algorithmis only allowed to branch on unassigned variables.

Hencethe algorithm is forced to branch on other variables. Second,the propagated variables also have their Q scores updated.Hence variables with low Q scores that will not be pickedfor branching can still have their Q scores updated.Differences Between CHB and VSIDSThere are several major differences between the CHB andVSIDS branching heuristics. First, VSIDS only updates theactivities on each conflict, whereas CHB updates the QAlgorithm 1 a simple CDCL solver with CHB as thebranching heuristic.1: α ← 0.42: numConf licts ← 03: plays ← ∅4: for v ∈ V ars do5:lastConf lict[v] ← 06:Q[v] ← 07: end for8: loop9:Boolean constraint propagation10:plays ← plays ∪ {variables propagated just now}11:if a clause is in conflict then12:multiplier ← 1.013:else14:multiplier ← 0.915:end if16:for v ∈ plays domultiplier17:reward ← numConf licts−lastConflict[v]+118:Q[v] ← (1 − α) × Q[v] + α × reward19:end for20:if a clause is in conflict then21:numConf licts ← numConf licts + 122:if decisionLevel == 0 then23:return UNSAT24:end if25:if α > 0.06 then26:α ← α − 10−627:end if28:conflict analysis and learn a new clause29:c ← {variables in conflict analysis}30:u ← the first UIP of the learnt clause31:non-chron.

backtrack based on conflict analysis32:assert variable u based on new learnt clause33:for v ∈ c do34:lastConf lict[v] ← numConf licts35:end for36:plays ← {u}37:else38:if no more unassigned variables then39:return SAT40:end if41:unassigned ← {unassigned variables}42:v ∗ ← argmaxv∈unassigned Q[v]43:assign v ∗ to true or false based on polarityheuristic such as phase saving44:plays ← {v ∗ }45:end if46: end loopscores whenever a variable is branched on, propagated, orasserted.

Additionally, VSIDS decays the activities of allvariables whereas CHB again only decays the Q scores ofbranched, propagated, and asserted variables. The rewardvalues (or bump values) in CHB are variable, whereas thesevalues are constant in VSIDS. Also, the reward value inCHB is based on the conflict history whereas the bump valuein VSIDS is determined by just the current conflict. Lastly,CHB is based on a known algorithm from reinforcementlearning, thus giving us a basis for modeling and understanding branching heuristics.EvaluationThis section describes our experimental evaluation of thepractical performance of CHB versus VSIDS.Choice of SAT SolversCHB was evaluated on 2 notable CDCL SAT solvers: MiniSat version 2.2.0 (Sorensson and Een 2005) and Glucoseversion 4.0 (Audemard and Simon 2009a). MiniSat is apopular CDCL SAT solver, which many other competitivesolvers use as their basis.

Additionally, it contains very fewfeatures, thus isolating the effects of the change in branching heuristics in our experiments. We used the core versionof MiniSat which does not perform simplifications otherthan removing satisfied clauses. Glucose is a state-of-the-artCDCL SAT solver, and a winner of numerous SAT competitions. The two solvers in our evaluation gave us a comprehensive perspective of the effects of the CHB branchingheuristic: on the one hand, we evaluated the effects of CHBon a very simple CDCL solver to isolate its effects, and onthe other hand, a modern competitive solver to understandhow CHB competes with state-of-the-art. Note that MiniSatand Glucose implement variations of VSIDS as their branching heuristics.MethodologyFor each solver-instance pair, we ran the solver on the SATinstance twice.