# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
The backbone-guided decision heuristic they proposed was heavily dependent on unit propagation, which consequently added a significant overhead to the solver performance. It should be noted that early in our work, we have implemented the backbone guided decision heuristic [24] on top of MapleLCMDistChronoBT-DL-v3 to compute backbones; however, the solver performed poorly and never beat the base solver. In addition, it was demonstrated in [19; 50] that it is difficult to build a solver that detects backdoors due to the difficulty of computing them. In this regard, we have proposed the BBLO and BDLO heuristics for computing backbones and backdoors. As far as backdoors, they are calculated under the assumption of no overlap between backbones and backdoors, which is only an experimental observation. According to the performance evaluation in Section 5, both variants Maple_VBBsfr_v2 and LSTech_VBBsfrc_v1 have outperformed the base solvers on solving satisfiable benchmarks, that is, instances with backbones. Therefore, improvements in VSIDS have led to improved performance for both variants in solving more satisfiable instances. It is therefore evident that VSIDS is not only superior at solving unsatisfiable instances [51] but could even be improved to solve satisfiable instances as well. Further observations include the improved performance of Maple_VBBsfr_v2 with both satisfiable and unsatisfiable benchmarks, while LSTech_VBBsfrc_v1 only improved with satisfiable benchmarks. Evidence suggests that the BBLO heuristic could assist the CCAr solver in finding an earlier solution by identifying promising partial assignments. ## 7 Conclusion and Future Work

In this study, we performed a set of modifications to the VSIDS decision heuristic to exploit backbones and backdoors. To guide the CDCL SAT solver to branch on backbone/backdoor variables, we proposed low-overhead heuristics to compute them. We implemented 15 variants on top of two popular state-of-the-art award-winning CDCL solvers, MapleLCMDistChronoBT-DL-v3 and LSTech. The variants were evaluated on

Figure 4: Performance results of Maple_VBBsfr_v2 and LSTech_VBBsfrc_v1 with state-of-the-art CDCL SAT solvers. Subfigures (**a,b**) illustrate results on satisfiable and unsatisfiable industrial benchmarks, respectively. 32 industrial families from 2002 to 2021 SAT competitions. Results showed that bumping the backbone and backdoor variables during the branching heuristic improved both solvers' performance. In particular, the variant of LSTech that augmented the VSIDS decision heuristic to exploit the backbone size and frequency and bumped during restarts and conflicts solved more industrial instances compared to the best state-of-the-art CDCL solvers. In the future, we would like to assess the accuracy of the proposed backbone and backdoor heuristics and to investigate the possibility of any improvements. A further research goal would be to modify other decision heuristics, such as LRB and CHB. Moreover, we would like to conduct a larger study to include broader bases of CDCL SAT solvers and benchmarks. Conceptualization, T.A.-Y. and M.E.B.A.M. ; methodology, T.A.-Y. and M.E.B.A.M. ; software, T.A.-Y. ; validation, T.A.-Y. and M.E.B.A.M. ; formal analysis, T.A.-Y. and M.E.B.A.M. ; investigation, T.A.-Y. and M.E.B.A.M. ; resources, T.A.-Y. and M.E.B.A.M. ; data curation, T.A.-Y. ; writing--original draft preparation, T.A.-Y. ; writing--review and editing, T.A.-Y. and M.E.B.A.M. ; supervision, M.E.B.A.M. and H.M. All authors have read and agreed to the published version of the manuscript. The authors would like to thank the Deanship of Scientific Research (DSR) in King Saud University for funding and supporting this research through the initiative of DSR Graduate Students Research Support (GSR). Not applicable. The datasets generated during the current study are not publicly available but are available from the corresponding author on reasonable request.