# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 1 Introduction  
The Boolean satisfiability problem (SAT) [1] is a fundamental NP-complete problem in automated reasoning and mathematical logic. As NP-complete problems can be reduced to SAT in polynomial time, SAT is applicable to a wide range of fields [2, 3, 4]. The annual SAT competitions have become an essential event for the distribution of SAT benchmarks and the development of new SAT-solving methods [5]. Sequential SAT solvers compete mainly in three categories: industrial, crafted, and random tracks. The SAT competitions have demonstrated how difficult it is for SAT solvers to perform well across all categories. Results show that conflict-driven clause-learning (CDCL) SAT solvers were most important for solving industrial and crafted SAT benchmarks, whereas look-ahead and Stochastic Local Search (SLS)-based SAT solvers have dominated the random category [5]. Modern implementations of CDCL SAT solvers employ a lot of heuristics. Some of them can be considered baseline, such as the Variable State Independent Decaying Sum (VSIDS) [6], restarts [7], and Literal Block Distance (LBD) [8]. Several others were incorporated recently, including: Learnt Clause Minimization (LCM) [9], Distance (Dist) heuristic [10], Chronological Backtracking (ChronoBT) [11], duplicate learns heuristic [12], Conflict History-Based (CHB) heuristic [13], Learning Rate-based Branching (LRB) heuristic [14], and the SLS component [15]. The results of the SAT competitions have led researchers to conclude that (1) industrial, crafted, and random SAT instances have distinct structures, and (2) SAT-solving methods could exploit such structures. Boolean structural measure proposed for SAT include the phase transition [16], backbone size [17], and backdoor size [18, 19]. We propose three new related measures to thebackbones and backdoors: the backbone frequency, backbone coverage, and backdoor coverage (The reader is referred to Appendix A where the evidence of the backbone and backdoor-related measures on industrial, crafted, and random benchmark instances drawn from 2002-2020 SAT competitions are investigated. In particular, we evaluated the backbone size, LSR backdoor size, and backbone/backdoor variable overlap size, along with the three proposed new related measures: backbone frequency, backbone coverage, and backdoor coverage.). Empirical results indicate that most random benchmarks have no backbones, whereas on average, industrial and crafted benchmark instances have small backbone sizes [20; 21]. 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 [20; 21]. Additionally, across all SAT benchmarks, there tends to be a little overlap between backbone and backdoor variables [20; 21]. A fundamental problem of interest and practical importance concerns the possibility of enhancing the performance of SAT solvers by exploiting the inherent structure of the instances. Several studies have shown, for example, that backbone/backdoor-guided branching heuristics improve the solver performance [18; 22; 23; 24]. Despite these efforts, this problem remains an open issue [19; 25]. One reason is that the computational estimation of most Boolean structural measures (e.g., backbone and backdoor) is intractable [26]. Second, as a consequence, the structural measures of SAT and their impact on the behavior of SAT solvers have not been fully investigated [19; 25]. The present study examines the relevance of Boolean structural measures on the performance of CDCL SAT solvers. The aim is to improve the performance of CDCL SAT solves by exploiting Boolean structural measures. In achieving this, low-overhead heuristics for computing backbones and backdoors are proposed. Using these heuristics, the VSIDS heuristic is extended to exploit backbones and backdoors.