Revisiting Restarts of CDCL: Should the Search Information be Preserved?
Xindi Zhang Zhihan Chen Shaowei Cai


Improvement of Neutron-HP package: Unresolved Resonance Region description with Probability Tables
    [
    
==================================================================================================




SAT solvers are indispensable in formal verification for hardware and software with many important applications. 
CDCL is the most widely used framework for modern SAT solvers, and restart is an essential technique of CDCL. 
When restarting, CDCL solvers cancel the current variable assignment while maintaining the branching order, variable phases, and learnt clauses. 
This type of restart is referred to as warm restart in this paper. 
Although different restart policies have been studied, there is no study on whether such information should be kept after restarts. 
This work addresses this question and finds some interesting observations. 

This paper indicates that under this popular warm restart scheme, there is a substantial variation in run-time with different randomized initial orders and phases, which motivates us to forget some learned information periodically to prevent being stuck in a disadvantageous search space. 
We propose a new type of restart called cold restart, which differs from previous restarts by forgetting some of the learned information. 
Experiments show that modern CDCL solvers can benefit from periodically conducting cold restarts. 
Based on the analysis of the cold-restart strategies, we develop a parallel SAT solver. 
Both the sequential and parallel versions of cold restart are more suitable for satisfiable instances, which suggests that existing CDCL heuristics for information management should be revised if one hopes to construct a satisfiable-oriented SAT solver. 






§ INTRODUCTION

The propositional Satisfiability problem (SAT) is a decision procedure that asks for the satisfiability of a given propositional formula.
The propositional formulas are usually presented in Conjunctive Normal Form (CNF), i.e., F = ⋀ _i ∨ _j ℓ_ij.
As the first proved NP-complete problem, SAT is a fundamental problem in computer science <cit.>.




The Conflict-Driven Clause Learning (CDCL) paradigm <cit.> is the most prevalent framework in current SAT solvers.
CDCL is a depth-first searching framework that is equipped with two powerful pruning techniques — non-chronological backtracking and clause learning. The process resembles a binary search tree, where the two outgoing edges of a node represent the two assignments (true or false) of a variable, and each node along with its paternal path is related to a partial (or full) assignment of the given variable set. 
Thanks to the combination of 
restarting <cit.>, 
branching heuristics <cit.>, 
clause management <cit.>,
local search cooperation <cit.>,
and other effective components, CDCL has achieved many remarkable successes in a variety of practical applications, such as electronic design automation (EDA) <cit.>, 
Model Checking <cit.>,
Satisfiability Modulo Theories (SMT) <cit.>, among others.


Restarting contributes significantly to the good performance of CDCL solvers.
Gomes et al. discovered that when solving satisfiable instances, introducing noises into specific heuristics of several complete SAT solvers may result in a run-time variation, which follows a heavy-tailed distribution <cit.>. 
Consequently, they suggested restarting regularly to avoid being stuck in a bad searching direction.
Later, it was found that restarting can also benefit solving unsatisfiable instances, and there are mainly two supportive viewpoints.
On the one hand, restarting can be used to compact the assignment stack and improve the order of decision variables <cit.>; On the other hand, there is evidence that restarts assist CDCL in learning higher quality clauses <cit.>. 


Restart policies determine when to pause the SAT solver's current searching process and relaunch it from the beginning. 
Several restart policies have been proposed and studied <cit.>.
A famous policy is the so-called Luby restart <cit.>, which restarts according to a static fixed-interval sequence. 

The Luby sequence has been proved optimal for a particular class of randomized algorithms called Las Vegas algorithms <cit.>.
Dynamic restart <cit.>, uses on-the-fly information during the searching process to determine when to restart. For example, Glucose restarts <cit.> when the average Literal Block Distance (LBD) <cit.> of recently learned clauses is larger than the global average LBD. 
Biere and Fröhlich (2015) proposed a variant of Glucose's restart strategy based on the exponential moving averages (EMA) <cit.>.
Modern CDCL solvers typically incorporate multiple restarting methods, and their frequency of restarts is quite high — solvers may perform hundreds of restarts every second. 









Current popular CDCL restart policies can all be viewed as warm restarts, in the sense that they keep the search information and use them after a restart. 
There are mainly three types of information that can be kept after restarts:
the scores of variables are preserved for branching;
promising assignments for variables is preserved for phase saving <cit.> or rephasing <cit.>;
the learnt clauses are kept for pruning search space.
Such information is kept and used after restarts, so that the previous computational effort spent would not be wasted <cit.>. 


However, should these information be preserved after restarts? This critical question has not been studied yet. This work aims to answer this question via empirical studies. Our studies lead to some interesting findings, and also new variants of restarts that can bring improvements to state-of-the-art CDCL solvers. 




  
*Contributions
This paper shows by experiments that even after decades of improvements, modern CDCL solvers still exhibit significant run-time variation, mainly due to the greedy strategies that re-use previous information after restarts.
The run-time variation suggests that “periodically performing thorough restarts, resetting heuristic scores, or discarding learnt clauses, may benefit the performance”.

To study this research question, we evaluate three cold restart variants and their combinations in CDCL solvers. These restart policies erase some search information and are called cold restarts. 
The first policy, denoted as FO, forgets the branching rrder, by using random order instead of preserving the branching scores; 
the second, denoted as FP, forgets the phases, by using random phases after restart (note that re-phasing has been studied previously, but our idea uses only random phases); 
finally, the third restart policy forget all the learnt clauses after restarting, which is denoted as FC.


We implement our cold restart policies in three representative state-of-the-art CDCL solvers, including


 <cit.>,
 <cit.>,
and 
 <cit.>.
Generally, our experiments show that by performing such “colder restart” periodically, CDCL solvers can be further improved, sometimes significantly. The FO and FP policies are helpful for both satisfiable and unsatisfiable instances. The FC policy helps improve the performance of satisfiable instances but significantly degrades the performance of unsatisfiable instances.
Through the experiments on selecting LBD thresholds for forgetting the learnt clauses during FC, we know: when the objective is to improve the performance on satisfiable instances, we should set the threshold as small as possible.

Additionally, we use the idea of the best cold restart policy, that is, , to improve two state-of-the-art parallel solvers named  <cit.> and  <cit.>. 
Meanwhile, we apply the parallel cold restart method to  <cit.> and the performance is particularly good on the satisfiable instances, and shows promising speedups.
Based on the analysis of the clause forgetting threshold, we adopt a simple clause-sharing strategy that only shares clauses whose LBD≤2 and LBD≤2, and it produces a solver that is better than state-of-the-art methods on satisfiable instances.
Meanwhile, the idea of can be seen as a reasonable alternative to the configuration selection strategy in parallel portfolios as it is compatible with any CPU core.

Cold restart and its parallel variant work particularly better on satisfiable instances. 
As a result, to develop a satisfiable-oriented SAT solver, it is advisable to rethink and refine certain heuristics, for example, the learned information management policies during restart.



    Paper Organization


The rest of this paper is organized as follows:
Section 2 gives basic concepts.
Section 3 shows the heavy-tail phenomenon of modern CDCL.

Section 4 studies three types of “cold restarts” and their combinations, and further discusses the role of learnt clauses with different LBD values.

Section 5 presents a parallel implementation based on the idea of forgetting order cold restart.
Section 6 discusses some related works and Section 7 concludes the paper. 




§ PRELIMINARIES




 §.§ Background Knowledge


Given a set of Boolean variables V={x_1,x_2,...,x_n}, a literal is either the positive or negative of a Boolean variable.
A clause C = ⋁ _i x_i is a disjunction of literals.
A Conjunctive Normal Form (CNF) formula F = ⋀ _i C_i is a conjunction of clauses.
A complete (partial) assignment is a mapping α: V →{0, 1} that assigns values to all (part of) the variables in V.

SAT is the problem of deciding whether there is a complete assignment that satisfies a given formula.



Modern SAT solvers are based on the conflict-driven clause learning (CDCL) approach <cit.>, which is a (non-)chronological backtracking search process.

This paper is mainly associated with the branching and restart components of CDCL solvers. 



Overview of CDCL Branching
Modern CDCL branching heuristics aim to pick the variable likely to lead to high-quality conflicts, and the ranking score is usually saved in a heap or a priority queue.
Popular branching heuristics include Variable State Independent Decaying Sum (VSIDS) <cit.>, Learning-Rate Based Branching (LRB) <cit.> and Variable Move To Front (VMTF) <cit.>.
Note that the default order of all the solvers mentioned in this paper is sorted according to the index number of variables.

Overview of CDCL Phasing
The phases of CDCL decide the assignment when branching on a variable. Modern CDCL solvers use the phase saving trick <cit.>, which prefers to assign a variable the value it was last assigned. 
Recently, rephasing <cit.> is proposed to periodically reset the phases. There are studies proposing to stick to phases that maximize the assignment trail by extending promising assignments via a technique called target phases <cit.> or via a non-conflicting propagation and improved by local search <cit.>.

Overview of CDCL Restarting
Modern CDCL solvers implement multiple restarting methods, as frequent restarts greatly improve the performance of CDCL.
When restating, CDCL solvers cancel the partial assignment of all variables, but preserve the previous order, phase, and learned clauses.
The restarting operations of modern SAT solvers are almost the same, but there are various heuristics that decide when to start.
The most implemented restarting heuristic in modern SAT solvers include Luby <cit.>, the Glucose-style restart <cit.> and its EMA variants <cit.>. 

Overview of Parallel SAT Solving
There are two main parallel paradigms: the cube-and-conquer paradigm <cit.>, and the portfolio paradigm. 
The first paradigm divides the search space into millions of little subspaces and solves each of them separately, which is successfully used to solve many mathematical problems <cit.>. 
The second paradigm simply runs different SAT solvers or different configurations of a single SAT solver for each thread, where the latter one is called diversity <cit.>. 

Modern portfolio solvers usually use clause sharing <cit.>

to enhance the performance by avoiding searching the same search space.




 §.§ Experimental Settings

In this paper, all experiments are carried out on a cluster with two AMD EPYC 7763 CPU @ 2.45Ghz of 128 physical cores in total and 1T RAM under the operating system Ubuntu 20.04 LTS (64bit).
Benchmarks are selected from SAT Competitions 2020 and 2021, SC20 and SC21 for short, and each has 400 instances.
We only perform one test for each solver, as in SAT competitions. The seeds for each solver are 0, and thus those solvers are deterministic.

For each solver and benchmark, we report the number of solved satisfiable (SAT) and unsatisfiable (UNSAT) instances, denoted as `#SAT' and '#UNS', and the total solved instances, #ALL=#SAT+#UNS.
We also report the penalized average run time score (PAR2),  which penalizes the run time of a failed run as twice the cutoff time (5000 seconds in default), and is a ranking basis of SAT Competition[For SAT and UNSAT experiments, the PAR2 time of the solvers is calculated by excluding the instances that none of the solvers (in the competition and in this work) can solve. ].
For parallel solvers, the speedup for t threads is the ratio of the run time of a single core to the run time of t cores.
The parallel solvers in this paper can use at most 32 CPU cores for each instance, which is a common constraint followed by the competitors in SAT Competition. 
The source codes and detailed results of this paper can be found in a GitHub repository [<https://github.com/CDCL-cold-restart/cold-restart>].
The base sequential and parallel solvers to implement our methods are as follows:


    
  *  (Version 3.0) (for short)  <cit.>: 
    It is a derived version of the series SAT solvers, and these series have won 4 SAT Competitions/Races since  <cit.>.
    
    
    
    
    
    
  *   (for short) <cit.>: It is developed based on <cit.>. It and its improved version won the Hack of SC21 and SC22.
    
    
    
  *  <cit.>: 
    It is the winner of the Main-Track of SC21, which is based on the SC20 Main-Track winner <cit.>. The main idea is to use MAB to dynamically adjust the VSIDS and CHB branching methods. 





    
  *  <cit.>:
    It is a parallel portfolio based on and solved the most satisfiable instances in the Parallel-Track of SC21. 
    
    
    
  *  <cit.>: series parallel solvers have won the Parallel-Track of SAT Competitions 2018, 2020, and 2021. 
    
    is a recent portfolio solver based on the framework.





§ RUN TIME VARIATION WITH WARM RESTARTS

An intriguing phenomenon of backtrack-style SAT solvers is that their performance on one certain instance can vary dramatically with different random seeds, or when the heuristics change slightly.
Restart policies are proposed to address this heavy-tailed behavior.
Initially, when Gomes et. al. proposed the restart to exploit the run time variation of DPLL solvers (the predecessor of CDCL), they introduced some randomized strategies to the branching orders <cit.>. 
Later, in order to re-use previous efforts, more restart policies keep the search information, and we call them warm restarts.
In fact, keeps branching order scores after restart <cit.>. Nowadays, state-of-the-art CDCL solvers employ warm restarts. In this way, the performance of CDCL solvers can be improved, but the price is that the solvers are sensitive to the heuristics, including the ordering and phasing heuristics.
With warm restart, modern CDCL solvers are inclined to visit the previous search space as they preserve the variable branching scores and phases. 

In this section, we study the run time variation of a representative state-of-the-art CDCL solver w.r.t. the initial setting of branching order and default phases of variables.





 §.§ Investigations on the Initial Order




To study the impact of the initial branching order on the performance of CDCL solvers, we choose  <cit.> as the studied solver, the winner of Main Track in SC21. To avoid over-tuning, we use the SC20 benchmark for assessment.
We select the instances that can solve within 5000s (the cutoff in SAT Competitions), and the run time is denoted as T_baseline. 

For each selected instance, we run 100 times with different initial branching orders, which are generated randomly.
The run times are denoted as T_sample. 
For each instance, Fig. <ref> reports the 100 ratios of T_baseline/T_sample, unless T_sample is timeout. We filter the easy instances
that can solve in 10 minutes in this figure. 


    For SAT instances, the run time of the solver varies significantly depending on the initial orders. For 33.3% SAT instances, there are at least one (among the 100) initial orders that can lead to at least 32× speedup. Further, 33 satisfiable instances that cannot be solved by the original solver can be solved by the solver with these random orders.
    
    For UNSAT instances, the run time variance is much smaller. For most UNSAT instances, among the 100 runs with different random orders, the variation for the best run time (or the worst run time) is usually less than 4×.






 §.§ Investigations on the Initial Phases






Besides the branching order, the variables' phase is another important part to guide the CDCL search. 
We study the influence of random initial phases on the performance of the solver. The experiments are carried out similarly. 

In Table 1, we summarize the experiment results of the influence of initial orders and initial phases on the run time of the solver. The plot-figure of run time speedup distribution according to phases resembles Figure <ref>, so it is not presented here. Similar observations can be obtained as with the study on the random initial branching orders.

We would like to note that recent solvers introduced the rephasing methods to periodically reset the variables' phases. They prefer to pick the phases that can lead to a more depth search space <cit.> or use local search optimized phases <cit.>. 
Although these rephasing heuristics introduce a small probability to randomize the phases, 
it is still insufficient to eliminate the heavy-tailed distribution.


The run time variance across different initial phases motivates us to test whether there is a good heuristic that can help to improve performance. 
We try constructing good initial phases by propagation <cit.>, which is similar to the `warm-up' ideas of Knuth <cit.> and how `ReasonLS' initializes the local search <cit.>.
Similarly, for each instance, we generate 100 full assignments using this heuristic method, yet it failed to lead to better peak performance (the best among the 100 runs) than the randomized method.



  §.§.§ Observation for Warm Restart


Overall, we observe that the run-time variation is more significant in SAT instances than in UNSAT instances.  For each instance, we calculate the Coefficient of Variation (CV) of the 100 run-times. A higher CV indicates greater dispersion.
For the case of initial branching order (resp. variable phase),  the average CV is 71.5% (resp. 71.8%) for SAT instances and 27.2% (resp. 36.8%) for UNSAT instances.
We conclude this section by giving this important observation:

Observation 1: The performance (run time) of current CDCL solvers is sensitive to the initial branching order and initial phases, particularly for satisfiable instances. 










§ EVALUATING COLD RESTARTS
 


For many combinatorial search algorithms, random noises could cause run time variance, and restart is an effective method to lessen this variance <cit.>.
However, modern CDCL solvers often employ frequent restart policies, and only a few conflicts occur between two successive restarts. Therefore, modern CDCL solvers tend to search in a similar branching order as the one before restart, since the variable branching scores are adjusted primarily depending on conflicts <cit.>.
Meanwhile, modern SAT solvers tend to assign the same truth value for a chosen variable due to the usage of phase saving <cit.>. Consequently, the current CDCL restart method directs the search direction after a restart to a search space near the location before the restart. 






According to the findings of Section 3, modern solvers still exhibit a significant run time variance according to different initial branching orders or phases, which may be caused by the information-saving behavior of restart policies.
In order to reduce the probability of getting stuck in a disadvantageous searching space, in this section, we study the central research question in this work: 


Should the search information be kept after restart? 


We refer to the restart policies saving all search information in between restarts as warm restarts. All modern CDCL solvers adopt warm restarts. 
There are mainly three types of information that are kept in the warm restart, including branching order (variable score),  phase (variable polarity), and learnt clauses.
For convenience, we refer to the restarts forgetting all search information as complete cold restarts, and those forgetting parts of the information as partial cold restarts. Both of them belong to cold restarts, distinguishing from the normal warm restarts in modern CDCL solvers.

In this section, we first study three cold restart policies (Table <ref>), and then study their combinations (Table <ref>).

    
  * FO policy: Cold restart that forgets the branching order
    
  * FP policy: Cold restart that forgets the phases
    
  * FC policy: Cold restart that forgets learnt clauses






Instead of replacing the warm restarts in the CDCL solvers with our cold restarts, we indeed integrate the cold restarts into the solvers while keeping the warm restarts.[Experiments indicate that the performance deteriorates significantly when warm restarts are directly replaced with cold restarts because cold restarts with an excessively high frequency severely disrupt the search process. It can even make the solver incomplete.] 
In essence, the cooperation of warm restarts and cold restarts corresponds to the classic topic in search algorithms: the balance between exploitation (warm restarts) and exploration (cold restarts).

 Cold Restart Frequency 
We use a common static restart policy with linear growth intervals to keep completeness.
Let us use r to denote the number of conflicts encountered since the last cold restart, and n the number of cold restarts performed.  When r ≥ p× n the next warm restart is replaced by the cold restart, where p is a parameter.
We use the same interval metric (the number of conflicts) as most current restart policies, which keeps the number of cold restarts positively correlated to the number of warm restarts.[The number of cold restart is usually fewer than a few dozen for most instances, while the number of warm-restart is approximately 3, 4 orders of magnitude more than that.]


Parameter Tuning There is only one hyper-parameter p for the cold restart intervals. For each benchmark and solver, the parameter p is adjusted from 100k conflicts to 1000k conflicts with 100k as the minimum granularity, which results in 10 numbers. We report the best results among the 10 parameters. The specified settings for each solver are given in the `p' column for each table, and all the numbers are given in scientific notation.  Note that we did not tune p separately for satisfiable and unsatisfiable benchmarks. 

































































 §.§ Forgetting the Branching Order

Each time the FO (Forgetting Order) cold restart is performed, for all variables, the branching score for each branching heuristics is reset to a float number in [0, 1] randomly, 
because it is a relatively small number, whose impact on the scoring of other variables can be ignored after a few steps of scoring.
The data structures used to sort the variables are updated accordingly.
Note that for the heuristic with no variable scores, e.g. VMTF, we shuffle the variable order that enters the priority queue.


From the results, we can see that periodically resetting variable orders randomly improves the overall performance, especially for SAT instances. In detail, by implementing order forgetting, the #Solved number is increased by 6.3 and 6.7 on average for each solver on SC20 and SC21, respectively. The number for #SAT are 5.7 and 4.0. The improvement for the SAT instances mainly owes to the huge run time variance depending on different initial branching orders.

We also observe the improvements on #UNS for all the solvers, particularly for .
A reasonable explanation is that restart helps to find better refutation paths with high-quality clauses <cit.>. 

Observation 2:  The cold restart that forgets the branching order information is helpful for solving both SAT and UNSAT instances.






























































 §.§ Forgetting the Phases

Now we turn to the FP (Forgetting the Phases) cold restart policy.
Each time the FP restart is performed, we assign a random value either 0 or 1 for each variable.
Similarly, we implement the method on top of the base  solvers. 


The FP cold restart allows to improve the overall performance of all the CDCL solvers.
The number of #Solved is improved by 4.5, 7.0, and 4.5 on average for the three solvers (in the order of their appearance in the table) for each benchmark. We also observe that the performance improvements are mainly due to the improvements on solving satisfiable instances, which is similar to FO. 

Observation 3: The cold restart that forgets the phases is helpful for solving SAT instances, while it has a slight impact on the performance of UNSAT instances.




 §.§ Forgetting Learnt Clauses




























































The FC (Forgetting Learnt Clauses) cold restart policy is simple: Each time a FC cold restart is executed, the solver deletes all the learnt clauses that are maintained by the internal data structures related to clauses management.
We implement FC restart in the three base solvers.


We can observe that forgetting all the learnt clauses is always harmful to solving UNSAT instances. Nevertheless, it sometimes can be beneficial for solving satisfiable instances. Indeed, it is helpful for all the tested solvers on solving SAT instances.
Particularly, the FC restart helps to solve 7 more satisfiable instances for both  and on SC20. This is somehow surprising.
Modern CDCL solvers have a clause management component, which periodically removes some bad clauses to release the reasoning burden. Our experiments demonstrate periodically deleting all learnt clauses can be helpful for solving satisfiable instances, which motivates further study on the role of learnt clauses, particularly in the context of solving a satisfiable instance.







  §.§.§ LBD Threshold for Forgetting Learnt Clauses

In order to gain a better understanding of the role that learned clauses play in CDCL,
we carried out additional supplementary experiments for FC. 
Based on these experiments, we can learn which clauses should be forgotten during cold restart.
We established different thresholds for forgetting learnt clauses during FC cold restart.

In the study that proposed the famous three tire clauses management strategy, Chanseok Oh stated that the leanrt clauses with LBD>5 are barely useful in a practical and global sense <cit.>.
Thus, we set the threshold from LBD > 0 (the default version of FC cold restart) to LBD > 5, in order to preserve some useful learnt clauses [
When a learned clause is produced, if its LBD is 1, it signifies a unit clause, which is immediately used in assigning a value to a variable. Consequently, such clauses are not stored in the learned clause database. Therefore, there will be no learned clauses with LBD less than 2 in the database if there is no other reason. However, it is possible to encounter learned clauses with LBD equal to 1 when performing FO. This occurs when these clauses undergo simplification or their LBDs are recalculated under another branching order when used.].
We take as the base solver and use benchmarks from SAT Competition 2020 and 2021 for evaluation. Note that the cold-restart parameter p is the same as the corresponding default FC version. 
From the results in Table <ref>, we learn that:

    
  * Forgetting more learning clauses usually means better satisfiability performance but worse unsatisfiability performance.
    
  * Keep clauses with LBD ≤ 3 during cold restart helps the solver reach the most balanced performance, which provides another evidence for Oh's methods that take LBD=3 as the cut between core leanrt clauses and the mid-tier learnt clauses <cit.>.

















  §.§.§ Learnt Clause Utilization


We have also calculated the utilization efficiency of clauses belonging to different LBD values in the CDCL process. 
Specifically, for LBD values ranging from 2 to 7, we have separately tracked the usage of learned clauses at these levels in both unit propagation and conflict analysis.
A learned clause is considered to be involved in conflict analysis once if it participates in the generation of another learned clause, and it is deemed to be involved in unit propagation once if it contributes to the reasoning of a variable's assignment directly. For the convenience of statistics, the LBD level of a learnt clause is considered to be the LBD value calculated when it was generated.

The data are shown in Table <ref>, and we normalized the statistics by dividing them by the corresponding values in the `LBD=2' column. From the results, we learnt that there is a significantly larger disparity between the data in columns `LBD=2' and `LBD=3', while the differences among the other columns are relatively minor.








Observation 4:  The cold restart that forgets all learnt clauses is always harmful to solving UNSAT instances, while it is usually (not always) beneficial for solving satisfiable instances. Keeping learnt clauses within higher LBD in cold restart helps for the UNSAT instances.



 §.§ Forgetting Multiple Types of Information


In the preceding section, we evaluated three cold restarts that forget only one type of information, including orders, phases, and learnt clauses.
In this subsection, we evaluate the performance of forgetting multiple types of information, leading to four combinations, including, `+FO+FP', `+FO+FC', `+FP+FC', and `+FO+FO+FC'.


    
  * +: Each  time this cold restart is executed, the solver shuffles the branching order and resets the phase randomly.
    
  * +: Each time this cold restart is executed, the solver randomly shuffles the branching order and removes all learnt clauses.
    
  * +: Each time this cold restart is executed, the solver resets the variable phases randomly and removes all learnt clauses.
    
  * ++: Each time this cold restart is executed, the solver shuffles the branching order randomly, resets the variable phases randomly, and removes all learnt clauses.


We report the best version of hybrid cold restart for each solver on each benchmark in Table <ref>. The results indicate that there is likely optimal configuration for cold restarts for SAT and UNSAT instances respectively. 


Observation 5:  The FO+FC cold restart gives the best performance for satisfiable instances. The FO restart is the best for UNSAT instances and also gives the overall (SAT+UNSAT) best performance in the most cases.









 §.§ Detailed Analysis for Preference

From the previous results, we know the FO cold restart shows the best overall performance. This motivates us to analyze the preference of the FO cold restart on different types of instances.
We split the benchmarks into small categories according to the proceedings of SC20 and SC21. 

We summarized the results here, and the detailed results for all categories are given in our GitHub repository to save space. `#k' is used to denote the number of instances belonging to a given family. 


    
  * Our method is more suitable for solving the `hypertree decomposition' family (#14), `sliding tile puzzle' family (#13), some traveling salesman problems like the `minimal super-permutation' family (#13), and some instances belong to the coloring problem. Compared to the base solver, the improved solver can solve at least two more instances for each of these families.
    
  * For some families, the base solver, and the +version show complementary performance. 
    For example, and +both solve 8 instances on the `circuit multiplier' family (#13), but there are four complementary examples. This shows a potential for further improvements by a deeper study on the balance of warm restart and cold restart.
    
  * On the other hand,
    the FO method deteriorates the performance on the `preimage' family (#11), which encodes the preimage attack problem from cryptanalysis. +solves 2 fewer instances in this family.
    
  * The CV value of solvers on SAT instances remains high, exceeding 50% for half of the instances, slightly improved compared to the version utilizing solely warm-restarts. The `baseball lineup selection' family (#14) exhibits a CV value of less than 30%.






§ A PARALLEL METHOD BASED ON FORGETTING ORDER





We notice that the cold restart augmented solvers and their original base solver exhibit complementary performance for certain instances. 
This is because a cold restart may interrupt the search process when CDCL fails to find a result in a hard but good search space within the given time.
It drives us to develop a parallel variant of the cold restart, to make better use of the complementarity. 
This section implements the parallel forgetting order (FO) cold restart technique, as it is the version with the best overall performance, and we use it to improve state-of-the-art parallel solvers.








    Implementation

Parallel FO uses the same policy as the sequential version except that parallel FO uses different seeds for each thread.


Evaluations 
We implement the parallel cold restart on top of two SOTA parallel solvers, namely [We change the base sequential CDCL solver of from  <cit.> to a better version  <cit.> for comparison, and the performance is almost the same with the original one.]
and .
From the results in Table <ref>, FO can be used to improve the performance of them, especially for #SAT. Specifically, +FO(p) (resp. +FO(p)) improves the PAR2(SAT) time of the (resp. ) by 13.7% (41.81%) on average.



    
    
    
    







    Speedup Analysis


For better evaluating the average speedup[Only instances that can be solved by both a single core and C cores are included in the calculation of the average speedup of C cores, but the instances should not be too easy (can be solved by both solvers in 1 second). Another proper method for calculating averaged speedup, which considers the timeout instances and the punishment, is to compare the PAR2 scores.] 

of parallel forgetting order, we develop a parallel SAT solver with FO, +FO(p), which is developed directly upon a sequential SAT solver without any other parallel techniques.
The results are summarized in Table <ref>.
The solved number and speedup are positively related to the number of CPU cores. The performance on SAT instances is particularly good and it outperforms the SOTA solvers under the same CPU cores, while the improvement on UNSAT instances is limited.

Clause selection in clause sharing portfolios
Prevalent parallel SAT solvers usually employ clause sharing <cit.> to exchange learnt clauses among each thread. 
The idea of sharing the learnt clauses among threads is similar to the idea from the current warm restart that keeps learnt clauses of good quality.
This raises our interest in studying whether the rules about the threshold of learning clauses in FC are also valid for parallel clause sharing.

According to the results in Table <ref>, LBD≤3 learnt clauses have the highest cost-effectiveness. 
We extend the basic parallel FO with clause sharing by simply sharing the learnt clause whose LBD≤2 and LBD≤3 with the help of the framework [We also tried the clause sharing strategy in , which dynamically adjusts the threshold according to the shared literals. It has a similar performance to the version that shares clauses of LBD≤2, and can draw similar conclusions.].
For every thread, a maximum of 1500 literals can be shared within a duration of 0.75 seconds.

According to the results and speedups in Table <ref>, clause sharing can further enhance the performance of UNSAT instances, but has almost little effect on SAT instances.
Thus, the parallel FO is good enough to develop a satisfiable-oriented parallel solver.



Observation 6: The FO cold restart is beneficial for parallel solving, which is significant for SAT instances and minor for UNSAT instances. Clause Sharing has a significantly positive influence on the UNSAT instances, while has nearly no influence on the SAT instances.










Discussions on Comparing Parallel and Previous Diversity Parallel Methods
In a sense, the cold restart parallel method can be seen as a type of the diversity-based parallel method.
As with previous diversity methods, our parallel FO method utilizes the complementarity between threads. 
Previous methods usually make use of the complementarity between different configurations for the strategies in the CDCL solvers <cit.>.
For the parallel FO method, the complementarity mainly comes from periodically switching to different starting points of the search space.
Parallel FO is lightweight and easy to implement — the developers do not need to be familiar with the strategies/codes of CDCL in detail to select configurations.
Simply applying the relevant parallel FO framework with clause sharing can achieve the performance of mainstream parallel SAT solvers.
Another advantage of parallel FO is its strong adaptability. It has good scalability, as it can be applied to any given number of CPU cores without changing the codes.
Based on our experimental findings, it appears that the speedup possesses the potential to further grow alongside an increase in the number of cores.








    Effectiveness Summary

To see how our methods push the state-of-the-art, we compare our best sequential and parallel solvers with their best-performing competitors in Figure <ref>. As we can see from the figure, both the sequential and the parallel versions of cold restart are mainly helpful to push the edge of CDCL solvers on satisfiable instances.

For sequential solvers, +FO+FC performs the best on SAT instances but deteriorates on UNSAT instances, while +FO has the best UNSAT performance (Observation 5).
For the parallel version, the parallel FO helps to improve the effectiveness and efficiency of the satisfiable performance, while having a slight influence on the unsatisfiable performance (Observation 6).



§ RELATED WORKS




Gomes et al. introduced randomization to combinatorial backtrack search and use restarts to exploit the heavy-tailed phenomena <cit.>. 
They introduced controlled randomization into DPLL algorithms by random tie-breaking methods and used a restart heuristic with linear increasing intervals in the following year <cit.>. The CDCL solver Chaff <cit.> proposed the famous VSIDS branching heuristic and added a certain amount of transient randomness to the decision procedure, but it kept the current order at restart. Different from the above works, in this work, the FO cold restart randomly shuffled the branching order. 

After the clause learning technique was invented, there was a study on GRASP <cit.> showing that recording clauses in between restarts can reduce the run time <cit.>. This quickly became a standard of CDCL solvers.  To the best of our knowledge, no CDCL solver is forgetting all learnt clauses in the search process. 


There have been many works studying when to restart <cit.>. However, all these CDCL solvers implemented warm restarts. 
Recently, Biere et al. showed that scrambling CNF usually has a negative effect on the performance of single solvers but has no impact on solver ranking <cit.>.
Rephasing <cit.> is a technique to reset the phases heuristically when restarting, which is becoming a standard technique for current SAT solvers <cit.>.




§ CONCLUSIONS AND FUTURE WORK

Modern CDCL solvers adopt the warm restart policies, which keep all search information in between restarts.
This paper empirically studied the question of whether this information should be preserved in between restarts, leading to several meaningful observations, as well as several cold restart policies (forgetting some information in between cold restarts).  

Experiments suggest that periodically performing cold restarts helps both sequential and parallel CDCL solvers, especially for satisfiable instances.


This work provided an interesting direction for CDCL solvers. In the future, we intend to design better cold restart policies with dynamic intervals.
On real-world benchmarks, even with integrated cold restarts, current CDCL solvers still have great runtime variations, which need to be improved experimentally and theoretically in the future.

Meanwhile, the paper can be viewed as a successful attempt at developing a satisfiable-oriented SAT solver by revisiting the restart policies. 















