# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
Figure 14: Spearman correlation results between Boolean structural measures and the number of progations on 2002–2020 SAT benchmark instances. Experiments were conducted, as before, on Shaheen II [48] and carried out on satisfiable SAT instances with backbones computed from 2002-2020 SAT benchmark instances (see Figure A1). The decision variables for the first 1000 decisions ran by MapleLCMDistChronoBT-DL-v3 were collected. The percentage of exploited backbones performed by MapleLCMDistChronoBT-DL-v3 for the first 1000 decisions on all 2002-2020 benchmark instances is displayed in Figure A8. Generally, it seems that the percentage of exploited backbones varies more on industrial and crafted benchmark instances than on random ones. In addition, for structured instances, there appears to be a percentage number of instances where all backbone variables are exploited. Furthermore, we analyzed the percentage of exploited backbones for SAT instances that have been solved in less than 1000 decisions for all benchmark categories. Each row in Tables A3-A5 (In the case of crafted instances, we grouped three instances per row for convenience.) identifies an instance, highlighting the number of decisions required to solve it (first column) and the percentage backbone variables exploited (second column). For instances that can be solved in less than 1000 decisions, it is obvious that structured instances exploit most of the backbone variables. On the other hand, less than 50% of backbone variables are exploited for random benchmark instances. ## Appendix C The CDCL Framework and Popular Variable Decision Heuristics

### The CDCL Framework

The CDCL framework is depicted in Algorithm 1. After constraint propagation detects a conflict (lines 3-4), CDCL learns at least one reason for that conflict in the form of a new clause (lines 5 and 6), called learnt clause, which is added to the CNF formula. In this case, the CDCL SAT solver directly backtracks to an earlier level (lines 9-12). The instance is declared unsatisfiable if the backtracked level is zero. In the absence of a conflict, a branching variable is picked and the level of that variable is updated accordingly (lines 18-21). Once all variables are assigned, the formula is satisfied (line 2). In the event that the restart condition is triggered, the SAT solver will restart (lines 13-16). ```
Input:\(\phi\): CNF formula with variables \(x\in X\) Output:\(\mathit{satisfiable}\) and \(\mathit{solution}\), otherwise \(\mathit{unsatisfiable}\)
1 Initialize() while\(\mathit{notAllVariablesAssigned()}\)do
2\((\phi,\mathit{status})\leftarrow\textsc{BooleanConstraintPropagation(}\phi,\mathit{solution})\) if\(\mathit{status}\) is \(\mathit{conflict}\)then
3\((\mathit{lbvel},\mathit{learntClauseVars},\mathit{conflictSideVars})\)\(=\)ConflictAnalysis() //Clauselearning
4\(\mathit{AfterConflictAnalysis(}[\mathit{learntClauseVars},\mathit{conflictSideVars})\) if\(\mathit{lbvel}\) is \(\mathit{equal}\) to \(\mathit{then}\) return\(\mathit{unsatisfiable}\)
5 else
6\(\mathit{solution}\leftarrow\textsc{Backtrack(}\mathit{lbvel},\mathit{solution})\) //Backtrack decisionLevel \(\leftarrow\mathit{lbvel}\) OnUnassign(\(x\)) //Calledwhenvariable\(\mathit{x}\)isunassigned bybacktracking or restart
7
8 elseifrestart condition is triggeredthen
9\(\mathit{solution}\leftarrow\textsc{Backtrack(}0,\mathit{solution})\) //Restart decisionLevel \(\leftarrow\) 0 OnUnassign(\(x\)) //Calledwhenvariable\(\mathit{x}\)isunassigned bybacktracking or restart
10
11 else
12\(x\leftarrow\)PickBranchingVariable() //Branch Onassign(\(x\)) \(decisionLevel\leftarrow\mathit{decisionLevel}+1\) \(solution\leftarrow\mathit{solution}\cup(x,\mathit{value})\)
13
14
15 return(\(\mathit{satisfiable},\mathit{solution}\))
```
**Algorithm 1**CDCL framework. ### The VSIDS Heuristic

VSIDS refers to a class of branching heuristics commonly used in CDCL SAT solvers that rank all the variables in an SAT instance during the run of the solver.