Understanding VSIDS Branching Heuristics in CDCL SAT solvers (Презентации лекций), страница 4

Likewise, a highmean Spearman implies the average instance has a strong positive correlationbetween VSIDS and TGC rankings.Results and Interpretations. In Table 3 (resp. Table 4), we compare VSIDSand TDC (resp. TEC) rankings. The data shows a strong correlation betweenVSIDS and TDC, in particular, the 0.818 mean Spearman between cVSIDS andTDC is high. The metrics are lower with TEC, but the correlation remainsstrong. mVSIDS has a better mean Spearman with TEC than TDC in the application category. We have also conducted this experiment with non-temporaldegree/eigenvector centrality and the resulting mean Spearman and mean top-kare significantly lower than their temporal counterparts.It is commonly believed that VSIDS focuses on the “most constrained partof the formula” [24], and that this is responsible for its effectiveness.

However,the term “most constrained part of the formula” has previously not been welldefined in a mathematically precise manner. One intuitive way to define theconstrainedness of a variable is to analyze the Boolean formula, and count howmany clauses a variable occurs in. The variables can then be ranked based onthis measure. In fact, this measure is the basis of the branching heuristic calledDLIS [33], and was once the dominant branching heuristic in SAT solvers. Weshow that graph centrality measures are a good way of mathematically definingthis intuitive notion of syntactic “constrainedness of variables” that has beenused by the designers of branching heuristics.

Degree centrality of a vertex inthe VIG is indeed equal to the number of clauses it belongs to, hence it is a goodbasis for guessing the constrained variables for the same reason. Eigenvectorcentrality extends this intuition by further increasing the ranks of variables closein proximity to other constrained variables in the VIG. Additionally, as thedynamic structure of the VIG evolves due to the addition of learnt clauses bythe solver, the most highly constrained variables in a given instance also changeover time. Hence we incorporated learnt clauses and temporal information intothe TVIG to account for changes in variables’ constrainedness over time.Besides the success of branching heuristics like VSIDS and DLIS, there isadditional evidence that the syntactic structure is important for making goodbranching decisions.

For example, Iser et al. discovered that initializing theVSIDS activity based on information computed on the abstract syntax tree oftheir translator has a positive impact on solving time [27]. In a different paper [38], the authors have shown that the graph-theoretic community structurestrongly influences the running time of CDCL SAT solvers. This is more evidenceof how CDCL SAT solver performance is influenced by syntactic graph properties of input formulas. Finally, by combining the results of this section withContribution I, we conclude that VSIDS picks high-centrality bridge variables.5Contribution IV: Exponential Moving Average andMultiplicative DecayIn this section, we argue that the multiplicative decay aspect of the VSIDSbranching heuristic is a form of exponential moving average (EMA) [11].

It isthe inclusion of multiplicative decay in VSIDS that gives it its distinctive featureof focusing its search based on recent conflicts. The original Chaff paper [36] andpatent [35] rather cryptically mentioned that VSIDS acts like a “low-pass filter”.They do not specify what signals are being fed to this filter, and why the highfrequency components are being filtered out and discarded.In his paper [8], Armin Biere was perhaps the first to articulate the idea thatadditive bumping of variable scores can be viewed as a signal (a square wave,to be more precise) over the run of the solver.

More precisely, at every timestep, the signal of a variable is 1 if it is bumped, orP0 otherwise. Armin Bierenformalized normalized VSIDS [8] as sn = (1 − f ) × k=1 δk × f n−k . sn is thenormalized VSIDS activity of a variable v after the nth conflict. δk = 1 if variablev was bumped in the k th conflict, otherwise δk = 0. f is the decay factor.While Huang et al.

[26] referred to VSIDS as an EMA, we will show this explicitly. We not only characterize VSIDS as an EMA explicitly, but also describewhy this is crucial to the effectiveness of VSIDS as a branching heuristic. In thenext section we leverage this connection between EMA and VSIDS to proposean adaptive VSIDS branching heuristic inspired by an adaptive version of EMA.EMA is a form of exponential smoothing, used in getting rid of noise (variables whose VSIDS scores are akin to high-frequency signals) in time series data(the signals due to VSIDS scores). Exponential smoothing is a class of techniques to mitigate the effect of random noise in time series data for the purposeof analysis and forecasting.

Armin Biere’s normalized VSIDS equation can berewritten to the following recursive formula: sn = (1 − f ) × δn + f × sn−1 . Thisformula fits exactly the definition of Brown’s simple exponential smoothing, alsoknown as exponential moving average. Therefore normalized VSIDS is exactlyan EMA over the δ time series. The EMA causes VSIDS to favor variables that“persistently” occur in “recent” conflicts.

A rationale why this is effective couldbe as follows: A conflict essentially points to faulty judgment by the solver inassigning values to variables. If a set of variables are at the root of a faulty judgment and thus occurs in a conflict, then they would repeatedly occur in relatedfaulty judgments and hence in related conflicts. Variables that occur persistentlyin “recent” conflicts could be a good guess for the root cause of those conflicts.Hence, perhaps the most effective search strategy is to focus on determining thisroot cause. The learnt clauses that result from such a strategy improve in qualitywith time, until such time that the root cause of a set of faulty judgment hasbeen determined and enshrined as a learnt clause.6Contribution V: A Faster Branching Heuristic BasedOn Adaptive Moving AverageIn this section, we report on our design of a better VSIDS based on the knowledgethat VSIDS decay is a form of EMA. The EMA is integral to VSIDS performanceas a branching heuristic, and now that the connection between EMA and VSIDSis established, all the literature on EMA and other time series data analysis aredirectly applicable to VSIDS.Adaptive Moving Average.

Given that VSIDS decay is a form of EMA, westudied the literature of EMA from the financial domain [31], where it is knownthat the fixed decay factor can be undesirable. A moving average with a largedecay factor would lag behind fast moving markets whereas a small decay factorwould fail to smooth out a lot of noise. Kaufman [31] noted that a fixed decayfactor performs poorly when the market volatility changes.

He devised adaptivemoving average where the decay factor (also known as smoothing constant) isdetermined by the market volatility to minimise lag and noise. By fluctuatingthe decay factor when necessary, adaptive moving average is better than EMAat uncovering trends in the market.Just like how markets can go up and down, a CDCL SAT solver can go upand down in “productivity” over time. For example, Audemard and Simon [6]discovered that a learnt clause with lower literals blocks distance (LBD) [6] isof higher quality. LBD of a clause is defined to be the number of decision levels that its variables span.

If the solver is in a search space that produces manylearnt clauses with low LBD, then we want to encourage the solver to stay withinthat search space. We do so by adjusting the VSIDS decay factor to be closerto 1, i.e., decay slower. On the other hand, if the solver is in a search spacethat produces many learnt clauses with high LBD, it is best to choose a smallerdecay factor, i.e., decay faster.

Based on this insight, we devised a new VSIDSheuristic called adaptVSIDS by extending mVSIDS with an adaptive movingaverage. adaptVSIDS maintains a floating-point number lbdema equal to theexponential moving average of the learnt clause LBDs. lbdema is updated afterevery learnt clause and this number will be used to adjust the decay factor of thevariables’ activities. In mVSIDS, the variables’ activities are decayed by multiplying with a constant decay factor, typically 0.95, after each conflict. Whereasin adaptVSIDS, the decay factor is adjusted based on the LBD of the learntclause. If the LBD of the learnt clause is greater than lbdema, then use a decayfactor of 0.75, otherwise use a decay factor of 0.99. Our website has all the code.Experimental Setup and Methodology. The experiments were performedon the application and combinatorial categories of the SAT Competition 2013.For each instance with a timeout of 5000 seconds as per competition rules, we ranan unmodified MiniSAT 2.2.0 and a modified MiniSAT 2.2.0 with adaptVSIDSon StarExec [1].Results and Interpretations.

Our adaptVSIDS solved 351 instances whereasmVSIDS solved 343 instances, an increase of 2.4% more solved instances.7Interpretation of ResultsWe began our research by posing a series of questions regarding VSIDS, and wenow interpret the results obtained in light of these questions.What is special about the class of variables that VSIDS chooses to additively bump? (Answered by Contributions I and III.) In the bridge variablesexperiment (Section 3), we showed that VSIDS disproportionately favored bridgevariables.