# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### Algorithms for Computing Backbones and Backdoors  
Throughout the literature, many algorithms for backbone computation have been proposed. To begin with, [PERSON] and [PERSON] [40] proposed three backbone computation algorithms based on model enumeration and SAT testing. To compute backbones, [PERSON] and [PERSON] [41] proposed a graph reduction technique called limit crossing. [PERSON] et al. [26] computed backbones based on enumerating implicants and iterative SAT testing and optimizations with calls to a CDCL SAT solver. The work of [PERSON] and [PERSON] [42] follows the idea of enumerating implicants in [26], but it differs in terms of using a CDCL SAT solver with preferences. [PERSON] et al. [43] suggested three sets of filtering optimization heuristics to improve the performance of the iterative SAT testing method for backbone computation. [PERSON] and [PERSON] [24] introduced a heuristic for backbone computation. The heuristic was incorporated into the DPLL solver, \(k\)cnfs, to encourage branching on backbone variables. Experimental results indicated that \(k\)cnfs performed well on random \(k\)-CNF formulas [5]. [PERSON] [44] applied machine learning to optimize the values of the branching variables in MiniSat [32]. Experimental results confirmed that the solver managed to set on average 78% of the backbones correctly. The solver did reduce conflicts; however, the long preprocessing time outweighed the decrease in runtime.  
Many algorithms for backdoor computation have been proposed in the literature. [PERSON] et al. [18] computed strong backdoors in several industrial instances. Experimental results indicated that the size of the backdoor is close to zero. The authors also investigated the relatedness between backdoors, restarts, and the heavy-tailed distribution phenomena. They suggested that backdoors with sizes near-zero lead to runtime distributions that are lower bounded by heavy tails. This led [PERSON] et al. [18] to hypothesize that SAT solvers that are effective in solving industrial SAT instances exploit backdoors. [PERSON] et al. [20] concluded that strong backdoors seem to be correlated with problem hardness on random 3-CNF formulas, whereas this was not observed for weak backdoors. [PERSON] et al. [21] studied weak backdoors for random and crafted instances. They observed that backdoor values for crafted instances are close to zero. Moreover, the authors discovered that when clause learning is enabled, the average backdoor size decreases. This is of interest because modern CDCL solvers implicitly exploit the backdoor structure. [PERSON] et al. [19] computed weak backdoors for all SAT categories on benchmark instances from 2009-2014 SAT competitions.  
Experiments concluded that weak backdoors are hard to compute and small for all instance categories. [PERSON] et al. [45] extended traditional backdoors to LS backdoors to take advantage of clause learning [29] during the search performed by a CDCL SAT solver. Experiments showed that LS backdoors are exponentially smaller than traditional strong backdoors on mixed integer programming SAT instances [46]. Overall, experiments on instances from all SAT categories have reported a near-zero backdoor size. [PERSON] et al. [19] extended the notion of LS backdoors to allow restarts by introducing the concept of LSR backdoors. The results confirmed that industrial instances indeed appear to have smaller LSR backdoor sizes compared to random instances. [PERSON] et al. [19] observed that the number of LSR backdoors that have been computed are of twice the instances of weak backdoors. [PERSON] et al. [19] concluded that LSR backdoor sizes are larger compared to weak backdoors. However, weak backdoors are harder to compute.