# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
The best performing variant for each base solver is MapleLCMDistChronoBT-DL-v3_VSIDS_BBsize_BBfreq_restart_version2 (Maple_VBBsfr_v2) and LSTech_VSIDS_BBsize_BBfreq_restart_conflicts_version1 (LSTech_VBBSsfrc_v1). Maple_VBBsfr_v2 solved 307 instances, which was five more than the base solver. With LSTech_VBBSfrc_v1, four more instances were solved than with the base solver. For the solvers based on VSIDS_BDsize_restart, the only variant that improved is LSTech_VSIDS_BDsize_restart_version1. Furthermore, note that the solver variants based on backtracks (row number 3) did not perform well. The scatter plots shown in Figure 2a,b detail performance comparisons of Maple_VBBsfr_v2 and LSTech_VBBsfrc_v1 to their base solvers. Each improved variant solved more instances and achieved a lower PAR-2 score than its base counterpart. Table 4 and Figure 3 report runtime results of Maple_VBBsfr_v2 and LSTech_VBBSfrc_v1 compared to state-of-the-art CDCL SAT solvers on the whole benchmark instances in Table 2. It is observed that LSTech_VBBSfrc_v1 scored 312, which is one instance more than the number of instances solved by [PERSON]_MAB, the winner of the 2021 SAT competition. According to Table 4 and Figure 4a,b, Maple_VBBsfr_v2 showed improvements on both satisfiable and unsatisfiable benchmarks, while LSTech_VBBSfrc_v1 showed improvements on satisfiable benchmarks. \begin{table}
\begin{tabular}{l c c c} \hline \hline  & **\#SAT** & **\#UNSAT** & **Total** \\
**VBS** & **189** & **140** & **329** \\ \hline MapleLCMDistChronoBT-DL-v3 & 175 & 127 & 302 \\ Maple\_VBBsfr\_v1 & 177 & 130 & 307 \\ LSTech & 179 & 129 & 308 \\ LSTech\_VBBSfrc\_v2 & **183** & 129 & **312** \\ Relaxed\_LCMD5 BDL\_newTech & 178 & 128 & 306 \\ Kissat\_GB & 166 & **131** & 297 \\ Kissat\_MAB & **183** & 128 & 311 \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Performance evaluation of CDCL SAT solvers on industrial instances from the 2002–2021 SAT competitions. #SAT (#UNSAT) denotes the number of solved satisfiable (unsatisfiable) instances. Appendix D reports the results in detail. \begin{table}
\begin{tabular}{l c c c c c c} \hline \hline \multicolumn{1}{c}{\multirow{2}{*}{**VBS\({}^{1}\)**}} & \multicolumn{6}{c}{**Number of Solved Industrial Instances**} \\ \cline{3-8}  & \multicolumn{2}{c}{**VBS\({}^{1}\)**} & \multicolumn{2}{c}{**329**} \\ \hline \multirow{4}{*}{**Base Solver**} & \multicolumn{2}{c}{**Version 1**} & \multicolumn{2}{c}{**Version 2**} & \multicolumn{2}{c}{**Version 3**} \\  & **Maple** & **LSTech** & **Maple** & **LSTech** & **Maple** & **LSTech** \\  & **302** & **308** & **302** & **308** & **302** & **308** \\ \hline
1 & VSIDS\_BBsize\_restart & 301 & **309** & 301 & 310 & **310** & **309** \\
2 & VSIDS\_BBsize\_BBfreq\_restart & 302 & 304 & **307** & 308 & **305** & **309** \\
3 & VSIDS\_BBsize\_BBfreq\_backtrack & 296 & 305 & 290 & 302 & 299 & 302 \\
4 & VSIDS\_BBsize\_BBfreq\_conflict & **303** & 308 & **Figure 3: Performance results of Maple_VBBsfr_v2 and LSTech_VBBsfrc_v1 with state-of-the-art CDCL SAT solvers. Results are on the whole industrial benchmarks. A point (1500, 80) is interpreted as follows: there are 80 instances that took less than 1500 s to solve with the respective SAT solver. Figure 2: **(a,b)** Performance comparison of Maple_VBBsfr_v2 and LSTech_VBBsfrc_v1 to their base solvers. The results are on the whole 32 industrial benchmarks. For the \(x\) and \(y\) axes, the labels are of the form a(b/c), where a is the solver name, b is the total number of instances solved, and c is the PAR-2 score. In subfigure (**b**), for example, a point (1000, 1200) means that LSTech_VBBsfrc_v1 took 1000 s to solve the specified instance, whereas LSTech took 1200 s.

## 6 Discussion

Backbones and backdoors have been introduced for over two decades, but the current state of the art of CDCL SAT solvers [17; 49] shows limited evidence of their use to improve CDCL SAT solvers. Among the few is [PERSON] and [PERSON] work [24].