Understanding VSIDS Branching Heuristics in CDCL SAT solvers (1185838), страница 5
Текст из файла (страница 5)
Even though SAT instances have large number of bridge variables onaverage, the frequency with which VSIDS picks, bumps, and learns bridge variables is much higher. There is no a priori reason to believe that VSIDS wouldbehave like this. This surprising result, plus a previous result that good community structure correlates with faster solving time [38], suggests CDCL solversexploit community structure.
More precisely, they target variables linking distinct communities, possibly as a way to solve by divide-and-conquer approach.In the VSIDS vs. TGC experiments (Section 4), we used the Spearman’s rankcorrelation coefficient to show that the VSIDS and TGC rankings are stronglycorrelated. From our experiments, we can say that for all the VSIDS variantsconsidered in this paper, additive bumping matches with the increase in centrality of the chosen variables. We also observe from our results that the variablesthat solvers pick for branching have very high TGC rank.
The concept of centrality allows us to define in a mathematically precise the intuition many solverdevelopers have had, i.e., that branching on “highly constrained variables” isan effective strategy. Our bridge variable experiment combined with the TGCexperiment suggests that VSIDS focuses on high-centrality bridge variables.What role does multiplicative decay play in making VSIDS so effective? (Answered by Contribution IV, that in turn led to a new adaptive VSIDSpresented as Contribution V.) We show that multiplicative decay is essentiallya form of exponential smoothing (Section 5). We add an explanation as to whythis is important, namely, that exponential smoothing favors variables that persistently occur in conflicts and this is a better strategy for root-cause analysis.We designed a new VSIDS technique, we call adaptVSIDS, based on the aboveresults, wherein we rapidly decay the VSIDS activity if the learnt clause LBDsare large (Section 6).
We showed that this technique is better than mVSIDS onthe SAT Competition 2013 benchmark.Is VSIDS temporally and spatially focused? (Answered by ContributionII.) We show that VSIDS exhibits spatial focus and temporal focus (Section 3),forms of locality in search. While there has been speculation among solver researchers that that CDCL with VSIDS solvers perform local search, we preciselydefine spatial and temporal locality in terms of the community structure.8Related WorkMarques-Silva and Sakallah are credited with inventing the CDCL technique [34].The original VSIDS heuristic was invented by the authors of Chaff [36].
ArminBiere [8] described the low-pass filter behavior of VSIDS, and Huang et al. [26]stated that VSIDS is essentially an EMA. Katsirelos and Simon [30] were thefirst to publish a connection between eigenvector centrality and branching heuristics. In their paper [30], the authors computed eigenvector centrality (via GooglePageRank) only once on the original input clauses and showed that most of thedecision variables have higher than average centrality. Also, it bears stressingthat their definition of centrality is not temporal. By contrast, our results correlate VSIDS ranking with temporal degree and eigenvector centrality, and showthe correlation holds dynamically throughout the run of the solver.
Also, wenoticed that the correlation is also significantly stronger after extending centrality with temporality. Simon and Katsirelos do hypothesize that VSIDS may bepicking bridge variables (they call them fringe variables). However, they do notprovide experimental evidence for this. To the best of our knowledge, we arethe first to establish the following results regarding VSIDS: first, VSIDS picks,bumps, and learns high-centrality bridge variables; second, VSIDS-influencedsearch is more spatially and temporally focused than other branching heuristicswe considered; third, explain the importance of EMA (multiplicative decay) tothe effectiveness of VSIDS; and fourth, invent a new adaptive VSIDS branchingheuristic based on our observations.9Conclusions and Future WorkIn this paper we present various empirically-verified findings on VSIDS.
We showthat VSIDS tends to favor the high-centrality bridge variables in the communitystructure of the Boolean formula. In addition, we show that VSIDS focuses ona small subset of communities in the graph of a SAT instance during search.Lastly, we explain the multiplicative decay of VSIDS with EMA and use thisfinding to devise a new branching heuristic we call adaptVSIDS. These resultsput together show that community structure, graph centrality, and exponentialsmoothing are important lenses through which to understand the behavior ofthe VSIDS family of branching heuristics and CDCL SAT solving. In the future,we plan to strengthen our results by considering a larger number of benchmarks,solvers, branching heuristics, and graph representations.10AcknowledgementWe thank Kaveh Ghasemloo for his help in refining our TGC model and for hisinsight on the connection between VSIDS decay and exponential moving average.References[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][20][21][22][23][24]Starexec, http://www.starexec.org/Proceedings of Past SAT Conferences (2013), http://www.satisfiability.orgSAT Competition Website (2013), http://www.satcompetition.orgSHARCNET Website (2013), https://www.sharcnet.caAtserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with manyrestarts and bounded-width resolution.
In: Theory and Applications of Satisfiability Testing-SAT 2009, pp. 114–127. Springer (2009)Audemard, G., Simon, L.: Glucose: a solver that predicts learnt clauses quality.IJCAI 9, 399–404 (2009)Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessingthe potential of clause learning. Journal of Artificial Intelligence Research (JAIR)22, 319–351 (2004)Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing. pp.
28–33. SAT’08, Springer-Verlag, Berlin, Heidelberg (2008)Biere, A.: Lingeling (2010)Blondel, V.D., Guillaume, J.L., Lambiotte, R., Lefebvre, E.: Fast unfolding ofcommunities in large networks. Journal of Statistical Mechanics: Theory and Experiment 2008(10), P10008 (2008)Brown, R.G.: Exponential Smoothing for predicting demand. Little (1956)Buro, M., Büning, H.K.: Report on a SAT competition. Fachbereich Math.Informatik, Univ.
Gesamthochschule (1992)Clauset, A., Newman, M.E., Moore, C.: Finding community structure in verylarge networks. Physical review E 70(6), 066111 (2004)Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of theThird Annual ACM Symposium on Theory of Computing. pp. 151–158. STOC’71, ACM, New York, NY, USA (1971)Een, N., Sörensson, N.: MiniSat: A SAT solver with conflict-clause minimization.Sat 5 (2005)Faust, K.: Centrality in affiliation networks. Social networks 19(2), 157–191 (1997)Fisher, R.A.: Frequency distribution of the values of the correlation coefficient insamples from an indefinitely large population.
Biometrika pp. 507–521 (1915)Freeman, J.W.: Improvements to Propositional Satisfiability Search Algorithms.Ph.D. thesis, Philadelphia, PA, USA (1995), uMI Order No. GAX95-32175Freeman, L.: Centrality in social networks conceptual clarification. Social Networks 1(3), 215–239 (1979)Gini, C.: Measurement of inequality of incomes. The Economic Journal pp.
124–126 (1921)Girvan, M., Newman, M.E.: Community structure in social and biological networks. Proceedings of the National Academy of Sciences 99(12), 7821–7826 (2002)Gloor, P., Krauss, J., Nann, S., Fischbach, K., Schoder, D.: Web science 2.0:Identifying trends through semantic social network analysis. In: ComputationalScience and Engineering, 2009. CSE ’09.
International Conference on. vol. 4, pp.215–222 (Aug 2009)Golub, G.H., Van Loan, C.F.: Matrix computations, vol. 3. JHU Press (2012)Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT 6(4),245–262 (2009)[25] Hoos, H.H., Stützle, T.: Stochastic Local Search: Foundations & Applications.Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2004)[26] Huang, R., Chen, Y., Zhang, W.: SAS+ planning as satisfiability. J. Artif. Int.Res.
43(1), 293–328 (Jan 2012)[27] Iser, M., Taghdiri, M., Sinz, C.: Optimizing MiniSAT variable orderings for therelational model finder Kodkod. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing.
pp. 483–484. SAT’12,Springer-Verlag, Berlin, Heidelberg (2012)[28] Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals ofmathematics and Artificial Intelligence 1(1-4), 167–187 (1990)[29] Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomyof modern SAT solvers. In: Proceedings of the 14th International Conference onTheory and Application of Satisfiability Testing.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
