# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 2 Definitions and Notations
### Boolean Structural Measures  
**Definition 10** (Backbone literal [17]). : \(x_{b}\) _is a backbone literal of \(\phi\) if for all satisfying assignments of \(\phi\), the value of \(x_{b}\) is fixed._  
**Definition 11** (Backbone of a CNF formula [17]). : _The backbone of \(\phi\) is the set of all backbone literals, which is denoted \(BB_{\phi}\)._  
**Definition 12** (Backbone size of a CNF formula [17]). : _The backbone size of \(\phi\) is the cardinality of \(BB_{\phi}\), which is denoted \(|BB_{\phi}|\). The normalized backbone size of \(\phi\) is the ratio of the backbone size to the number of variables \(|X|\), which is denoted \(BBsize_{\phi}\):_  
\[BBsize_{\phi}=\frac{|BB_{\phi}|}{|X|} \tag{1}\]  
**Definition 13** (Backbone frequency). : _The backbone frequency of a backbone literal \(x_{b}\in BB_{\phi}\) is the ratio of the total number of occurrences of \(x_{b}\) in \(\phi\) to the total number of clauses (after CNF formula simplification, which involves reducing the number of variables and/or clauses in a CNF formula to a logically equivalent formula. It is part of the preprocessing phase that takes place before the solving phase. ), which is denoted \(BBfree_{x_{b}}\). This can be expressed as follows:_\[BBfre_{x_{b}}=\frac{\sum\limits_{i=1}^{|\mathcal{E}|}1}{|\mathcal{C}|} \tag{2}\]  
_The backbone frequency of \(\phi\) is the percentage average of the backbone frequencies of all backbone literals, which is denoted \(BBfre_{\phi}\). This is expressed as follows:_  
\[BBfre_{\phi}=\frac{\sum\limits_{ \begin{subarray}{c}k=1\\ x_{b}\in BB_{\phi}\end{subarray} }^{|BB_{\phi}|}BBfre_{x_{b}}}{|BB_{\phi}|}\times 100 \tag{3}\]  
**Definition 14** (SAT sub-solver [18]). : _A SAT sub-solver \(\Gamma\) is an algorithm that takes an input CNF formula \(\phi\) and satisfies the following:_  
1. _(Trichotomy)_ \(\Gamma\) _correctly determines_ \(\phi\)_. If satisfiable it returns a solution; otherwise, it is unsatisfiable._
2. _(Efficiency)_ \(\Gamma\) _runs in polynomial time._
3. _(Trivial-solvability)_ \(\Gamma\) _can determine whether_ \(\phi\) _is trivially_ * _true, that is,_ \(\phi\) _has no clauses; or_ * _false, that is,_ \(\phi\) _has an empty clause._
4. _(Self-reducibility) If_ \(\Gamma\) _determines_ \(\phi\)_, then_ \(\forall x_{i}\in X\)_,_ \(\Gamma\) _determines:_ \[\phi^{*}|_{\{x_{i}=value_{i}|value_{i}\in\{true,false\}\}}.\] (4) _where the latter denotes a simplified formula by fixing the value of any_ \(x_{i}\) _to true or false._  
**Definition 15** (Weak backdoor [18]). : _A non-empty subset of variables \(BD_{\phi}\subseteq X\) is a weak backdoor with respect to sub-solver \(\Gamma\) if there exists a truth assignment of \(BD_{\phi}\) s.t. \(\Gamma\) returns a satisfying assignment._  
**Definition 16** (Strong backdoor [18]). : _A subset of variables \(BD_{\phi}\subseteq X\) is a strong backdoor with respect to sub-solver \(\Gamma\) if for all truth assignments of \(BD_{\phi}\), \(\Gamma\) returns a satisfying assignment or concludes unsatisfiability._  
**Definition 17** (Learning-Sensitive (LS) backdoor [27]). : _A subset of variables \(B_{LS}\) is an LS backdoor with respect to sub-solver \(\Gamma\) if there exists a search tree exploration order such that a CDCL SAT solver branches only on variables in \(B_{LS}\), and with \(\Gamma\) and learnt clauses at the leaves of the search tree, it either finds a satisfying assignment for \(\phi\), or it proves that \(\phi\) is unsatisfiable._  
**Definition 18** (Learning Sensitive with Restarts (LSR) backdoor [19]). : _A subset of variables \(B_{LSR}\) is an LSR backdoor with respect to sub-solver \(\Gamma\) if there exists a search tree exploration order with restarts such that a CDCL SAT solver branches only on variables in \(B_{LSR}\), and with a sub-solver \(\Gamma\) and learnt clauses at the leaves of the search tree, it either finds a satisfying assignment for \(\phi\) or proves that \(\phi\) is unsatisfiable._  
**Definition 19** (Backdoor size of a CNF formula [18]).