Designing New Phase Selection Heuristics
 102 Downloads
Abstract
CDCLbased SAT solvers have transformed the field of automated reasoning owing to their demonstrated efficiency at handling problems arising from diverse domains. The success of CDCL solvers is owed to the design of clever heuristics that enable the tight coupling of different components. One of the core components is phase selection, wherein the solver, during branching, decides the polarity of the branch to be explored for a given variable. Most of the stateoftheart CDCL SAT solvers employ phasesaving as a phase selection heuristic, which was proposed to address the potential inefficiencies arising from farbacktracking. In light of the emergence of chronological backtracking in CDCL solvers, we reexamine the efficiency of phase saving. Our empirical evaluation leads to a surprising conclusion: The usage of saved phase and random selection of polarity for decisions following a chronological backtracking leads to an indistinguishable runtime performance in terms of instances solved and PAR2 score.
We introduce Decaying Polarity Score (DPS) to capture the trend of the polarities attained by the variable, and upon observing lack of performance improvement due to DPS, we turn to a more sophisticated heuristic seeking to capture the activity of literals and the trend of polarities: Literal State Independent Decaying Sum (LSIDS). We find the 2019 winning SAT solver, Maple_LCM_Dist_ChronoBTv3, augmented with LSIDS solves 6 more instances while achieving a reduction of over 125 seconds in PAR2 score, a significant improvement in the context of the SAT competition.
1 Introduction
Given a Boolean formula F, the problem of Boolean Satisfiability (SAT) asks whether there exists an assignment \(\sigma \) such that \(\sigma \) satisfies F. SAT is a fundamental problem in computer science with wideranging applications including bioinformatics [24], AI planning [18], hardware and system verification [7, 9], spectrum allocation, and the like. The seminal work of Cook [10] showed that SAT is NPcomplete and the earliest algorithmic methods, mainly based on local search and the DPLL paradigm [11], suffered from scalability in practice. The arrival of Conflict Driven Clause Learning (CDCL) in the early ’90s [35] ushered in an era of sustained interest from theoreticians and practitioners leading to a medley of efficient heuristics that have allowed SAT solvers to scale to instances involving millions of variables [25], a phenomenon often referred to as SAT revolution [2, 6, 12, 22, 26, 27, 28, 35].
The progress in modern CDCL SAT solving over the past two decades owes to the design and the tight integration of the core components: branching [19, 34], phase selection [31], clause learning [3, 23], restarts [4, 14, 16, 21], and memory management [5, 30]. The progress has often been driven by the improvement of the state of the art heuristics for the core components. The annual SAT competition [17] is witness to the pattern where development of the heuristics for one core component necessitates and encourages the design of new heuristics for other components to ensure a tight integration.
The past two years have witnessed the (re)emergence of chronological backtracking, a regular feature of DPLL techniques, after almost a quartercentury since the introduction of nonchronological backtracking (NCB), thanks to Nadel and Ryvchin [28]. The impact of chronological backtracking (CB) heuristics is evident from its quick adoption by the community, and the CBbased solver, Maple_LCM_Dist _ChronoBT [32], winning the SAT Competition in 2018 and a subsequent version, Maple_LCM_Dist _ChronoBTv3, the SAT Race 2019 [15] winner. The 2nd best solver at the SAT Race 2019, CaDiCaL, also implements chronological backtracking. The emergence of chronological backtracking necessitates reevaluation of the heuristics for the other components of SAT solving.
We turn to one of the core heuristics whose origin traces to the efforts to address the inefficiency arising due to loss of information caused by nonchronological backtracking: the phase saving [31] heuristic in the phase selection component. When the solver decides to branch on a variable v, the phase selection component seeks to identify the polarity of the branch to be explored by the solver. The idea of phasesaving traces back to the field of constraint satisfaction search [13] and SAT checkers [33], and was introduced in CDCL by Pipatsrisawat and Darwiche [31] in 2007. For a given variable v, phase saving returns the polarity of v corresponding to the last time v was assigned (via decision or propagation). The origin of phase saving traces to the observation by Pipatsrisawat and Darwiche that for several problems, the solver may forget a valid assignment to a subset of variables due to nonchronological backtracking and be forced to rediscover the earlier assignment. In this paper, we focus on the question: is phase saving helpful for solvers that employ chronological backtracking? If not, can we design a new phase selection heuristic?
 1.
We observe that in the context of 2019’s winning SAT solver Maple_LCM_Dist _ChronoBTv3 (referred to as mldc henceforth)^{1}, phase saving heuristic for decisions following a chronological backtracking performs no better than the random heuristic which assigns positive or negative polarity randomly with probability 0.5.
 2.
To address the inefficacy of phase saving for decisions following a chronological backtracking, we introduce a new metric, decaying polarity score (DPS), and DPSbased phase selection heuristic. DPS seeks to capture the trend of polarities assigned to variables with higher priority given to recent assignments. We observe that augmenting mldc with DPS leads to almost the same performance as the default mldc, which employs phase saving as the phase selection heuristic.
 3.
To meet the dearth of performance gain by DPS, we introduce a sophisticated variant of DPS called Literal State Independent Decaying Sum (LSIDS), which performs additive bumping and multiplicative decay. While LSIDS is inspired by VSIDS, there are crucial differences in computation of the corresponding activity of literals that contribute significantly to the performance. Based on empirical evaluation on SAT 2019 instances, mldc augmented with LSIDS, called mldclsidsphase solves 6 more instances and achieves the PAR2 score of 4475 in comparison to 4607 seconds achieved by the default mldc.
 4.
To determine the generality of performance improvement of mldclsidsphase over mldc; we perform an extensive case study on the benchmarks arising from preimage attack on SHA1 cryptographic hash function, a class of benchmarks that achieves significant interest from the security community.
The rest of the paper is organized as follows. We discuss background about the core components of the modern SAT solvers in Sect. 2. Section 3 presents an empirical study to understand the efficacy of phase saving for decisions following a chronological backtracking. We then present DPSbased phase selection heuristic and the corresponding empirical study in Sect. 4. Section 5 presents the LSIDSbased phase selection heuristic. We finally conclude in Sect. 6.
2 Background
A literal is a propositional variable v or its negation \(\lnot v\). A Boolean formula F over the set of variables V is in Conjunctive Normal Form (CNF) if F is expressed as conjunction of clauses wherein each clause is a disjunction over a subset of literals. A truth assignment \(\sigma : V \mapsto \{0,1\}\) maps every variable to 0 (False) or 1 (True). An assignment \(\sigma \) is called satisfying assignment or solution of F if \(F(\sigma ) = 1\). The problem of Boolean Satisfiability (SAT) seeks to ask whether there exists a satisfying assignment of F. Given F, a SAT solver is expected to return a satisfying assignment of F if there exists one, or a proof of unsatisfiability [36].
2.1 CDCL Solver
The principal driving force behind the socalled SAT revolution has been the advent of the Conflict Driven Clause Learning (CDCL) paradigm introduced by MarquesSilva and Sakallah [35], which shares syntactic similarities with the DPLL paradigm [11] but is known to be exponentially more powerful in theory. The power of CDCL over DPLL is not just restricted to theory, and its practical impact is evident from the observation that all the winning SAT solvers in the main track have been CDCL since the inception of SAT competition [17].
On a highlevel, a CDCLbased solver proceeds with an empty set of assignments and at every time step maintains a partial assignment. The solver iteratively assigns a subset of variables until the current partial assignment is determined not to satisfy the current formula, and the solver then backtracks while learning the reason for the unsatisfiability expressed as a conflict clause. The modern solvers perform frequent restarts wherein the partial assignment is set to empty, but information from the run so far is often stored in form of different statistical metrics. We now provide a brief overview of the core components of a modern CDCL solver.
 1.
Decision. The decision component selects a variable v, called the decision variable from the set of unassigned variables and assigns a truth value, called the decision phase to it. Accordingly, a Decision heuristic is generally a combination of two different heuristics – a branching heuristic decides the decision variable and a phase selection heuristic selects the decision phase. A decision level is associated with each of the decision variables while it gets assigned. The count for decision level starts at 1 and keeps on incrementing with every decision.
 2.
Propagation. The propagation procedure computes the direct implication of the current partial assignment. For example, some clauses become unit (all but one of the literals are False) with the decisions recently made by the solver. The remaining unassigned literal of that clause is asserted and added to the partial assignment by the propagation procedure. All variables that get assigned as a consequence of the variable v get the same decision level as v.
 3.
Conflict Analysis. Propagation may also reveal that the formula is not satisfiable with the current partial assignment. The situation is called a conflict. The solver employs a conflict analysis subroutine to deduce the reason for unsatisfiability, expressed as a subset of the current partial assignment. Accordingly, the conflict analysis subroutine returns the negation of the literals from the subset as a clause c, called a learnt clause or conflict clause which is added to the list of the existing clauses. The clauses in the given CNF formula essentially imply the learnt clause.
 4.
Backtrack. In addition to leading a learnt clause, the solver then seeks to undo a subset of the current partial assignment. To this end, the conflict analysis subroutine computes the backtrack decision level l, and then the solver deletes assignment to all the variables with decision level greater than l. As the backtrack intimates removing assignment of last decision level only, backtracking for more than one level is also called nonchronological backtracking or, backjumping.
The solver keeps on repeating the procedures as mentioned above until it finds a satisfying assignment or finds a conflict without any assumption. The ability of modern CDCL SAT solvers to solve realworld problems with millions of variables depends on its highly sophisticated heuristics employed in different components of the solver. Now we discuss some terms related to CDCL SAT solving that we use extensively in the paper.

Variable state independent decaying sum (VSIDS) introduced in Chaff [27] refers to a branching heuristic, where a score called activity is maintained for every variable. The variable with the highest activity is returned as the decision variable. Among different variations of VSIDS introduced later, the most effective is Exponential VSIDS or, EVSIDS [8, 20] appeared in MiniSat [12]. The EVSIDS score for variable v, activity[v], gets incremented additively by a factor f every time v appears in a learnt clause. The factor f itself also gets incremented multiplicatively after each conflict. A constant factor \(g = 1/f\) periodically decrements the activity of all the variables. The act of increment is called bump, and the decrement is called decay. The heuristic is called state independent because the activity of a variable is not dependent of the current state (e.g., current assumptions) of the solver.

Phase saving [31] is a phase selection heuristic used by almost all solver modern solvers, with few exceptions such as the CaDiCaL solver in SAT Race 19 [15]. Every time the solver backtracks and erases the current truth assignment, phase saving stores the erased assignment. For any variable, only the last erased assignment is stored, and the assignment replaces the older stored assignment. Whenever the branching heuristic chooses a variable v as the decision variable and asks phase saving for the decision phase, phase saving returns the saved assignment.

Chronological backtracking. When a nonchronological solver faces a conflict, it backtracks for multiple levels. Nadel et al. [28] suggested nonchronological backtracking (NCB) might not always be helpful, and advocated backtracking to the previous decision level. The modified heuristic is called chronological backtracking (CB). We distinguish a decision based on whether the last backtrack was chronological or not. If the last backtrack is chronological, we say the solver is in CBstate, otherwise the solver is in NCBstate.
2.2 Experimental Setup
In this work, our methodology for the design of heuristics has focused on the implementation of heuristics on a base solver and conduction of an experimental evaluation on a highperformance cluster for SAT 2019 benchmarks. We now describe our experimental setup in detail. All the empirical evaluations in this paper used this setup, unless mentioned otherwise.
 1.
Base Solver: We implemented the proposed heuristics on top of the solver Maple_LCM_Dist_ChronoBTv3 (mldc), which is the winning solver for SAT Race 2019. Maple_LCM_Dist_ChronoBTv3 is an modification of Maple_LCM_Dist_ChronoBT (2018), which implements chronological backtracking on top of Maple_LCM_Dist (2017). Maple_LCM_Dist, in turn, evolved from MiniSat (2006) through Glucose (2009) and MapleSAT (2016). The years in parenthesis represent the year when the corresponding solver was published.
 2.
Code Blocks: The writing style of this paper is heavily influenced from the presentation of MiniSat by Eén and Sörensson [12]. Following Eén and Sörensson, we seek to present implementation details as code blocks that are intuitive yet detailed enough to allow the reader to implement our heuristics in their own solver. Furthermore, we seek to present not only the final heuristic that performed the best, but we also attempt to present closely related alternatives and understand their performance.
 3.
Benchmarks: Our benchmark suite consisted of the entire suite, totaling 400 instances, from SAT Race ’19.
 4.
Experiments: We conducted all our experiments on a highperformance computer cluster, with each node consists of E52690 v3 CPU with 24 cores and 96 GB of RAM. We used 24 cores per node with memory limit set to 4 GB per core, and all individual instances for each solver were executed on a single core. Following the timeout used in SAT competitions, we put a timeout of 5000 seconds for all experiments, if not otherwise mentioned. In contrast to SAT competition, the significant difference in specifications of the system lies in the size of RAM: our setup allows 4 GB of RAM in comparison to 128 GB of RAM allowed in SAT race ’19.
We computed the number of SAT and UNSAT instances the solver can solve with each of the heuristics. We also calculated the PAR2 score. The PAR2 score, an acronym for penalized average runtime, used in SAT competitions as a parameter to decide winners, assigns a runtime of two times the time limit (instead of a “not solved” status) for each benchmark not solved by the solver.^{2}
3 Motivation
The impressive scalability of CDCL SAT solvers owes to the tight coupling among different components of the SAT solvers wherein the design of heuristic is influenced by its impact on other components. Consequently, the introduction of a new heuristic for one particular component requires one to analyze the efficacy of the existing heuristics in other components. To this end, we seek to examine the efficacy of phase saving in the context of recently introduced heuristic, Chronological Backtracking (CB). As mentioned in Sect. 1, the leading SAT solvers have incorporated CB and therefore, we seek to revisit the efficacy of other heuristics in light of CB. As a first step, we focus on the evaluation of phase selection heuristic.
 1.
Phasesaving: Choose the saved phase as polarity, default in mldc.
 2.
Opposite of saved phase: Choose the negation of the saved phase for the variable as polarity.
 3.
Always false: The phase is always set to False, a strategy that was originally employed in MiniSat 1.0.
 4.
Random: Randomly choose between False and True.
Performance of mldc on 400 SAT19 benchmarks while aided with different phase selection heuristics. SAT, UNSAT, and total columns indicate the number of SAT, UNSAT, and SAT+UNSAT instances solved by the solver when using the heuristic. A lower PAR2 score indicates a lower average runtime, therefore better performance of the solver.
Phase selection heuristic used  SAT  UNSAT  Total  PAR2  

In NCBstate  In CBstate  
Random  Random  133  89  222  5040.59 
Phasesaving  Phasesaving  140  97  237  4607.61 
Phasesaving  Random  139  100  239  4537.65 
Phasesaving  Always false  139  98  237  4597.06 
Phasesaving  Opp. of saved phase  137  98  235  4649.13 
We first observe that the mldc solves 237 instances and achieves a PAR2 score of 4607 – a statistic that will be the baseline throughout the rest of the paper. Next, we observe that usage of random both in CBstate and NCBstate leads to significant degradation of performance: 15 fewer instances solved with an increase of 440 s for PAR2. Surprisingly, we observe that random phase selection in CBstate while employing phase saving in NCBstate performs as good as phasesaving for CBstate. Even more surprisingly, we do not notice a significant performance decrease even when using Always false or Opposite of saved phase. These results strongly indicate that phase saving is not efficient when the solver is in CBstate, and motivate the need for a better heuristic. In the rest of the paper, we undertake the task of the searching for a better phase selection heuristic.
4 Decaying Polarity Score for Phase Selection
dps[v] represent the decaying polarity score of the variable v.
pol(v) is \(+1\) if polarity was set to True at the last assignment of the variable, \(1\) otherwise.
The decay factor dec is chosen from (0, 1). The greater the value of dec is, the more preference we put on polarities selected in older conflicts.
Whenever the branching heuristic picks a variable v to branch on, the DPSbased phase selection heuristic returns positive polarity if dps[v] is positive; otherwise, negative polarity is returned.
4.1 Experimental Results
Performance comparison of decaying polarity score with phase saving on SAT19 instances. mldcdecphase represent the solver using DPS.
System  SAT  UNSAT  Total  PAR2 

mldc  140  97  237  4607.61 
mldcdecphase  141  96  237  4604.66 
5 LSIDS: A VSIDS Like Heuristic for Phase Selection
 1.
Literal bumping refers to incrementing activity for a literal. With every bump, the activity for a literal is incremented (additive) by \(inc*mult\), where mult is a fixed constant while at every conflict, inc gets multiplied by some factor \(g > 1\). Literal bumping takes place in the following two different phases of the solver.
Reasonbased bumping
When a clause c is learnt, for all the literals \(l_i\) appearing in c, the activity for \(l_i\) is bumped. For example, if we learn the clause that consists of literals \(v_5\), \(\lnot v_6\) and \(v_3\), then we bump the activity of literals \(v_5\), \(\lnot v_6\) and \(v_3 \).
Assignmentbased bumping
While an assignment for a variable v gets canceled during backtrack; if the assignment was True, then the solver bumps activity for v, otherwise the activity for \(\lnot v\) is bumped.
 2.
Literal decaying denotes the incident of multiplying the parameter inc by a factor \({>} 1\) at every conflict. The multiplication of inc implies the next bumps will be done by a higher inc. Therefore, the older bumps to activity will be relative smaller than the newer bumps. The name decaying underscores the fact that the effect of increasing inc is equivalent to decreasing (or, decaying) the activity of all literals.
 3.
Literal rescoring: As the activity gets incremented by a larger and larger factor every time, the value for activity reaches the limit of a floatingpoint number at some time. At this point the activity of all the literals are scaled down.
5.1 Implementation Details
5.2 Experimental Results
Performance comparison of LSIDS based phase selection with phase saving on 400 SAT19 instances.
System  SAT  UNSAT  Total  PAR2 

mldc  140  97  237  4607.61 
mldclsidsphase  147  96  243  4475.22 
Solved Instances and PAR2 Score Comparison. Table 3 compares numbers of instances solved by the solver mldc and mldclsidsphase. First, observe that mldclsidsphase solves 243 instances in comparison to 237 instances solved by mldc, which amounts to the improvement of 6 in the number of solved instances. On a closer inspection, we discovered that mldc performs CB for at least 1% of backtracks only in 103 instances out of 400 instances. Since mldclsidsphase is identical to mldc for the cases when the solver does not perform chronological backtracking, the improvement of 6 instances is out of the set of roughly 100 instances. It perhaps fits the often quoted paraphrase by Audemard and Simon [4]: solving 10 or more instances on a fixed set (of size nearly 400) of instances from a competition by using a new technique, generally shows a critical feature. In this context, we would like to believe that the ability of LSIDSbased phase selection to achieve improvement of 6 instances out of roughly 100 instances qualifies LSIDSbase phase saving to warrant serious attention by the community.
Table 3 also exhibits enhancement in PAR2 score due to LSIDSbased phase selection. In particular, we observe mldclsidsphase achieved reduction \(2.87\%\) in PAR2 score over mldc, which is significant as per SAT competitions standards. In particular, the difference among the winning solver and runnerup solver for the main track in 2019 and 2018 was \(1.27\%\) and \(0.81\%\), respectively. In Fig. 4, we show the scatter plot comparing instancewise runtime performance of mldc visavis mldclsidsphase. While the plot shows that there are more instances for which mldclsidsphase achieves speedup over mldc than viceversa, the plot also highlights the existence of several instances that time out due to the usage of mldclsidsphase but could be solved by mldc.
Solving Time Comparison. Figure 5 shows a cactus plot comparing performance of mldc and mldclsidsphase on SAT19 benchmarks. We present number of instances on xaxis and the time taken on yaxis. A point (x, y) in the plot denotes that a solver took less than or equal to y seconds to solve y benchmarks out of the 400 benchmarks in SAT19. The curves for mldc and mldclsidsphase indicate, for every given timeout, the number of instances solved by mldclsidsphase is greater than or equal to mldc.
Percentage of Usage and Difference of Selected Phase. Among the instances solved by mldclsidsphase, percentage of decisions taken with LSIDS phase selections is on average \(3.17\%\) over the entire data set. Among the decisions taken with LSIDS phase selection, the average fraction of decisions where the selected phase differs from that of phase saving is \(4.67\%\); It is worth remarking that maximum achieved is \(88\%\) while the minimum is \(0\%\). Therefore, there are benchmarks where LSIDS and phase selection are entirely the same while there are benchmarks where they agree for only \(12\%\) of the cases. The numbers thereby demonstrate that the LSIDSbased phase selection can not be simply simulated by random or choosing phase opposite of phase selection.
Applicability of LSIDS in NCBState. The performance improvements owing the usage of LSIDS during CBstate raise the question of whether LSIDS is beneficial in NCBstate as well. To this end, we augmented mldclsidsphase to employ LSIDSbased phase selection during both NCBstate as well as CBstate. Interestingly, the augmented mldclsidsphase solved 228 instances, nine less compared to mldc, thereby providing evidence in support of our choice of usage of LSIDS during CBstate only.
Deciding the Best Combination of CB and NCB. Nadel and Ryvchin [28] inferred that SAT solvers benefit from an appropriate combination of CB and NCB rather than solely reliance on CB or NCB. To this end, they varied two parameters, T and C according to the following rules to heuristically decide the best combination.

If the difference between the current decision level and backtrack level returned by conflict analysis procedure is more than T, then perform CB.

For the first C conflicts, perform NCB. This rule supersedes the above one.
Performance comparison of LSIDS based phase selection with phase saving on 400 SAT19 instances with different T and C.
T = 100  C = 4000  

C = 2000  3000  4000  5000  T = 25  90  150  200  
SAT  mldc  137  141  140  137  139  137  134  138 
mldclsidsphase  143  139  147  139  142  141  139  142  
UNSAT  mldc  98  96  97  97  98  97  95  97 
mldclsidsphase  99  101  96  100  99  96  99  97  
Total  mldc  235  237  237  234  237  233  229  235 
mldclsidsphase  242  240  243  239  241  238  238  239  
PAR2  mldc  4663  4588  4607  4674  4609  4706  4773  4641 
mldclsidsphase  4506  4558  4475  4575  4555  4556  4622  4583 
5.3 Case Study on Cryptographic Benchmarks
Following SATcommunity traditions, we have concentrated on SAT19 benchmarks. But the complicated process of selection of benchmarks leads us to be cautious about confidence in runtime performance improvement achieved by LSIDSbased phase selection. Therefore, in a bid to further improve our confidence in the proposed heuristic, we performed a case study on benchmarks arising from security analysis of SHA1 cryptographic hash functions, a class of benchmarks of special interest to our industrial collaborators and to the security community at large. For a message \(\mathcal {M}\), a cryptographic hash function F creates a hash \(\mathcal {H} = F(\mathcal {M})\). In a preimage attack, given a hash \(\mathcal {H}\) of a message \(\mathcal {M}\), we are interested to compute the original message \(\mathcal {M}\). In the benchmark set generated, we considered SHA1 with 80 rounds, 160 bits for hash are fixed, and k bits out of 512 message bits are fixed, \(485< k < 500\). The solution to the preimage attack problem is to give the remaining \((512  k)\) bits. Therefore, the brute complexity of these problems will range from \(O(2^{12})\) to \(O(2^{27})\). The CNF encoding of these problems was created using the SAT instance generator for SHA1 [29]. Note that by design, each of the instances is satisfiable. In our empirical evaluation, we focused on a suite comprising of 512 instances^{5} and every experiment consisted of running a given solver with 3 h of timeout on a particular instance.
Performance comparison of LSIDS based phase selection with phase saving on 512 cryptographic instances. Name of systems are same as Table 3.
System  Total solved  PAR2 

mldc  291  9939.91 
mldclsidsphase  299  9710.42 
6 Conclusion
In this paper, we evaluated the efficacy of phase saving in the context of the recently emerged usage of chronological backtracking in CDCL solving. Upon observing indistinguishability in the performance of phase saving visavis random polarity selection, we propose a new score: Literal State Independent Decay Sum (LSIDS) that seeks to capture both the activity of a literal arising during clause learning and also the history of polarities assigned to the variable. We observed that incorporating LSIDS to Maple_LCM_Dist_ChronoBTv3 leads to 6 more solved benchmarks while attaining a decrease of 132 seconds in PAR2 score. The design of a new phase selection heuristic due to the presence of CB leads us to believe that the community needs to analyze the efficiency of heuristics for other components in the presence of chronological backtracking.
Footnotes
 1.
Acronyms in sans serif font denote solvers or solvers with some specific configurations. mldc is used as abbreviation for Open image in new window .
 2.
All experimental data are available at https://doi.org/10.5281/zenodo.3817476.
 3.
 4.
 5.
Benchmarks are available at https://doi.org/10.5281/zenodo.3817476.
Notes
Acknowledgment
We are grateful to the anonymous reviewers for constructive comments that significantly improved the final version of the paper. We are grateful to Mate Soos for identifying a critical error in the early drafts of the paper. This work was supported in part by National Research Foundation Singapore under its NRF Fellowship Programme[NRFNRFFAI120190004] and AI Singapore Programme [AISGRP2018005], and NUS ODPRT Grant [R25200068513]. The computational work for this article was performed on resources of the National Supercomputing Centre, Singapore [1].
References
 1.ASTAR, NTU, NUS, SUTD: National Supercomputing Centre (NSCC) Singapore (2018). https://www.nscc.sg/aboutnscc/overview/
 2.Audemard, G., Simon, L.: Glucose: a solver that predicts learnt clauses quality. SAT Competition, pp. 7–8 (2009)Google Scholar
 3.Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: TwentyFirst International Joint Conference on Artificial Intelligence (2009)Google Scholar
 4.Audemard, G., Simon, L.: Refining restarts strategies for SAT and UNSAT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 118–126. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642335587_11CrossRefGoogle Scholar
 5.Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27(01), 1840001 (2018)CrossRefGoogle Scholar
 6.Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, p. 1 (2013)Google Scholar
 7.Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3540490590_14CrossRefGoogle Scholar
 8.Biere, A., Fröhlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405–422. Springer, Cham (2015). https://doi.org/10.1007/9783319243184_29CrossRefGoogle Scholar
 9.Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSIC programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540247302_15CrossRefzbMATHGoogle Scholar
 10.Cook, S.A.: The complexity of theoremproving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)Google Scholar
 11.Davis, M., Logemann, G., Loveland, D.: A machine program for theoremproving. Commun. ACM 5(7), 394–397 (1962)MathSciNetCrossRefGoogle Scholar
 12.Eén, N., Sörensson, N.: An extensible SATsolver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540246053_37CrossRefGoogle Scholar
 13.Frost, D., Dechter, R.: In search of the best constraint satisfaction search. AAAI 94, 301–306 (1994)Google Scholar
 14.Gomes, C.P., Selman, B., Kautz, H., et al.: Boosting combinatorial search through randomization. AAAI/IAAI 98, 431–437 (1998)Google Scholar
 15.Heule, M.J., Järvisalo, M., Suda, M.: Proceedings of SAT race 2019: solver and benchmark descriptions (2019)Google Scholar
 16.Huang, J., et al.: The effect of restarts on the efficiency of clause learning. IJCAI 7, 2318–2323 (2007)Google Scholar
 17.Järvisalo, M., Le Berre, D., Roussel, O., Simon, L.: The international SAT solver competitions. Ai Mag. 33(1), 89–92 (2012)CrossRefGoogle Scholar
 18.Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: ECAI, vol. 92, pp. 359–363. Citeseer (1992)Google Scholar
 19.Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123–140. Springer, Cham (2016). https://doi.org/10.1007/9783319409702_9CrossRefzbMATHGoogle Scholar
 20.Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS branching heuristics in conflictdriven clauselearning SAT solvers. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 225–241. Springer, Cham (2015). https://doi.org/10.1007/9783319262871_14CrossRefGoogle Scholar
 21.Liang, J.H., Oh, C., Mathew, M., Thomas, C., Li, C., Ganesh, V.: Machine learningbased restart policy for CDCL SAT solvers. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 94–110. Springer, Cham (2018). https://doi.org/10.1007/9783319941448_6CrossRefGoogle Scholar
 22.Liang, J.H., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119–135. Springer, Cham (2017). https://doi.org/10.1007/9783319662633_8
 23.Luo, M., Li, C.M., Xiao, F., Manya, F., Lü, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence, pp. 703–711 (2017)Google Scholar
 24.Lynce, I., MarquesSilva, J.: SAT in bioinformatics: making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136–141. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_16CrossRefGoogle Scholar
 25.MarquesSilva, J., Lynce, I., Malik, S.: Conflictdriven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131–153. IOS Press (2009)Google Scholar
 26.MarquesSilva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRefGoogle Scholar
 27.Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535. ACM (2001)Google Scholar
 28.Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111–121. Springer, Cham (2018). https://doi.org/10.1007/9783319941448_7CrossRefGoogle Scholar
 29.Nossum, V.: Instance generator for encoding preimage, secondpreimage, and collision attacks on SHA1. In: Proceedings of the SAT Competition, pp. 119–120 (2013)Google Scholar
 30.Oh, C.: Improving SAT solvers by exploiting empirical characteristics of CDCL. Ph.D. thesis, New York University (2016)Google Scholar
 31.Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: MarquesSilva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540727880_28CrossRefGoogle Scholar
 32.Ryvchin, V., Nadel, A.: Maple LCM dist ChronoBT: featuring chronological backtracking. In: Proceedings of SAT Competition, p. 29 (2018)Google Scholar
 33.Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_36CrossRefGoogle Scholar
 34.Silva, J.P.M., Sakallah, K.A.: Grasp—a new search algorithm for satisfiability. In: Kuehlmann, A. (ed.) The Best of ICCAD, pp. 73–89. Springer, Heidelberg (2003). https://doi.org/10.1007/9781461502920_7CrossRefGoogle Scholar
 35.Silva, J.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: Proceedings Eighth IEEE International Conference on Tools with Artificial Intelligence, pp. 467–469. IEEE (1996)Google Scholar
 36.Wetzler, N., Heule, M.J.H., Hunt, W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., PaulinMohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229–244. Springer, Heidelberg (2013). https://doi.org/10.1007/9783642396342_18CrossRefGoogle Scholar