Exponential Recency Weighted Average Branching Heuristic for SAT Solvers (Презентации лекций)

Exponential Recency Weighted Average Branching Heuristic for SAT SolversJia Hui Liang and Vijay Ganesh and Pascal Poupart and Krzysztof Czarneckijliang@gsd.uwaterloo.ca, vijay.ganesh@uwaterloo.cappoupart@uwaterloo.ca, kczarnec@gsd.uwaterloo.caUniversity of Waterloo, CanadaAbstractModern conflict-driven clause-learning SAT solvers routinelysolve large real-world instances with millions of clauses andvariables in them. Their success crucially depends on effective branching heuristics.

In this paper, we propose anew branching heuristic inspired by the exponential recencyweighted average algorithm used to solve the bandit problem. The branching heuristic, we call CHB, learns onlinewhich variables to branch on by leveraging the feedback received from conflict analysis. We evaluated CHB on 1200 instances from the SAT Competition 2013 and 2014 instances,and showed that CHB solves significantly more instancesthan VSIDS, currently the most effective branching heuristic in widespread use. More precisely, we implemented CHBas part of the MiniSat and Glucose solvers, and performedan apple-to-apple comparison with their VSIDS-based variants. CHB-based MiniSat (resp.

CHB-based Glucose) solvedapproximately 16.1% (resp. 5.6%) more instances than theirVSIDS-based variants. Additionally, CHB-based solvers aremuch more efficient at constructing first preimage attackson step-reduced SHA-1 and MD5 cryptographic hash functions, than their VSIDS-based counterparts.

To the best ofour knowledge, CHB is the first branching heuristic to solvesignificantly more instances than VSIDS on a large, diversebenchmark of real-world instances.IntroductionOver the past two decades, conflict-driven clause-learning(CDCL) SAT solvers (Marques-Silva and Sakallah 1999;Moskewicz et al. 2001; Audemard and Simon 2009a;Sorensson and Een 2005; Biere 2010), designed to solve theBoolean satisfiability problem, have played a crucial role inthe development of many innovative techniques in AI, software engineering, and security. Examples include solverbased automated testing with symbolic execution (Cadar etal.

2008), bounded model checking (Biere et al. 2003) forsoftware and hardware verification, and planning in AI (Rintanen 2009). These solvers are surprisingly efficient in solving large classes of real-world instances which may contain tens of millions of variables and clauses in them, eventhough the Boolean satisfiability problem is known to beNP-complete and believed to be intractable in general. A keyc 2016, Association for the Advancement of ArtificialCopyright Intelligence (www.aaai.org).

All rights reserved.element in the success of CDCL SAT solvers is the branching heuristic, such as Variable State Independent DecayingSum (VSIDS) (Moskewicz et al. 2001), that dynamically select variables and assign them truth values (the process alsoknown as branching) as the solver searches for a solution tothe input Boolean formula.While many branching heuristics have been invented, twosignificant issues have hampered their study in the past.First, despite the considerable effort expended in designingbranching heuristics such as DLIS (Marques-Silva 1999),BerkMin (Goldberg and Novikov 2007), and JeroslavWang (Jeroslow and Wang 1990), the VSIDS branchingheuristic and its variants remain as the most effective onesin widespread use today. The success of VSIDS has dramatically raised the bar that any new heuristic has to overcome.Second, until very recently, little was understood as to whythe VSIDS branching heuristic and its variants are so effective.

Some recent papers provide insights into the innerworking of VSIDS (Liang et al. 2015; Ansótegui, GiráldezCru, and Levy 2012; Biere and Fröhlich 2015), and some ofthose insights (Liang et al. 2015) are the basis and inspiration for the work presented in this paper.In this paper, we present a new branching heuristic, wecall conflict history-based branching heuristic (CHB), basedon the exponential recency weighted average (ERWA) algorithm used in nonstationary multi-armed bandit problems(i.e., single state reinforcement learning problems) to estimate the average reward of different actions (Sutton andBarto 1998). Inspired by the bandit framework and reinforcement learning, we learn to choose good variables tobranch based on past experience.

Our goal is to leveragethe theory and practice of a rich sub-field of reinforcementlearning to explain and design an effective branching heuristic for solving real-world problems.The branching heuristic proposed in this paper, CHB, iscompletely online and learns which variable to branch ondynamically as the input instance is being solved. By onlinewe mean that the heuristic learns only during the solvingprocess, and there is no offline learning.We evaluated the efficacy of CHB on the SAT Competition 2013 (Balint et al.

2013) and 2014 (Belov et al.2014) benchmarks from the application and hand-craftedcategories, and show that CHB solves significantly moreinstances than VSIDS. The SAT Competition is a fiercelycompetitive annual international competition, where dozensof the best SAT solvers in the world compete with each otheron a set of benchmarks. These benchmarks, the gold standard of SAT solver research, are perhaps the most comprehensive, diverse, large, difficult-to-solve, and well-curatedset of instances obtained from industrial applications suchas software and hardware verification, AI, security, programanalysis, and cryptography.We implemented CHB as part of the MiniSat and Glucose solvers, and performed an apple-to-apple comparisonwith their VSIDS-based variants.

CHB-based MiniSat (resp.CHB-based Glucose) solved approximately 16.1% (resp.5.6%) more instances than the stock VSIDS-based solver.Additionally, CHB-based solvers are much more efficientthan VSIDS-based ones in constructing first preimage attacks on step-reduced versions of SHA-1 and MD5 cryptographic hash functions. Both Glucose and MiniSat areamong the best solvers in widespread use today.

The Glucose solver in particular has won several recent SAT competitions in multiple categories (Audemard and Simon 2009a).To better appreciate the advance brought about by theCHB branching heuristic, we quote two of the leading SATsolver developers Professors Audemard and Simon (Audemard and Simon 2012):“We must also say, as a preliminary, that improvingSAT solvers is often a cruel world. To give an idea, improving a solver by solving at least ten more instances(on a fixed set of benchmarks of a competition) is generally showing a critical new feature.

In general, thewinner of a competition is decided based on a coupleof additional solved benchmarks.”ContributionsIn this paper, we make the following contributions to theefficacy and understanding of branching heuristics in CDCLSAT solving:• We contribute a new branching heuristic called CHB, inspired by the bandit framework in reinforcement learning,that when combined appropriately with conflict analysis solves significantly more instances than VSIDS-basedsolvers. VSIDS (Moskewicz et al. 2001) has been thestate-of-the-art branching heuristic for the last 15 years.As far as we know, this is the first branching heuristic capable of solving more instances than VSIDS on a largeand diverse real-world benchmark.• We show that CHB-based CDCL solvers construct firstpreimage attacks on step-reduced versions of SHA-1 andMD5 cryptographic hash functions more efficiently thanthe VSIDS-based solvers (Mironov and Zhang 2006).BackgroundIn this section, we describe CDCL SAT solvers, the stateof-the-art branching heuristic called VSIDS (Moskewicz etal.

2001), and an algorithm for solving the nonstationarymulti-armed bandit problem called ERWA (Sutton and Barto1998) which is the basis of the branching algorithm CHBproposed in this paper.Conflict-driven Clause-learning SAT SolversConflict-driven clause-learning (CDCL) SAT solvers are thedominant solvers in practice today. They take as input formulas in Boolean logic, and decide whether they are satisfiable. The input formulas are specified in conjunctive normal form (CNF). CDCL SAT solvers perform backtrackingsearch, where at each step, the branching heuristic picksan unassigned variable and assigns it a value of true orfalse (Moskewicz et al. 2001), a process called branching. The assignment given to a variable during branchingis propagated via a method called Boolean constraint propagation (Moskewicz et al.

2001). Propagation is the processby which the solver simplifies the input formula, leveragingthe assignment given to the branched variable and its logicalconsequences. If propagation leads to a falsified clause, thecurrent assignment is not a satisfying assignment for the input formula. This state of the solver is referred to as being inconflict. The solver recovers from a conflict by backtracking,undoing some of the offending decisions, and trying someother assignments.Crucial to the success of CDCL solvers is the process ofclause learning (Marques-Silva and Sakallah 1999), that istriggered when the solver enters a conflict state. At a highlevel, the solver computes a root cause of why the conflictoccurred, i.e., a subset of currently assigned variables, suchthat any extensions of which is always an unsatisfying assignment to the input formula.

Once this root cause hasbeen identified, the solver remembers it in the form of alearnt clause in order to avoid the mistakes (and exponentially many similar mistakes) that led to a conflict.The algorithm responsible for picking which variable tobranch on is called the branching heuristic. Typically, a separate heuristic is used to pick which value, true or false,to assign to the variable. The order in which the branching heuristic picks variables has an enormous impact on thesolving time. Besides clause learning, the branching heuristic is one of the most important features in modern CDCLSAT solvers (Katebi, Sakallah, and Marques-Silva 2011).The current state-of-the-art branching heuristic is calledVariable State Independent Decaying Sum (VSIDS), proposed in 2001 by the authors of the Chaff solver (Moskewiczet al. 2001).