# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
21 then
22 ifbranchMode equals \(\mathit{VSIDS}\)then
23\(\mathit{branchMode}\leftarrow\mathit{LRB}\)
24 else
25\(\mathit{branchMode}\leftarrow\mathit{VSIDS}\)
26\(\mathit{Lastrestart}\leftarrow\mathit{Restarts}\) // \(\mathit{Lastrestart}\) is reset to \(\mathit{break}\)
27\(x\)-PickBranchValue() // the decision heuristic is based on \(\mathit{branchMode}\) OnAssinc(x) // called when variable x is assigned by branching or propagations decisionLevel \(\leftarrow\mathit{decisionLevel}+1\) // increment decision level due to new decision
28\(\mathit{solution}\leftarrow\mathit{solution}\cup(x,\mathit{value})\)
29
30 return\((\mathit{satisfiable},\mathit{solution})\)
```
**Algorithm 2**Pseudocode for top-level implementation of LSTech. ## 4 The Proposed CDCL SAT Solvers

A description of the proposed CDCL SAT solvers that exploit backbones and backdoors is presented in this section. To begin with, for the purpose of guiding the CDCL SAT solver to branch on backbones/backdoors, two low-overhead heuristics are proposed for computing backbones and backdoors. They are described in the following subsection. ### Backbone and Backdoor Computational Heuristics

This section details the proposed heuristics for computing the backbone and backdoor sets: backbone low-overhead (BBLO) heuristic and backdoor low-overhead (BDLO) heuristic. Both heuristics are designed based on relevant features of the backbone and backdoor while having low computational overhead. As described below, this trade-off between accuracy and computational time is motivated by the work of [47]. It should be noted that these heuristics are not intended to be standalone heuristics for computing the backbones and backdoors. Rather, they are incorporated within the CDCL SAT solver, in particular the branching heuristic, to encourage the solver to branch on these variables. #### 4.1.1 The BBLO Heuristic

The BBLO heuristic was inspired by the low-overhead computation of backbones in [47]. [PERSON] and [PERSON] [47] proposed a backbone-based co-evolutionary algorithm for the partial maximum satisfiability problem guided by the estimated backbone literals of the problem. That is, literals that are set to the same value on each run will be considered backbones; otherwise, they will not. BBLO adopts a similar concept except that local search runs are the search tree trails and non-backbone literals are identified in each run (A trail is the partial assignment that represents the current path in the search tree produced by a CDCL SAT solver.). This process is repeated for each restart. The BBLO heuristic is presented in Algorithm 3. It is called during every restart procedure in Algorithms 1 and 2. At the first call of the Algorithm 3, all variables in _list_ are marked as undefined. Upon completing a trail, the initial value of the _list_ is its final value of the previous trail. For each assigned variable (line 3), the heuristic determines if it is not a backbone literal whenever a variable has a different assignment than the previous trail (lines 7 and 8). At the end, all assigned variables in _List_ are moved as literals to the backbone set. ```
Input:\(\phi\): CNF formula with a set of variables \(X\) Output:\(\mathit{BackBones}_{\phi}\): a set of backbone literals for \(\phi\) Data:\(\mathit{List}_{\phi}\): a list of size \(|X|\) where each entry takes one of the values: \(\mathit{true}\), \(\mathit{false}\), \(\mathit{undefined}\), or \(\mathit{notBackBone}\). \(\mathit{List}_{\phi}\) is initialized to \(\mathit{undefined}\) in the first call of Algorithm 3 and its final value is its initial value upon completing a trail. 1 iftrailis completed;//a trailcompletion triggers the computation of the backbones set
2 then
3 for\(x\in\mathit{Assigned}_{\phi}\);//\(\mathit{Assigned}_{\phi}\)is the set of assigned variables so far in \(\phi\).