# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
We are grateful to the KAUST Supercomputing Laboratory for the use of Shaheen II ([[https://www.hpc.kaust.edu.sa](https://www.hpc.kaust.edu.sa)]([https://www.hpc.kaust.edu.sa](https://www.hpc.kaust.edu.sa)) (accessed on 15 January 2020)). We thank them for providing the computational resources and professional support for carrying out this work. The authors declare no conflict of interest. ## Appendix A The Evidence of Boolean Structural Measures for SAT

Boolean structure measures well known in the literature are: phase transition, backbone size, backdoor size, and backbone/backdoor variable overlap size [25]. In view of the fact that the phase transition is only located for random and industrial-like instances, we focus on characterizing SAT instances based on backbones and backdoors. Interest in backbone and backdoor size was originally motivated to relate them to problem hardness and the performance of the SAT solver [20]. Backbones have been used to guide the variable decision heuristics for SAT solvers [24]. Insight into the heavy-tailed phenomena observed in backtrack heuristics comes from considering backdoor variables. Intuitively, backtrack heuristics appear to be lucky on certain runs due to small (near-zero) backdoor sizes. Consequently, backdoor variables are identified early and set correctly [31; 49; 52]. Boolean structural measures examined are the backbone size, backdoor size, and backbone/backdoor variable overlap size. We also introduced three new related measures: backbone frequency, backbone coverage, and backdoor coverage. All measures are defined in Section 2 except for backbone coverage and backdoor coverage, which are defined below:

**Definition A1** (Backbone coverage). : _Backbone coverage is the percentage proportion of clauses that contains backbone literals in a CNF formula (after CNF formula simplification), denoted \(BBcvg_{\phi}\). Backbone coverage is expressed as follows:_

\[BBcvg_{\phi}=\frac{\sum\limits_{ \begin{subarray}{c}i=1,\\ \exists x_{i}\in BB\phi\times X_{i}\in C_{i}\\ s.t.\ C_{i}\in C\end{subarray} }1}{s.t.\ C_{i}\in C}\times 100\] (A1)

**Definition A2** (Backdoor coverage). : _Backdoor coverage is the percentage number of clauses that contain backdoor variables in a CNF formula (after CNF formula simplification), denoted \(BDcvg_{\phi}\). This is formulated as follows:_

\[BDcvg_{\phi}=\frac{\sum\limits_{ \begin{subarray}{c}i=1,\\ \exists\pi\in BD_{\phi}\phi\times\pi\in C_{i}\\ s.t.~{}G_{i}\in C\end{subarray} }^{|C|}1}{|C|}\times 100 \tag{1}\]

### Backbone and Backdoor Computation

To demonstrate the presence of backbones and backdoors for SAT instances, we calculated these measures across the entire benchmark sets. Backbones were computed exactly by the tool in [42]. This tool is based on repeated calls to MiniSat. Based on the backbone sets, the frequencies and coverages of the backbone sets were calculated as shown in Equations (3) and (1). LSR-backdoors were computed using a tool developed by [19] called LaSeR. Due to the difficulty of exactly computing the LSR-backdoors, the tool was configured to compute an upper bound on the size of the minimal LSR-backdoor. The tool is built on top of the MapleSAT solver [14]. After the backdoor sets were computed, the backdoor coverages were calculated, as shown in Equation (1). Finally, the backbone/backdoor overlap was computed based on Equations (6) and (7). ### Benchmarks and Experimental Setup

Experiments were conducted on Shaheen II [48]. A timeout period of 72 h was set to compute all backbone-related measures (backbone size, backbone frequency, and backbone coverage) and similarly for backdoor-related measures (backdoor size, backdoor coverage, and backbone/backdoor variable overlap size) for each of the 7779 instances (see Table 1) (We were unable to locate benchmarks for 2004, 2005, or 2017). ### Experimental Results

We computed the backbones for all satisfiable instances presented in Table 1. In Figure 1, we report the number of satisfiable instances in each benchmark category withand without backbones.