# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech  
The base solvers considered in this study, MapleLCMDistChronoBT-DL-v3 and LSTech, are described in the following section (The reader is referred to Appendix B.1 for a justification of the selection of base solvers.). Both solvers follow the general CDCL framework (A general framework for a CDCL solver is provided in Appendix C.1). We specifically discuss the branching decision heuristic augmented in both solvers, as the proposed improvements are focused on it (A justification for choosing the branching decision heuristic to exploit backbones in order to improve the base solvers is described in Appendix B.2. In addition, Appendix C.2 provides the algorithm for the decision heuristic VSIDS implemented in Maple-based series SAT solvers.). Algorithm 1 describes a top-level implementation for MapleLCMDistChronoBT-DL-v3. There are three decision heuristics augmented in it: Dist, VSIDS, and LRB. For the first 50,000 conflicts, the solver branches using the Dist heuristic (lines 18-19). After the \begin{table}
\begin{tabular}{c c c c c c c} \hline \hline \multirow{2}{*}{**CDCL Solver**} & \multirow{2}{*}{**Base Solver**} & \multirow{2}{*}{**Decision Heuristic**} & \multirow{2}{*}{**Restart Heuristic**} & \multirow{2}{*}{**Backtracks**} & \multirow{2}{*}{**Improvements**} & \multicolumn{2}{c}{**SAT Competition Rank**} \\ \hline MapleLCM & & & & & \(\bullet\) Luby restarts for & & \(\bullet\) Duplicate learns & \(\bullet\) Main track \\ MapleLCM & MapleLCM & LRB and & & \(\bullet\) Glucose-style & & heuristic & ALL/UNSAT \\ DistChronoBT & DistChronoBT & VSIDS & & & \(\bullet\) Glucose-style & & Deterministic \\ -DL-v3 [12] & & & & \(\bullet\) VEIDS & & & LRB-VSIDS & \(\bullet\) Main track SAT \\  & & & & \(\bullet\) VSIDS & & & 2 nd (2019) \\ \hline Relaxed & MapleLCMDist- & & & \(\bullet\) Luby restarts for & & \(\bullet\) Relaxed CDCL & \(\bullet\) Main track ALL \\ LCMD5 BDL- & & & & \(\bullet\) Glucose-style & & approach & 2 nd (2020) \\ newTech [15] & MapleLCMDist- & ChronoBT-DL & VSIDS & & & \(\bullet\) Probability Based & \(\bullet\) Main track SAT \\  & & & & & & Phase Saving & 1 st (2020) \\ \hline Kissat\_MAB [39] & Kissat & VSIDS and & & \(\bullet\) Infrequent & & & Multi-Armed \\  & & & & \(\bullet\)matomato & & Bandit framework & \(\bullet\) ALL/SAT 1 st \\  & & & & \(\bullet\) Frequent restarts & & & VSIDS and CHB & (2021) \\ \hline Kissat\_gb [38] & Kissat\_SAT & VSIDS and & & \(\bullet\) Infrequent & & & \\  & & & \(\bullet\) restarts for SAT & & & \\  & & & \(\bullet\)mato & & & & \\  & & & & & & \\  & & & & & & \\  & & & & & & \\  & & & & & & \\  & & & & & & \\ \hline \hline \end{tabular}
\end{table} 
Table 1: The configuration of CDCL SAT solvers considered in this study. In the last column, under SAT competition rank, the SAT, UNSAT, or ALL indicate the type of track, which is either satisfiable, or unsatisfiable, or both, respectively. first 50,000 conflicts, the solver branches based on a deterministic LRB/VSIDS switching strategy (lines 21-25). It starts from LRB and switches each time the number of propagations since the last switch exceeds a threshold value. This value is initially set to 30,000,000 propagations; then, it increases by 10% with every switch (line 27). A top-level implementation for LSTech SAT solver is presented in Algorithm 2. As the Dist heuristic did not improve the performance of the solver, the developers removed it. The solver switches based on a new deterministic restart-based strategy (lines 35-41). Each time the solver loops a threshold value, it will switch between VSIDS and LRB once. This threshold value is set to 500 (line 35). In addition, LSTech relaxes the backtracking process for protecting promising partial assignments (lines 33-34). When the solver reaches a promising partial assignment, it enters a non-backtracking stage until it obtains a full assignment (line 34). The SLS solver, CCAr, is then called every number of restarts (_stthreshold_) in order to find a satisfying assignment close to the full assignment (lines 16-28).