***该文献对分支决策探讨的角度十分新颖！
Conflict-DrivenClause-Learning(CDCL)SATsolverscruciallydependontheVariableStateIndependentDecayingSum(VSIDS)branchingheuristicfortheirperformance.AlthoughVSIDSwasproposednearlyfifteenyearsago,andmanyotherbranchingheuristicsforSATsolvinghavesincebeenproposed,VSIDSremainsoneofthemosteffectivebranchingheuristics.Despiteitswidespreaduseandrepeatedattemptstounderstandit,thisadditivebumpingandmultiplicativedecaybranchingheuristichasremainedanenigma.
Inthispaper,weadvanceourunderstandingofVSIDSbyansweringthefollowingkeyquestions.
Thefirstquestionweposeis“whatisspecialabouttheclassofvariablesthatVSIDSchoosestoadditivelybump”译文：VSIDS选择添加的变量有什么特殊之处
InansweringthisquestionweshowedthatVSIDSoverwhelminglypicks,bumps,andlearnsbridgevariables,definedasthevariablesthatconnectdistinctcommunitiesinthecommunitystructureofSATinstances.ThisissurprisingsinceVSIDSwasinventedmorethanadecadebeforethelinkbetweencommunitystructureandSATsolverperformancewasdiscovered.译文：在回答这个问题时，我们展示了VSIDS压倒性地选择、碰撞和学习桥梁变量，桥梁变量被定义为在SAT实例的社区结构中连接不同社区的变量。
Puttingthesetwofindingstogether,weconcludethatVSIDSpickshigh-centralitybridgevariables.译文：将这两个发现结合在一起，我们得出结论，VSIDS选择了高中心性桥接变量。
Thesecondquestionweposeis“whatroledoesmultiplicativedecayplayinmakingVSIDSsoeffective”译文：在使VSIDS如此有效的过程中，乘法衰变起了什么作用
Weshowthatthemultiplicativedecaybehaveslikeanexponentialmovingaverage(EMA)thatfavorsvariablesthatpersistentlyoccurinconflicts(thesignal)overvariablesthatoccurintermittently(thenoise).
译文：我们表明，乘法衰减表现得像指数移动平均线(EMA)，它倾向于持续发生冲突的变量(信号)，而不是间歇发生的变量(噪声)。
WeshowthatVSIDSdisproportionatelypicksvariablesfromafewcommunitiesunlike,say,therandombranchingheuristic.译文：我们表明VSIDS不成比例地从少数群体中选择变量，不像随机分支启发式。
WeputthesefindingstogethertoinventanewadaptiveVSIDSbranchingheuristicthatsolvesmoreinstancesthanoneofthebest-knownVSIDSvariantsovertheSATCompetition2013benchmarks.译文：我们将这些发现放在一起，发明了一种新的自适应VSIDS分支启发式，它解决的实例比2013年SAT竞赛中最著名的VSIDS变种之一还要多。
BooleanFormulaExponentialSmoothingEigenvectorCentralityDecayFactor
译文：其中最重要的两个是冲突驱动的clause-learning和backjumping(CDCL)[34]和变元状态独立衰减和(VSIDS)分支启发式[36]
译文：研究人员对clauses-learning对现代SAT求解器性能的影响提出了一些理论解释:clauses-learning允许SAT求解器多项式地模拟一般求解命题证明系统[5,7,39]。
However,ourunderstandingoftheroleplayedbyVSIDSheuristichaspreviouslybeenlimited.译文：然而，我们对VSIDS启发式所扮演的角色的理解以前是有限的。
ThemotivationfortheresearchpresentedinthispaperistoachieveabetterscientificunderstandingofVSIDS.译文：本文提出的研究动机是为了更好地理解VSIDS。
ContributionIV:ExponentialMovingAverageandMultiplicativeDecayinVSIDS.VSIDS中的指数移动平均和乘法衰减。
Fourth,weshowthatthemultiplicativedecayinVSIDSisaformofexponentialmovingaverage,andprovideaplausibleexplanationastowhythisiscrucialtotheeffectivenessofVSIDS.译文：我们证明了VSIDS中的乘法衰减是指数移动平均的一种形式，并提供了一个合理的解释，为什么这对VSIDS的有效性至关重要。
ContributionV:ANovelAdaptiveBranchingHeuristic.OurfindingsledtoanewVSIDScalledadaptVSIDSthatadapativelyadjuststheexponentialmovingaverage(aformofadaptivemovingaverage)dependingonthequalityofthelearntclauses.WeshowthatadaptVSIDSoutperformsmVSIDS,bysolving2.4%moreinstancesovertheSATCompetition2013benchmarks.
译文：调整指数移动平均(自适应移动平均的一种形式)取决于学习的子句的质量。
ItistheinclusionofmultiplicativedecayinVSIDSthatgivesititsdistinctivefeatureoffocusingitssearchbasedonrecentconflicts.译文：VSIDS中包含了乘法衰减，这使它具有了将搜索重点放在最近冲突上的独特特征。T
Theydonotspecifywhatsignalsarebeingfedtothisfilter,andwhythehigh-frequencycomponentsarebeingfilteredoutanddiscarded.译文：他们没有具体说明什么信号被送入这个过滤器，以及为什么高频成分被过滤和丢弃。
Moreprecisely,ateverytimestep,thesignalofavariableis1ifitisbumped,or0otherwise.
EMAisaformofexponentialsmoothing,usedingettingridofnoise(variableswhoseVSIDSscoresareakintohigh-frequencysignals)intimeseriesdata(thesignalsduetoVSIDSscores).Exponentialsmoothingisaclassoftechniquestomitigatetheeffectofrandomnoiseintimeseriesdataforthepurposeofanalysisandforecasting.ArminBiere’snormalizedVSIDSequationcanberewrittentothefollowingrecursiveformula:
Variablesthatoccurpersistentlyin“recent”conflictscouldbeagoodguessfortherootcauseofthoseconflicts.Hence,perhapsthemosteffectivesearchstrategyistofocusondeterminingthisrootcause.译文：在“最近”冲突中持续发生的变量可能是对这些冲突根源的很好的猜测。因此，也许最有效的搜索策略是专注于确定这个根本原因。
Hedevisedadaptivemovingaveragewherethedecayfactor(alsoknownassmoothingconstant)isdeterminedbythemarketvolatilitytominimiselagandnoise.译文：他设计了自适应移动平均线，其中衰减因子(也称为平滑常数)由市场波动决定，以最小化滞后和噪声。
Byfluctuatingthedecayfactorwhennecessary,adaptivemovingaverageisbetterthanEMAatuncoveringtrendsinthemarket.译文：通过在必要时波动衰减因子，自适应移动平均线在揭示市场趋势时优于均线。
LBDofaclauseisdefinedtobethenumberofdecisionlevelsthatitsvariablesspan.译文：子句的LBD被定义为其变量所跨越的决策级别的数量。
IfthesolverisinasearchspacethatproducesmanylearntclauseswithlowLBD,thenwewanttoencouragethesolvertostaywithinthatsearchspace.译文：如果求解器所处的搜索空间产生了很多低LBD的学习子句，那么我们希望鼓励求解器留在该搜索空间内。--如何鼓励？见下面说明，如当前冲突分析的得到学习子句的lbd小，则将decay设置为接近于1，增量间距变小，ceil不变（例如保持1e100）活跃度增量溢出衰减操作推迟，阶段性除以1e100操作的间隔加长。
WedosobyadjustingtheVSIDSdecayfactortobecloserto1,i.e.,decayslower.Ontheotherhand,ifthesolverisinasearchspacethatproducesmanylearntclauseswithhighLBD,itisbesttochooseasmallerdecayfactor,i.e.,decayfaster.
Basedonthisinsight,wedevisedanewVSIDSheuristiccalledadaptVSIDSbyextendingmVSIDSwithanadaptivemovingaverage.
adaptVSIDSmaintainsafloating-pointnumberlbdemaequaltotheexponentialmovingaverageofthelearntclauseLBDs.译文：adaptVSIDS保持一个浮点数lbdema等于learn子句LBDs的指数移动平均值。
lbdemaisupdatedaftereverylearntclauseandthisnumberwillbeusedtoadjustthedecayfactorofthevariables’activities.
InmVSIDS,thevariables’activitiesaredecayedbymultiplyingwithaconstantdecayfactor,typically0.95,aftereachconflict.WhereasinadaptVSIDS,thedecayfactorisadjustedbasedontheLBDofthelearntclause.IftheLBDofthelearntclauseisgreaterthanlbdema,thenuseadecayfactorof0.75,otherwiseuseadecayfactorof0.99.Ourwebsitehasallthecode.译文：在mvsid中，变量的活动在每次冲突后通过乘以一个恒定的衰减因子(通常为0.95)来衰减。而在adaptVSIDS中，衰减因子是根据学习子句的LBD来调整的。如果learned子句的LBD大于lbdema，则使用0.75的衰减因子，否则使用0.99的衰减因子。我们的网站上有所有的代码。
译文：VSIDS选择添加的变量有什么特殊之处译文：我们证明了VSIDS不成比例地偏爱桥变量。
EventhoughSATinstanceshavelargenumberofbridgevariablesonaverage,thefrequencywithwhichVSIDSpicks,bumps,andlearnsbridgevariablesismuchhigher.译文：尽管SAT实例平均有大量桥接变量，但VSIDS选择、碰撞和学习桥接变量的频率要高得多。
WealsoobservefromourresultsthatthevariablesthatsolverspickforbranchinghaveveryhighTGCrank.Theconceptofcentralityallowsustodefineinamathematicallyprecisetheintuitionmanysolverdevelopershavehad,i.e.,thatbranchingon“highlyconstrainedvariables”isaneffectivestrategy.译文：中心性的概念允许我们在数学上精确地定义许多求解器开发人员的直觉，即“高度约束变量”分支是一种有效的策略。
OurbridgevariableexperimentcombinedwiththeTGCexperimentsuggeststhatVSIDSfocusesonhigh-centralitybridgevariables.
WhatroledoesmultiplicativedecayplayinmakingVSIDSsoeffective译文：在使VSIDS如此有效的过程中，乘法衰变起了什么作用(AnsweredbyContributionIV,thatinturnledtoanewadaptiveVSIDSpresentedasContributionV.)
SimonandKatsirelosdohypothesizethatVSIDSmaybepickingbridgevariables(theycallthemfringevariables).However,theydonotprovideexperimentalevidenceforthis.
Tothebestofourknowledge,wearethefirsttoestablishthefollowingresultsregardingVSIDS:译文：据我们所知，我们是第一个建立关于VSIDS的以下结果的:
Inthispaperwepresentvariousempirically-verifiedfindingsonVSIDS.译文：在本文中，我们提出了VSIDS的各种经验验证的发现。
WeshowthatVSIDStendstofavorthehigh-centralitybridgevariablesinthecommunitystructureoftheBooleanformula.
Inaddition,weshowthatVSIDSfocusesonasmallsubsetofcommunitiesinthegraphofaSATinstanceduringsearch.
Lastly,weexplainthemultiplicativedecayofVSIDSwithEMAandusethisfindingtodeviseanewbranchingheuristicwecalladaptVSIDS.译文：我们用EMA解释了VSIDS的乘法衰减，并利用这一发现设计了一个新的分支启发式，我们称之为adaptVSIDS。
Theseresultsputtogethershowthatcommunitystructure,graphcentrality,andexponentialsmoothingareimportantlensesthroughwhichtounderstandthebehavioroftheVSIDSfamilyofbranchingheuristicsandCDCLSATsolving.译文：这些结果放在一起表明，社区结构、图的中心性和指数平滑是理解分支启发式和CDCLSAT求解VSIDS家族行为的重要透镜。
Inthefuture,weplantostrengthenourresultsbyconsideringalargernumberofbenchmarks,solvers,branchingheuristics,andgraphrepresentations.译文：在未来，我们计划通过考虑更多的基准、求解器、分支启发式和图表示来增强我们的结果。