# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
4 do
5 if\(\mathit{List}_{\phi}[x]\)is undefinedthen
6\(\mathit{List}_{\phi}[x]\gets x_{\mathit{val}}\);//\(\mathit{x_{\mathit{val}}}\)is the assignment value of variable \(x\); either true or false
7 elseif\(\mathit{List}_{\phi}[x]\)is not marked notBackBone and \(\mathit{List}_{\phi}[x]\)is not equal to \(\mathit{x_{\mathit{val}}}\)then
8\(\mathit{List}_{\phi}[x]\gets\mathit{notBackBone}\)
9
10 Copy literals in \(\mathit{List}_{\phi}\) to \(\mathit{BackBones}_{\phi}\) returnBackBones\({}_{\phi}\)
```
**Algorithm 3**A backbone-based low-overhead computational heuristic (BBLO). #### 4.1.2 The BOLO Heuristic

The BPLO heuristic is inspired by the findings in [20,21] as well as our findings in Appendix A that show experimentally the near-zero overlap between backbone and LSR backdoor variables on all benchmark categories. Consequently, the BDLO heuristic computes the backdoor variables from the backbones in Algorithm 3. As computed in Algorithm 4, backdoor variables are those that are not backbones (line 9). ```
Input:\(\phi\): CNF formula with a set of variables \(X\) Output:\(BackDoors_{\phi}\): a set of backdoor variables for \(\phi\) Data:\(ListBB_{\phi}\): a list of size \(|X|\) that takes values \(true\), \(false\), \(undef\), and \(notBackBone\), \(ListBD_{\phi}\): a list of size \(|X|\) that takes values \(true\), \(false\), and, \(notBackDoor\). \(List_{\phi}\) is initialized to \(undef\) and \(ListBD_{\phi}\) to \(notBackDoor\) in the first call of Algorithm 4 and their final value is their initial values upon completing a trail. 1 if trail is completed;// a trail completion triggers the computation of the backbone set
2 then
3 for\(x\in Assigned_{\phi}\): // \(Assigned_{\phi}\) is the set of assigned variables so far in \(\phi\)do
4 if\(ListBB_{\phi}[x]\) is \(undef\)then
5\(ListBB_{\phi}[x]\gets x_{val}\); // \(x_{val}\) is the assignment value of variable x; either true or false else if\(ListBB_{\phi}[x]\) is not marked notBackBone and \(ListBB_{\phi}[x]\) is not equal to \(x_{val}\)then
6\(ListBB_{\phi}[x]\gets notBackBone\)
7\(ListBD_{\phi}[x]\gets x_{val}\)
8
9
10 Copy assigned variables in \(ListBD_{\phi}\) to \(BackDoors\phi\)
11 return\(BackDoors\phi\)
```
**Algorithm 4**A backdoor-based low-overhead computational heuristic (BDLO). ### VSIDS Variants

We chose to exploit backbone and backdoor variables by extending the VSIDS heuristic (A detailed description of the VSIDS heuristic is provided in Appendix C.2, along with a justification for choosing the branching heuristic to improve the solver is given in Appendix B.2). The following is a summary of VSIDS's policy implemented in MapleLCMDistChronoBT-DL-v3 and LSTech:

1. Initialization: Each variable has a floating point number, called activity, which is initialized to 0. 2. Additive bump: Following a conflict analysis phase, the activities of all variables that led to a conflict are additively bumped (increased), typically by 1, if their decision levels are greater than the backtrack level; otherwise, they are bumped by 0.5. 3. Decision: The (unassigned) variable with the highest activity is chosen at each decision. 4. Multiplicative decay: All variables are periodically decremented by multiplying their activities by a constant \(0<Decay<1\) called the multiplicative decay factor. To exploit backbone and backdoor variables, the VSIDS heuristic was extended, specifically, the additive bump policy. We considered the following cases: when to bump, which variables to bump, and with what value to bump. Accordingly, six variants of the VSIDS heuristic were derived: VSIDS_BBsize_restart, VSIDS_BBsize_BBfreq_restart, VSIDS_BBsize_BBfreq_backtrack, VSIDS_BBsize_BBfreq_conflict, VSIDS_BBsize_BBfreq_restart_conflict, and VSIDS_BDsize_restart. Algorithms 5-10 are variants of the VSIDS, and throughout, we highlight only the added policies to the VSIDS implemented in Maple-based series SAT solvers (see Appendix C.2). For all algorithms, all variables' activities are initialized to zero.