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

For allinstances, our window contains the set of communities from the ws most recentdecisions (note that the set may have less than ws elements). At every decision,we increment a counter window hits if the current variable is from a communityin the window. We assign a temporal score ts = window hits/decisions foreach instance.

We report the average ts value for each benchmark category. Thekey idea behind this experiment is to test the hypothesis that VSIDS branchingfavors picking from recently picked-from communities, versus random which doesnot display such temporal locality.Results and Interpretations of Bridge Variable Experiment. Table 1shows that bridge variables are highly favored in MiniSAT by its branchingheuristic, conflict analysis, and clause-learning. It is a surprising result thatbridge variables are favored even though the heuristics and techniques in Min-CategoryApplicationCombinatorial% ofvariablesthat are bridge61.078.2% ofpicked variablesthat are bridge79.987.6% ofbumped variablesthat are bridge71.684.3% oflearnt clause variablesthat are bridge78.488.2Table 1: MiniSAT’s CDCL and mVSIDS techniques prefers to pick, bump, andlearn over bridge variables.CategorymVSIDS cVSIDSApplication0.5920.560Combinatorial 0.2750.261Random0.0290.023random0.2160.0990.006CategorymVSIDS cVSIDSApplication0.5800.551Combinatorial 0.5050.473Random0.2690.268random0.2680.2650.219(a) Spatial-Experiment average ss score.

(b) Temporal-Experiment average ts score.Table 2: (a) VSIDS heuristics are more spatially focused than random branching.(b) VSIDS heuristics tend to pick from recently-picked communities.iSAT have no notion of communities. While bridge variables certainly make upa large percent of variables, the percent of picked bridge variables is even higher.Table 1 includes only the instances where the Louvain implementation completedbefore timing out.

In total, 229/300 instances in the application category and238/300 instances in the hard combinatorial category are included in the Table 1.In the random category, every variable is a bridge, hence the results are omitted.This is expected because it is highly improbable to generate random instanceswhere a variable is not neighboring another variable outside its community.Recent research suggests that CDCL solvers take advantage of good community structure in SAT instances [38] leading to faster solving time. The reason forthis phenomenon is not fully understood. One possibility is that good community structure lends itself to divide-and-conquer because the bridges are easier tocut (i.e., satisfy).

More precisely, the solver can focus its attention on the bridgesby picking the bridge variables and assigning them appropriate values. When iteventually assigns the correct values to enough bridges, the VIG is divided intomultiple components, and each component can be solved with no interferencefrom each other. Even if the VIG cannot be completely separated, it may stillbe beneficial to the cut bridges between communities so that these communitiescan be solved relatively independently.Results and Interpretations of Temporal and Spatial Focused SearchExperiments.

Table 2a depicts the average Gini coefficient for the SpatialExperiment. Both VSIDS techniques exhibit much more inequality relative torandom branching for the application and combinatorial instances, indicatingthat VSIDS may be attempting to hone in on certain communities. The verylow values for random instances indicate that none of the branching heuristicstypically favor certain communities, likely due to the poor community structuresexhibited by such instances.

Table 2b demonstrates that VSIDS techniques aremuch more temporally focused on average than random branching. It is commonly believed that VSIDS improves the search locality [32, 37] which in turnimproves solver performance. However, this term search locality has previouslybeen not rigorously defined. We precisely defined spatial focus and temporalfocus, and show that VSIDS displays high search locality in terms of these definitions.4Contribution III: Experimental Evidence SupportingStrong Correlation Between TGC and VSIDSIn this section, we describe the experiments to support the hypothesis that theVSIDS variants cVSIDS and mVSIDS, viewed as ranking functions, correlatestrongly with both temporal degree centrality and temporal eigenvector centrality according to Spearman’s rank correlation coefficient and top-k measures.Combining the results of this section with Contribution I (namely, VSIDS picks,bumps and learns over bridge variables), we conclude that VSIDS picks highcentrality bridge variables.Temporal Variable Incidence Graph (TVIG).

To incorporate the temporalaspect of learnt clauses we introduce temporal variable incidence graph (TVIG)here, that extends the VIG by encoding temporal information into its structure.In the TVIG, every clause is labeled with a timestamp denoted t(c). The t(c) isequal to 0 if c is a clause from the original input formula, otherwise t(c) is equalto the number conflicts up to the learning of c.

We refer to the difference betweenthe current time t and the timestamp of a clause t(c) as the age of the clause:age(c) = t − t(c). Fix an exponential smoothing factor 0 < α < 1. The TVIG isa weighted graph constructed in the same manner as the VIG except the weightage(e)of an edge is α|c|−1 . Like the VIG, multiple edges between a pair of vertices arecombined into one weighted edge. More precisely, the TVIG of a clause databaseat time t is defined in the same way as VIG except with a modified weightPage(c)function that takes the ages of clauses into account: w(xy) = x,y∈c∈F α|c|−1 .Observe that the TVIG evolves throughout the solving process: as new learntclauses are added, new edges are added to the graph, and all the ages increase.As an edge’s age increases, its weight decreases exponentially with time assumingno new learnt clause contains its variables.

In many domains, it is often the casethat more recent data points are more useful than older data points.(Temporal) Degree and Eigenvector Centrality. A graph centrality measure is a function that assigns a real number to each vertex in a graph. The number associated with each vertex denotes its relative importance in the graph [19,16, 41]. For example, the degree centrality [16] of a vertex in a graph is defined as the degree of the vertex. The eigenvector centrality of a vertex in agraph is defined as its corresponding value in the eigenvector of the greatesteigenvalue of the graph’s adjacency matrix. We similarly define the temporalversions of degree and eigenvector centrality. The key idea needed to define temporal graph centrality measures is to incorporate temporal information insidethe TVIG.

The temporal degree centrality (TDC) and (resp. temporal eigenvector centrality (TEC)) of a vertex at time t is defined as the degree centrality(resp. eigenvector centrality) of the vertex in the TVIG at time t.Experimental Setup and Methodology. We implemented the VSIDS variants and TGC measures in MiniSAT 2.2.0 [15].

All the experiments were performed using MiniSAT on all 1030 Boolean formulas obtained from all threecategories (application, combinatorial, and random) of the SAT Competition2013 [3]. Before beginning any experimentation, the instances are first simplifiedusing MiniSAT’s inbuilt preprocessor with the default settings. All experimentswere performed on the SHARCNET cloud [4], where cores range in specs between 2.2 to 2.7 GHz with 4 GB of memory, and 4 hour timeout. We use 100iterations of the power iteration algorithm [23] to compute TEC, and 1 iterationfor TDC. We use MiniSAT’s default decay factor of 0.95 for VSIDS.

We also use0.95 as the exponential smoothing factor for the TVIG. We take measurementson the current state of the solver after every 5000 iterations, where an iterationis defined as a decision or a conflict. Observe that we take measurements dynamically as the solver solves an instance, and not just once at the beginning.

Sucha dynamic comparison gives us a much better picture of the correlation betweentwo different ranking functions or measures than a single point of comparison.Methodology for Comparing Rankings based on Spearman’s RankCorrelation Coefficient. For each set of experiments, for each SAT instance,for every measurement made, we compute the Spearman’s rank correlation coefficient [40] between the VSIDS and TGC rankings.

Spearman’s rank correlationcoefficient is a widely-used correlation coefficient in statistics for measuring thedegree of relationship between a pair of rankings. The strength of Spearman’scorrelation is conventionally interpreted as follows: 0.00–0.19 is very weak, 0.20–0.39 is weak, 0.40–0.59 is moderate, 0.60–0.79 is strong, 0.80–1.00 is very strong.We compute the average of the Spearman’s correlation over the execution of aSAT solver on each instance. We follow the standard practice of applying theFisher transformation [17] when aggregating the correlations.Methodology for Comparing Rankings based on Top-k.

Let v be theunassigned variable with the highest ranked according to some VSIDS variant.Let i be the position of variable v according to a specific TGC ranking, excluding assigned variables. Then the top-k measure is 1 if i ≤ k, otherwise 0.The rationale for this metric is that SAT solvers typically only choose the topranked unassigned variable, according to the VSIDS ranking, to branch on. Ifthe VSIDS top-ranked unassigned variable occurs very often among the top-kranked variables according to TGC, then we infer that VSIDS picks variablesthat are highly ranked according to TGC. In our experiments, we used variousvalues for k.

Again, we compute the average of top-k measure over the executionof a SAT solver on each instance.The Reporting of Results. For every pair of rankings, one from the VSIDSfamily and the other from the TGC family, we report the top-k measure andSpearman’s rank correlation coefficient between the pair of rankings every 5000iterations. On termination, we compute the average for the instance. We take allthe instance averages and average them again, and report the average of the averages.

The final numbers are labeled as “mean top-k” or “mean Spearman”. Forexample, a mean top-10 of 0.912 is interpreted as “for the average instance in thecVSIDS vs TDCmVSIDS vs TDCApplication Combinatorial Random Application Combinatorial RandomMean Spearman0.8180.9460.9880.6290.7910.864Mean Top-10.8840.8650.9490.4270.3910.469Mean Top-100.9120.8980.9810.7050.7350.867Table 3: Results of comparing VSIDS and TDC.cVSIDS vs TECmVSIDS vs TECApplication Combinatorial Random Application Combinatorial RandomMean Spearman0.7900.9260.9870.6750.7640.863Mean Top-10.4700.5260.7940.2930.3040.418Mean Top-100.6930.7460.9570.6100.6700.856Table 4: Results of comparing VSIDS and TEC.experiment, 91.2% of the measured top-ranked variables according to VSIDS areamong the 10 unassigned variables with the highest centrality”.