2 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, Krzysztof CzarneckiNovember 18, HVC 2015Informal Problem Statement1.Discover the empirical invariants of VSIDS branching heuristic2.Leverage this insight to construct better heuristics3.But first, a little bit of background and motivation2Boolean formula(CNF)1.Conflict-drivenClause-learning1.(CDCL)SATUNSAT3Motivation for Studying Branching HeuristicsKatebi et al.

(2011). Empirical Study of the Anatomy of Modern SAT Solvers.4Problem Statement1.Why does VSIDS decay?2.Which variables does VSIDS bump?3.Does VSIDS focus on (local) regions of the search space?5State-of-the-Art Branching Heuristic: VSIDSHistoryBumpingDecayingProposed by the authors ofthe Chaff solver in 2001.Every variable has afloating-point numbercalled “activity” score.Recent conflict analysis ismore pertinent to thecurrent state of thesolving.●●●Give more weight torecent conflicts.Little computationaloverhead.Implemented bymost competitiveCDCL solvers.●●Activity scores areinitialized to zero.Add one (“bump”) toall the activities ofvariables occurring inconflict analysis.●Multiply theactivities of everyvariable by 0 < < 1after every conflict(“decay”).6Conflict Timeline ( = 0.5)t=1t=2X0.50t=3t=4t=5t=6X0.750.37X0.680.340.170Y0.50.12Y0.560.25Pick X or Y as the next branching variable?● The variable X was in more conflicts than Y.Perhaps we should focus on X?● However, variable Y was in more recent conflicts.VSIDS picks Y over X.7QuestionsFindings1.

Why does VSIDS decay?1. Exponential moving average(reinforcement learning)2. Which variables does VSIDS bump?2. Bridge variables in VIG andtemporal graph centrality3. Does VSIDS focus on (local) regionsof the search space?3. Community structure focus8Result 1: VSIDS decay is an exponentialmoving average (reinforcement learning)9Noisy Time-Series and Smoothing10ExponentialMoving AverageBrown’s simple exponentialsmoothingxt is the time-series data (i.e., price ofa stock).Brown’s simple exponentialsmoothing is defined as:st = α · xt + (1 - α) · st-1α is the smoothing factor11Conflict Timeline (α = 0.5)VSIDS activityt=1t=2X0.5X0.75t=3t=4t=5t=60.37X0.680.340.171xtst1,200.5s0 = 0st = α · xt + (1 - α) · st-10.75120.370.680.340.17Biere, Armin.

(2008). Adaptive Restart Strategies for Conflict Driven SAT Solvers.Huang et al. (2012). SAS+ Planning as Satisfiability.12Why use exponential movingaverages?1. Financial analysis: reduce random noise2. Signal processing: low-pass filtering to removehigh frequency noise3. Reinforcement learning: learning from rewardsin non-stationary environments13“Exponential RecencyWeighted AverageBranching Heuristic forSAT Solvers”AAAI 2016We took a well-known reinforcementlearning algorithm for the nonstationary multi-armed banditproblem and used it as a branchingheuristic.14Improvement on MiniSat with CHBThe number “+x (+y%)” means CHB is solving x more instances than VSIDS, animprovement of y percent.Improvement with CHB2013 + 2014 Application+33 (+10.3%)2013 + 2014 Crafted+64 (+22.5%)For the satisfiable applicationtrack for 2013 and 2014, MiniSatwith CHB solves more instancesthan the respective winners.15SHA-1 Preimage AttackPreimage attack on step-reduced SHA-1instances.16Result 2: VSIDS picks, bumps, and learnsover bridge and temporally centralvariables17Variable Incidence Graph (VIG) of a CNFCNF:a or b or not cabnot b or cc18Community Structure of a Graph● Partition the variables into“communities.”● Modularity(q): many internaledges, few external edges.● Bridge variable: adjacent to anexternal another variable.19“[The] community structure ofreal-world industrial instances isa better predictor of the runningtime of CDCL solvers than othercommonly considered factors1such as variables and clauses.”1Newsham et al.

(2014). Impact of Community Structure on SAT Solver Performance.20Bridge Variables● Bridge variables connectcommunities together.● Related to betweennesscentrality, “a measure of theinfluence a node has over thespread of information throughthe network.” 22Newman, M. E. (2005). A measure of betweennesscentrality based on random walks.21Affinity for Bridge VariablesCategory from SATCompetition 2013% of variables inCNF that arebridge% of VSIDS picksthat are bridge% of VSIDS bumpsthat are bridge% of learnt clausevariables that arebridgeApplication61.0%79.9%71.6%78.4%22Result 3: VSIDS performs focused searchover the community structure of the inputformula23“Conceptually the idea is tofocus on those variables,that have the strongestinfluence on the current3region of the search space.”3Shi et al.

(2005). PASSAT: Efficient SAT-based Test Pattern Generation for Industrial Circuits.24Spatial● Certain regions (i.e.,communities) are favoured.● Community score: number ofVSIDS picks from thecommunity normalized by theorder of the community.● Compute GINI coefficient ofthe community scores.● GINI closer to 1: inequality● GINI closer to 0: equalitypicked100÷ 4100= 25timespicked÷ 100010004 = 250timespicked80÷ 5 =8016times25Spatial (Industrial)Average GINI: mVSIDS 0.592, cVSIDS = 0.560, random = 0.21626TemporalSimilar to temporal locality inhardware cache and cache hit rate.More details in the paper.27Understanding VSIDS: ConclusionsQuestions we posedOur FindingsInterpretations1.Why does VSIDSdecay?1.Exponential movingaverage (reinforcementlearning)1.Reduce noise andreinforcement learning(AAAI 2016 and SHA-1)2.Which variables doesVSIDS bump?2.Bridge variables in theVIG and temporal graphcentrality2.3.Does VSIDS focus on(local) regions ofsearch space?3.Community structurefocus3.Highly central variablesand bridge variablesmay coincide withbackdoorsCommunity localityimplies search localityand cache locality28.