1、Towards a DEEPER Empirical Understanding of CDCL SAT Solvers,Vijay Ganesh Assistant Professor, University of Waterloo, Canada Keynote Constraints Solvers in Testing, Verification, and Analysis (CSTVA) July 17, 2016 Saarbrucken, Germany,MOTIVATION: The UNREASONABLE EFFECTIVENESS OF CDCL SAT SOLVERS,C
2、onflict-driven clause learning (CDCL) SAT solvers are a key tool in software engineering and security applications, primarily due to their extraordinary efficiency Example applications: SMT solvers, dynamic symbolic testing, bounded model-checking, liquid types, exploit construction, program analysi
3、s, Isnt SAT supposed to be a hard problem. After all it is NP-complete Yes, SAT is NP-complete. And, yes, in general we believe it to be hard However, for many classes of very large industrial instances SAT solvers are very efficient. This is a mystery that has stumped theoreticians and practitioner
4、s alikeBuild significantly more efficient SAT solvers,2,THE RESEARCH QUESTIONS IN UNDERSTANDING The UNREASONABLE EFFECTIVENESS OF CDCL SAT SOLVERS,Understand the input structure of SAT instances (e.g., community structure, backdoors,) WGS03, BSG09, AL12, NGFAS14, Identify the most important techniqu
5、es in CDCL SAT solvers KSM11, Define a precise model encompassing the most important techniques, e.g., branching LGZC15Put all of this together in a complexity-theoretic framework AFT11, PD11,3,A literal p is a Boolean variable x or its negation x. A clause C is a disjunction of literals: x2 x41 x15
6、 A CNF is a conjunction of clauses: (x2 x1 x5) (x6 x2) (x3 x4 x6) An assignment is a mapping from variables to Boolean values (True, False). A unit clause C is a clause with a single unbound literal The Boolean SAT problem is Find an assignment such that each input clause has a true literal (aka inp
7、ut formula is SAT) OR establish that input formula has no solution (aka input formula is UNSAT) SAT solvers are required to output a solution if input is SAT (many solvers also produce a proof if input is UNSAT) Boolean formulas are typically represented in DIMACS Format,The boolean satisfiability p
8、roblem some standard definitions,6,DPLL SAT Solver Architecture The Basic Solver,DPLL(cnf, assign) Propagate unit clauses;if ”conflict”: return FALSE;if ”complete assign”: return TRUE;”pick decision variable x”;return DPLL(cnfx=0, assignx=0)| DPLL(cnfx=1, assignx=1);,Key Steps in a DPLL SAT SolverPr
9、opagate (Boolean Constant Propagation)Propagate inferences due to unit clausesMost of solving “effort” goes into this stepDetect ConflictConflict: partial assignment is not satisfyingDecide (Branch)Choose a variable & assign some valueBacktrackingImplicitly done via recursive calls in DPLL,7,Modern
10、CDCL SAT Solver Architecture Key Steps and Data-structures,Key steps Decide()Propagate() (Boolean constant propagation)Conflict analysis and learning() (CDCL)Backjump()Forget()Restart()CDCL: Conflict-Driven Clause-LearningConflict analysis is a key stepResults in learning a learnt clausePrunes the s
11、earch spaceKey data-structures (Solver state)Stack or trail of partial assignments (AT)Input clause databaseConflict clause databaseConflict graphDecision level (DL) of a variable,THE RESEARCH QUESTIONS IN UNDERSTANDING The UNREASONABLE EFFECTIVENESS OF CDCL SAT SOLVERS,Understand the input structur
12、e of SAT instances (e.g., community structure, backdoors,) WGS03, BSG09, AL12, NGFAS14, Identify the most important techniques in CDCL SAT solvers KSM11, Define a precise model encompassing the most important techniques, e.g., branching LGZC15Put all of this together in a complexity-theoretic framew
13、ork AFT11, PD11,8,MotivationBackground: Internals of SAT solversProblem statementOur empirical discoveriesCharacterizing industrial instances via community structure LGRC15, NGFAS14*Understanding branching heuristics, a la, VSIDS LGZC15LRB: A new branching heuristic LGPC16, LGPC+16*Putting it all to
14、gether, and conclusions(* Won best paper award at SPLC 2015, and student paper award at SAT 2014. * Won the SAT competition 2016),Talk Outline,Community Structure and SAT Solver Performance Graphs and their Community Structure,Question: How does one go about characterizing the structure of SAT insta
15、nces? Theorists have proposed a variety of metrics like backdoors, treewidth, We considered these measures, but found them to be inadequate in various ways. E.g., weak backdoors do not apply to unsatisfiable instances. Tree width has been shown to not correlate well with SAT solver performance. Answ
16、er: The intuition we had was to focus on metrics that somehow mathematically characterize “important parts” of the SAT formula. We were hoping to argue that the solver somehow focuses on these “important parts” first, and thus solves very large instances without needing to “process” the entire formu
17、la. Defining the “important part of a SAT formula” in a generic way is easier said than done Community structure to rescue View SAT formula as a variable-incidence graph. Partition the graph via the concept of community structure. Focus on highly-connected components.,A note on Community Structure i
18、n Graphs Applications in Various Domains,Community structure GN03,CNM04,OL13 is used to study all kinds of complex networks.Social Networks, e.g. Facebook Internet Protein networks Neural network of the human brain Citation graphs Business networks Populations And more recently, the graph of logical
19、 formulas,Community Structure in Graphs Variable-incidence Graph of Non-random Formula,Community Structure in Graphs Variable-incidence Graph of Random Formula,Modularity and Communities in Graphs Community Structure in Graphs,Modularity (Q) of graph lies between 0 and 1A weighted ratio of the numbe
20、r of edges inside communities to the total number of edges in the graphQ measures qualityHow separable are the communities in the graphHigher Q implies “good community structure”, i.e. highly separable communitiesLower Q implies “bad community structure”, i.e. one giant hairy ball,Community Structur
21、e and SAT Solver Performance Empirical Results,Result #1: Hard random instances have low Q (0.05 Q 0.13)Result #2: Number of communities and Q of SAT instances are more predictive of CDCL solver performance than other measures we consideredResult #3: Strong correlation between community structure an
22、d LBD (Literal Block Distance) in Glucose solver,Community Structure and SAT Solver Performance Characterizing Typical Inputs,Take-home MessageCommunity structure (the quality of which is measured using a metric called Q) of SAT instances strongly affect solver performanceWorking towards Small predi
23、ctive set of features that forms the basis for a more complete explanation Community structure idea needs to be constrained further to eliminate easy theoretical counter-examples More broadly, community structure is a starting point for a line of research that enables us to identify “important sub-p
24、arts” of SAT formulas statically Community structure and learning-sensitive with restarts (LSR) backdoors,Community Structure and SAT Solver Performance IMPACT of this idea,Impact of the Community Structure IdeaNew techniques to exploit community structure by Giraldez-Cru, Levy, Simon,A flourishing
25、of approaches being applied to partition SAT instances and identify the “most important” part to focus on firstPseudo-industrial instance generators for SAT instances based on community structureTheorists have been looking at community structure trying to refine it furtherComprehensive analyses of o
26、ther structure metrics to explain SAT solver performance,MotivationBackground: Internals of SAT solversProblem statementOur empirical discoveriesCharacterizing industrial instances via community structure LGRC15, NGFAS14*Understanding branching heuristics, a la, VSIDS LGZC15LRB: A new branching heur
27、istic LGPC16, LGPC+16*Putting it all together, and conclusions(* Won best paper award at SPLC 2015, and student paper award at SAT 2014. * Won the SAT competition 2016),Talk Outline,19,Modern CDCL SAT Solver Architecture Key Steps and Data-structures,Key steps Decide()Propagate() (Boolean constant p
28、ropagation)Conflict analysis and learning() (CDCL)Backjump()Forget()Restart()CDCL: Conflict-Driven Clause-LearningConflict analysis is a key stepResults in learning a learnt clausePrunes the search spaceKey data-structures (Solver state)Stack or trail of partial assignments (AT)Input clause database
29、Conflict clause databaseConflict graphDecision level (DL) of a variable,What is a branching heuristic?,Decisions,Propagations,Clause Learning,Partial Assignment,Learnt Clause,A branching heuristic is a ranking function that computes a numeric metric called “activity”, and periodically dynamically ra
30、nks variables of an input formula based on activityBut the question remains “what computational problem does a branching heuristic solve?”,20,History,Proposed by the authors of the Chaff solver in 2001.Give more weight to recent conflicts. Little computational overhead.Implemented by most competitiv
31、e CDCL solvers.,Bumping,Every variable has a floating-point number called “activity” score.Activity scores are initialized to zero.Add one (“bump”) to all the activities of variables occurring in conflict analysis.,Decaying,Recent conflict analysis is more pertinent to the current state of the solvi
32、ng.Multiply the activities of every variable by 0d1 after every conflict (“decay”).,21,VSIDS (variable state independent decaying sum) Branching Heuristic,VSIDS Questions,Why does VSIDS perform multiplicative decay?Which variables does VSIDS bump, and why?Does VSIDS demonstrate locality?,Answers,22,
33、Exponential moving average (EMA)High temporal degree variables, and bridge variables in the community structureYes, focuses on few communities (Paper HVC 2015),Problem Statement,What problem do branching heuristics solve? Define precisely the computational problem a branching heuristic is designed t
34、o solve. Use the resultant understanding to improve the effectiveness of branching heuristics in CDCL SAT solvers.,ANSWER,View branching heuristic as technique to solve an optimization problem with a precise objective function, namely, learning rate. Use reinforcement learning to solve this problem.
35、The result is the LRB branching heuristic that outperforms VSIDS on a large, comprehensive set of benchmarks from SAT 2009-2014. MapleSAT solves 100+ more instances than MiniSAT. Also, MapleCMS is competitive against CMS, Glucose, and Lingeling.,23,Branching heuristic solves multi-objective Optimiza
36、tion problem,Decisions,Propagations,Clause Learning,Partial Assignment,Learnt Clause,Maximize:,Maximize the “quantity” of learnt clauses per unit time Maximize learning rateMaximize the “quality” of learnt clauses We dont know how to do this yet Possible candidates for quality include clause length,
37、 firstUIP,24,Learning Rate Example,Student,Teacher,A = false, B = true, C = false,Learnt Clause: A or C,Student,Teacher,A = false, C = true, D = false,Learnt Clause: A or D,Student,Teacher,A = false, B = true, D = false,Learnt Clause: D or C,Student,Teacher,B = true, D = false,Learnt Clause: D or E,
38、sampled_learning_rate(A) = 2/3,25,sampled_learning_rate(B) = 0/3,Learning Rate,26,learning_rate(X) = (X is in conflict analysis | X is assigned AND solver is in conflict),Problem 1: Unfortunately, learning rate is hard to compute. Can we estimate it?Problem 2: Also, learning rate is constantly chang
39、ing. Need to adapt our estimate over time in an online fashionSolution: Reinforcement learning techniques are ideal for such optimization problems,Exponential Moving Average (EMA),27,Multi-Armed Bandit PROBLEM to MODEL BRANCHING HEURISTICS,28,p,$,sample average = 1/3 $4 + 1/3 $3 + 1/3 $1,exponential
40、 moving average = (1 )2 $4 + (1 )1 $3 + (1 )0 $1,More weight,Less weight,p,$,p,$,Best slot machine to play (for now),Learning-Rate Branching (LRB) Example,29,A is assigned,A is unassigned,sampled_learning_rate(A) = 2/3,A is assigned,A is unassigned,sampled_learning_rate(A) = 1/3,exponential moving a
41、verage = (1 )1 2/3 + (1 )0 1/3,“Rewards”,Activity(A),VSIDS,The reward is a constant Every time a variable appears in a learnt clause, its activity is additively bumped by a constant,LRB (without Extensions),30,EMA performed for all variables at the same time After each conflict, the activities of al
42、l variables are decayed,The reward is not constant Every time a variable appears in a learnt clause, the numerator of its learning rate reward is incremented. After each conflict, the denominator of each assigned variables learning rate reward is incremented,EMA performed only when variable goes fro
43、m assigned to unassigned When a variable is unassigned, the variable receives the learning rate reward, and the estimate Q is updated,Experimental SETUP,Benchmark consists of all the instances in the application and hard combinatorial categories from four previous SAT competitions (2009, 2011, 2013,
44、 2014) Total number of instances: 1975 Experiments performed on StarExec cluster with 5000 second timeout The solvers we used in our experiments are: MiniSat 2.2.0 with VSIDS replaced with CHB and LRB (MapleSAT) CryptoMiniSat 4.5.3 with VSIDS replaced with LRB (MapleCMS) Lingeling bal from 2015 SAT
45、Race Glucose 4.0,31,APPLE-TO-APPLE ResultS (Minisat WITH vsids vs. chb vs. lrb),32,COMPARISON WITH STATE-OF-THE-ART: CryptoMinisat, MapleCMS, Glucose, and Lingeling,33,Result: Global Learning-Rate,34,Global Learning Rate: # of conflicts/# of decisionsExperimental setup: ran 1200+ application and han
46、d-crafted instances on MapleSAT with VSIDS, CHB, LRB, Berkmin, DLIS, and JW with 5400 sec timeout per instance on StarExec,Future Work: Quality Of Learning,Simultaneously maximize learning rate and maximize the “quality” of learnt clauses.Not all learnt clauses are created equal, good learnt clauses
47、 prune a lot of remaining search space.Should branch on variables that will lead to high quality learnt-clauses.Need to consider the trade-off between the two objectives: learning rate and quality.,35,Conclusion: Branching heuristics,LRB (and CHB) is shown to be a significant improvement over state-
48、of-the-art VSIDS branching heuristic, for the first time in 15 yearsView heuristics like the branching as an optimization problem with a learning rate objective functionLeverage reinforcement learning to solve such optimization problems, making use of the enormous amount of online data generated by
49、a CDCL SAT solverOnline policy optimization is everywhere in SAT solvers,36,MotivationBackground: Internals of SAT solversProblem statementOur empirical discoveriesCharacterizing industrial instances via community structure LGRC15, NGFAS14*Understanding branching heuristics, a la, VSIDS LGZC15LRB: A new branching heuristic LGPC16, LGPC+16*Putting it all together, and conclusions,
