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

Understanding VSIDS Branching Heuristicsin Conflict-Driven Clause-Learning SAT SolversJia Hui Liang, Vijay Ganesh, Ed Zulkoski,Atulan Zaman, and Krzysztof CzarneckiUniversity of Waterloo, Waterloo, CanadaAbstract. Conflict-Driven Clause-Learning (CDCL) SAT solvers crucially depend on the Variable State Independent Decaying Sum (VSIDS)branching heuristic for their performance. Although VSIDS was proposednearly fifteen years ago, and many other branching heuristics for SATsolving have since been proposed, VSIDS remains one of the most effective branching heuristics.

Despite its widespread use and repeated attempts to understand it, this additive bumping and multiplicative decaybranching heuristic has remained an enigma.In this paper, we advance our understanding of VSIDS by answering thefollowing key questions. The first question we pose is “what is specialabout the class of variables that VSIDS chooses to additively bump?”In answering this question we showed that VSIDS overwhelmingly picks,bumps, and learns bridge variables, defined as the variables that connect distinct communities in the community structure of SAT instances.This is surprising since VSIDS was invented more than a decade beforethe link between community structure and SAT solver performance wasdiscovered. Additionally, we show that VSIDS viewed as a ranking function correlates strongly with temporal graph centrality measures. Puttingthese two findings together, we conclude that VSIDS picks high-centralitybridge variables.

The second question we pose is “what role does multiplicative decay play in making VSIDS so effective?” We show that themultiplicative decay behaves like an exponential moving average (EMA)that favors variables that persistently occur in conflicts (the signal) overvariables that occur intermittently (the noise). The third question wepose is “whether VSIDS is temporally and spatially focused.” We showthat VSIDS disproportionately picks variables from a few communitiesunlike, say, the random branching heuristic. We put these findings together to invent a new adaptive VSIDS branching heuristic that solvesmore instances than one of the best-known VSIDS variants over the SATCompetition 2013 benchmarks.1IntroductionThe Boolean satisfiability (SAT) problem [14] is the quintessential NP-completeproblem, a class of decision problems conjectured to be computationally hard.Yet, impressively, modern sequential Conflict-Driven Clause-Learning SAT solvers [15,9, 32, 34, 6] are able to solve large instances obtained from real-world applications [29, 3].

Although hundreds of techniques and heuristics have been proposedover the last five decades to solve the Boolean SAT problem [2, 3], modern SATsolvers rely crucially only on a handful of them. Of these, the two most importantare Conflict-Driven Clause-Learning with backjumping (CDCL) [34] and Variable State Independent Decaying Sum (VSIDS) branching heuristic [36].

Manysystematic experiments have been performed to ascertain the veracity of this observation [29]. Additionally, not only is VSIDS one of the most effective branchingheuristics, but many other well-known high-performing branching heuristics aresimply variants of VSIDS. Researchers have proposed some theoretical explanations for the impact of clause-learning on the performance of the modern SATsolvers: clause-learning allows SAT solvers to polynomially simulate general resolution propositional proof system [39, 5, 7]. However, our understanding of therole played by VSIDS heuristic has previously been limited.

The motivation forthe research presented in this paper is to achieve a better scientific understanding of VSIDS. We focus on two well-known variations of VSIDS, namely cVSIDSand mVSIDS, described in Section 2.Our Scientific Findings and Contributions. In this paper we ask the following questions regarding the behavior of VSIDS.1 First, what is special aboutthe class of variables that VSIDS chooses to additively bump? (Answered byContributions I and III.) Second, what role does multiplicative decay play inmaking VSIDS so effective? (Answered by Contribution IV.) Third, is VSIDStemporally and spatially focused? (Answered by Contribution II.)Contribution I: Bridge Variables and VSIDS. Community structure is aproperty exhibited in many real-world graphs, particularly in social networks,where the graph can be partitioned into groups of vertices, called communities,such that each group is densely connected within itself but sparsely connectedwith other groups.

Recent research has shown that the community structurequality of the SAT input correlates with faster solving time [38]. We show thatbridge variables connecting distinct communities in the community structure ofa SAT instance [21] are high priority targets for both the branching heuristicand clause-learning, which suggests one possible explanation for this correlation.Contribution II: Community-focused Search and VSIDS. We define twoterms, spatial focus and temporal focus, to describe how a branching heuristicfocuses on certain regions of the search space during solving, with respect tothe underlying community structure.

We refer to this form of locality as focusedsearch, to distinguish it from local search performed by stochastic local searchsolvers [25]. We show that mVSIDS is more focused than cVSIDS and randombranching according to these metrics.Contribution III: Exponentially-smoothed Temporal Graph Centrality and VSIDS correlate strongly. Third, we show that VSIDS rankingscorrelate strongly with the variable rankings induced by exponentially smoothedtemporal graph centrality (TGC) measures over the temporal variable incidencegraphs (TVIG) of the original and learnt clauses of an input SAT instance. This1All code and experimental data sets are available from our website: https://github.com/JLiangWaterloo/vsids.correlation remains strong throughout the run of the solver.

The TVIG extendsthe well-known variable incidence graph over Boolean formulas by incorporating the dynamically evolving aspect of the learnt clause database inside a SATsolver and uses exponential smoothing to focus on recently learnt clauses. TGCis the temporal version of the widely-used graph centrality measures, such asdegree and eigenvector centrality, which are used to identify important verticesin a graph. The definitions are inspired by recent research on temporal aspectsof social networks [22, 42]. For example, the timed PageRank algorithm [42]is used to discover important publications that are likely to be referenced inthe future.

We show that VSIDS typically selects variables with high temporaldegree centrality and temporal eigenvector centrality. The above-mentioned findings essentially tell us that we have a single family of mathematically-precisegraph-theoretic measures, namely TGC, that succinctly characterizes both theadditive bump and multiplicative decay components of VSIDS family of heuristics. Variables that have high centrality correspond to variables in “recent” learntclauses that are “highly-constrained” and get additively bumped. Variables thatare not “persistently” highly-constrained, i.e., do not occur frequently in recentlearnt clauses get decayed away quickly. Putting together Contributions I andIII, we conclude that VSIDS picks high-centrality bridge variables.Contribution IV: Exponential Moving Average and Multiplicative Decay in VSIDS.

Fourth, we show that the multiplicative decay in VSIDS is aform of exponential moving average, and provide a plausible explanation as towhy this is crucial to the effectiveness of VSIDS.Contribution V: A Novel Adaptive Branching Heuristic. Our findingsled to a new VSIDS called adaptVSIDS that adapatively adjusts the exponentialmoving average (a form of adaptive moving average) depending on the quality ofthe learnt clauses. We show that adaptVSIDS outperforms mVSIDS, by solving2.4% more instances over the SAT Competition 2013 benchmarks.2BackgroundHere we describe VSIDS and the variable incidence graph of a CNF formula.The VSIDS Branching Heuristic and Variants.

The term VSIDS refers toa family of branching heuristics widely used in modern CDCL SAT solvers thatrank all variables of a Boolean formula during the run of a solver. As things standtoday, VSIDS is significantly more effective than other well-known heuristicssuch as DLIS [33], MOM [18], Jeroslow-Wang [28], and BOHM [12]. VSIDS wasa major breakthrough when first introduced as part of the Chaff solver [36]. Thekey idea is to collect statistics over learnt clauses to guide the direction of thesearch, where recent learnt clauses are favored. The key characteristics of VSIDSis the additive bumping and multiplicative decay behavior, described in moredetails below. Another positive characteristic of VSIDS is its low computationaloverhead.