# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
In contrast to random instances, most satisfiable industrial and crafted instances preserve the backbone structure. It is due to the fact that the backbone sizes for most random instances are controlled by being set to zero prior to generation. Structural measures related to backdoors are computed on all satisfiable and unsatisfiable SAT benchmark instances (see Table 1). Figure 2 displays the number of satisfiable and unsatisfiable instances with backdoors. One point to note is that the reported instances for backdoors are lower than those for backbones. This is due to the hardness of computing LSR backdoors [53]. The number of satisfiable instances with backbone/backdoor variable overlap is shown in Figure 3.

All Boolean measures are computed, along with their means and standard deviations. A summary of the results is presented in Table 2. Empirical results indicate that most random benchmarks have no backbones, whereas on average, industrial and crafted benchmark instances have small backbone sizes. The frequency of backbones is low for all benchmark categories. As for the backbone coverage, industrial and crafted benchmarks have higher coverages, on average, than random ones. In both crafted and random benchmark instances, the backdoor size and coverage are greater than those in the industrial category. Additionally, across all SAT benchmarks, there tends to be little overlap between backbone and backdoor variables. ## Appendix B Correlation and Exploitation Analysis

### Correlation Analysis

Correlation analysis was carried out to quantify the strength and direction of the relation between the Boolean structural measures and the CDCL metrics. In particular, we computed the Spearman correlation coefficient to measure the nonlinear dependency between two random variables: the Boolean structural measures and CDCL metrics. Four CDCL solver metrics were evaluated: runtime, number of decisions, number of propagations, and number of conflicts. These metrics are derived from the essential blocks that make up any CDCL solver. The CDCL-based solvers that were examined are MapleLCMDistChronoBT-DL-v3, CryptoMiniSat-ccnr, Kissat, and Riss6-default. In choosing these solvers, we primarily considered their superior performance in SAT competitions and the unique differences in techniques incorporated and implementation. Experiments were conducted on Shaheen II [48] and carried out on SAT instances presented in Table 11. A timeout period of 72 h was set to compute the four metrics runtime, number of decisions, number of propagation, and number of conflicts requiredby the solvers: MapleLCMDistChronoBT-DL-v3, CryptoMiniSat-ccnr, Kissat, and Riss6-default for each of the 7779 SAT instances. As for the backbone and backdoor measures, they were computed as specified in Appendix A. Results are depicted in Figures A4-A7. The results show that CDCL metrics are inversely proportional to backbone-related measures and backbone/backdoor overlap size, but they are proportional to backdoor-related measures across all industrial, crafted, and random benchmark instances. In addition, correlation results are apparent for structured instances. Finally, correlation results are more evident for MapleLCMDistChronoBT-DL-v3 on industrial benchmarks. Based on this, MapleLCMDistChronoBT-DL-v3 was selected as the base solver in our research, along with LSTech, which is an improvement of MapleLCMDistChronoBT-DL-v3 and a medal winner of the 2021 SAT competition. ### Exploitation Analysis

Following the correlation results described in Appendix B.1, MapleLCMDistChronoBT-DL-v3 was used to carry out the rest of the analysis and experiments. As a way of examining whether MapleLCMDistChronoBT-DL-v3 exploits Boolean structural measures, we determined the percentage number of backbone variables decided for the solver in the first 1000 iterations. The experiments were limited to only backbone variables, not backdoors, since backbones are unique in SAT instances while backdoors are not. Therefore, determining whether backdoor variables are exploited is challenging.