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

We focus on two of the more well-known variants of VSIDS, namely,the variant from Chaff [36] and the variant from MiniSAT version 2.2.0 [15]. Werefer to these variants as cVSIDS and mVSIDS respectively. Both variants havethe common characteristics listed below.Activity Score, Initialization and VSIDS Ranking. VSIDS assigns a floating point number, called activity, to each variable in the Boolean formula.

Atthe begining of a run of a solver, the activity scores of all variables are typicallyinitialized to 0. We refer to the ranking of variables according to their activityscores in the decreasing order as the VSIDS ranking. VSIDS picks the variablewith the highest activity to branch on.Additive Bump and Multiplicative Decay. When the solver learns a clause,a set of variables is chosen, and their activities are additively increased, typicallyby 1.

The quantum of this increase is called the (additive) bump. At regularintervals during the run of the solver, the activities of all variables are multipliedby a constant 0 < α < 1 called the (multiplicative) decay factor.cVSIDS. The activities of variables occurring in the newest learnt clause arebumped up by 1, immediately after the clause is learnt. The activities of allvariables are multiplied by a constant 0 < α < 1. The decay occurs after every iconflicts. We follow the policy used in recent solvers like MiniSAT and use i = 1.mVSIDS.

The activities of all variables resolved during conflict analysis thatlead to the learnt clause (including the variables in the learnt clause) are bumpedup by 1. The activities of all variables are decayed as in cVSIDS 2 .Variable Incidence Graph (VIG). The VIG of a CNF formula F is definedas follows: vertices of the graph are the variables in the formula.

For every clausec ∈ F we have an edge between each pair of variables in c. In other words, eachclause corresponds to a clique between its variables. The weight of an edge is1|c|−1 where |c| is the length of the clause. VIG does not distinguish betweenpositive and negative occurrences of variables. We combine all edges betweeneach pair of vertices into one weighted edge by summing the weights. Moreprecisely, the VIG of a CNF formula F is a weighted graph defined as follows:set of vertices V =PV ar, set of1 edges E = {xy | x, y ∈ c ∈ F }, and the weightfunction w(xy) = x,y∈c∈F |c|−1.3Contribution I and II: Community-focused Search,Bridge Variables, and VSIDSIn this section, we describe the experimental setup, methodology, and results toshow the connection between VSIDS and community structure.The Hypotheses. Here we state the three hypotheses that we tested in thissection: 1) Bridge Experiment: VSIDS disproportionately picks, bumps, andlearns the bridge variables, 2) Spatial Focus Experiment: VSIDS disproportionately picks from a smaller number of communities rather than a large fraction2MiniSAT’s actual implementation is slightly different, but has the same effect.

Ratherthan decaying the activities of every variable, it increases the bump quantum of allfuture conflicts instead [8].of the communities of a SAT instance, and 3) Temporal Focus Experiment:VSIDS typically picks from recently-seen communities.Community Structure of the Graph of SAT Instances, and BridgeVariables. The concept of decomposing graphs into natural communities [13, 43]arose in the study of complex networks such as the graph of biological systems.Informally, a network or graph is said to have community structure if the graphcan be decomposed into sub-graphs where the sub-graphs have more internaledges than outgoing edges [38]. We say that a graph has a “good” communitystructure if the percentage of intra-community edges is significantly higher thaninter-community edges. We refer to these inter-community edges as bridges, andthe vertices connected by such edges as bridge vertices.

In the context of thecommunity structure of the VIG of a Boolean formula, bridge vertices are calledbridge variables. We refer the reader to these papers [13, 43] for a more formalintroduction to community structure of graphs.Recently there has been some interesting discoveries regarding the impact ofcommunity on CDCL SAT solver performance [38].

Specifically, the authors ofthe paper [38] showed that the running time of CDCL solvers is strongly correlated with community structures of SAT instances. In light of these discoveries,it was but natural for us ask the question whether VSIDS somehow exploits thecommunity structure of SAT instances. What we discovered and explain belowis that VSIDS disproportionately picks, bumps, and learns the bridge variablesin the community structure of SAT instances.Temporal and Spatial Focused Search. We further define two terms, spatial focus and temporal focus, to describe how a branching heuristic gravitatestowards certain regions of the search space during solving, with respect to theunderlying community structure.

We say a branching heuristic is spatially focused if it disproportionately picks variables from a small set of communities,when normalized for size, throughout the entire run of the solver. A branchingheuristic exhibits temporal focus if it typically picks a new decision variable froma small fixed-size window of recently-seen communities.Experimental Setup and Methodology. Experiments were performed overthe 1030 instances from SAT Competition 2013 [3], after simplification usingMiniSAT simplifying-solver. We use the Louvain method [10] to compute thecommunities of the VIG of the input SAT formulas. There are many communitydetecting algorithms to choose from and we picked Louvain because it scales wellwith the size of input graphs.

For each instance, the Louvain method is given anhour to compute and save the communities it finds. The community informationis then given to a modified MiniSAT 2.2.0 so it can track the bridge variables.Due to the high cost, we only compute the communities once at the start.For the Bridge-Experiment, we ran the instances using a modified MiniSATwith a timeout of 5000 seconds, as per the SAT Competition 2013 rules. BeforeMiniSAT begins its CDCL loop, it reads in the community information storedby the Louvain method. The solver then scans through its the initial inputclauses and checks which variables share at least one clause with another variableresiding in a different community and marks them as bridge variables. Wheneverour modified version of MiniSAT 1) picks a decision variable, 2) bumps a variable,and 3) learns a clause over a variable during the search, it checks whether thevariable is a bridge variable.

If so, the solver updates its internal counters tokeep track of the number of bridge variables in the each of the 3 scenarios.At the end of the run, the solver outputs the percentage of variables that arebridge in each of these scenarios. This additional code adds little overhead anddoes not change the behavior of MiniSAT. We are simply instrumenting thesolver to collect statistics of interest. For the Temporal-Experiment and SpatialExperiment, we additionally modified MiniSAT to record all decision variablesto a file, in order to post-process the data. We allowed a 10000 second timeoutfor these experiments due to this additional overhead.The Reporting of Results. In the Bridge-Experiment, for each instance, wecompute the percentage of decision variables, bumped variables, learnt clausevariables, and number of variables that are also bridges.

Then we averaged thesepercentages over the three SAT 2013 Competition benchmark categories (application, combinatorial, and random) and reported these numbers.For the Spatial-Experiment, for every community i, we compute a community score csi = picks f rom(i)/order(i), where picks f rom(i) is the numberof times the solver branched on a variable from community i and order(i)is the size of community i in terms of variables. We then use the Gini coefficient [20], a statistical measure of inequality, to compute our spatial scoress = gini(csi for i ∈ communities). A score of 1 indicates total disparity (e.g.all picks are from one community), whereas zero indicates total equality. Higherscores therefore favor our hypothesis.

We report the average ss value for eachbenchmark category. The intuition behind this experiment and the use of theGini coefficient here (used in measuring the inequality of wealth distributionin countries) is that it is an effective method for computing how unequally abranching heuristic favors some communities over others. Using this metric weshow for example that VSIDS disproportionately favors a small set of communities (highly unequal distribution of picks) versus random branching heuristic(largely equal distribution of picks).For the Temporal-Experiment, we define our window size ws to be 10% ofthe total number of communities, rounded up to the nearest integer.