# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
15\(\mathit{bumpActivity}(x,BBFreq_{x})\)//bumptheactivitiesofallbackbonesbytheirBBFreq\({}_{x}\)aftereveryrestart. 16...
```
**Algorithm 10**VSIDS_BBsize_restart(Algorithm10):Followinga restart,theactivitiesofthebackdoorvariablescomputedinAlgorithm4 areadditivelybumpedtypicallyby1 (lines4-5). ```
// Callbedwhenthesolverrestarts. 1 ProcedureRestart()
2...
3\(BD_{\phi}\leftarrow\)BDLO(\(\phi\))//computebackdoorvariables,Algorithm4. 4 for\(x\in BD_{\phi}\)do
5\(bumpActivity(x,1)\)//bumptheactivitiesofeverybackdoorvariableby1 aftereveryrestart. 6...
```
**Algorithm 10** VSIDS_BDSize_restart a variant of the VSIDS decision heuristic. ### The CDCL SAT Solvers

To demonstrate that the six proposed VSIDS decision heuristics (Algorithms 5-10) contribute to the state of the art, we implemented each of them on top of two base CDCL SAT solvers, MapleLCMDistChronoBT-DL-v3 and LSTech. In doing so, three different versions of the six extended CDCL SAT solvers were developed. In version 1, during restarts/conflicts/backtracks, bumping occurs only in the VSIDS phase. In version 2, bumping during conflicts is only for the VSIDS phase. But, for restarts/backtracks the bumping occurs in both VSIDS and LRB phases (As the bump in VSIDS_BBsize_BBfreq_conflict occurs only during conflicts, it is the same for versions 1 and 2.). Version 3 is the same as version 1, except that in computing the bump with the backbone frequency, the polarity of variables is taken into account (Version 3 is not applicable to the variants VSIDS_BBsize_restart and VSIDS_BDsize_restart.). For convenience, we name each solver by starting with the base solver name, which is followed by the VSIDS variant, and then the version number, e.g., MapleLCMDistChronoBT-DL-v3_VSIDS_BDsize_restart_version1. ## 5 Performance Evaluation

### Benchmarks and Experimental Setup

Experimental evaluation was performed on industrial benchmark instances drawn from 2002-2021 SAT benchmark instances. On the basis of Table 2, we can see that there are 32 industrial families out of which 12 are satisfiable, 5 are not, and 15 are both. For the purpose of reducing bias, each family contains the same number of satisfiable or/and unsatisfiable instances, seven, and almost the same values of backbone-related measures: backbone size, frequency, and coverage. The CDCL SAT solvers were evaluated on Shaheen II [48], which is a supercomputer at King Abdullah University of Science and Technology (KAUST). Each node of the cluster is equipped with 128 GB of DDR4 memory and a dual CPU based on 16-core Intel Haswell processors running at 2.3 GHz. In accordance with the literature, the time limit for solving each instance was set at 3600 s. A comparison is presented here between the extended proposed CDCL SAT solvers and their counterpart bases as well as three state-of-the-art winning solvers: RelaxedLCMDCBDL_newTech [15], Kissat_GB [38], and Kissat_MAB [39]. The primary metric is the number of solved instances along with the PAR-2 score. The PAR-2 score is the sum of runtimes for all solved instances and twice the timeout for each unsolved instance, so that a lower score is better. \begin{table}
\begin{tabular}{c c} \hline \#families (satisfiable-unsatisfiable-both) & 32 (12-5-15) \\ \#instances & 329 \\ \#satisfiable instances (with backbones-without backbones) & 189 (185-4) \\ \#unsatisfiable instances & 140 \\ \hline \end{tabular}
\end{table} 
Table 2: A summary of industrial benchmarks used in the performance evaluation drawn from 2002–2021 SAT benchmark instances. ### Results

The performance results of the six proposed VSIDS extensions implemented in 15 variants of MapleLCMDistChronoBT-DL-v3 and LSTech are presented in Table 3. Each entry represents the number of solved instances. Bold values indicate that the variant performed better than the base solver. MapleLCMDistChronoBT-DL-v3 and LSTech solved 302 and 308, respectively, out of 329 industrial instances.