# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
VSIDS is significantly more effective than other well-known heuristics, particularly when solving unsatisfiable SAT instances [51; 54; 55]. The VSIDS heuristic was originally proposed as part of the Chaff solver [6]. Since then, many variants have been proposed, including VSIDS implemented in MiniSat and the variable move-to-front (VMTF) decision heuristic. In general, VSIDS is characterized by additive bumping, multiplicative decay, and low computation overhead. This work will focus on the VSIDS MiniSat variant implemented in Maple-based series SAT solvers [56]. The policy of VSIDS implemented in Maple-based series SAT solvers [56] is presented in Algorithm 2. All procedures are called as part of the CDCL framework in Algorithm 1. In the initialization procedure (line 1), each variable has a floating point number, called activity, which is initialized to 0 (lines 4-7). Following a conflict analysis phase (line 9), the activities of all variables that led to the learnt clause (including those in the learnt clause) are additively bumped (increased), typically by 1, if their decision levels of variables are greater than the backtrack level, such variables receive more bumps to activity scores (line 14); otherwise, they are bumped by 0.5 (line 16). In addition, all activities of variables are decremented by multiplying them by a constant \(0<\mathit{Decay}<1\) called the multiplicative decay factor (lines 18-20). To select a variable, the (unassigned) variable and polarity with the highest activity are chosen at each decision (line 24). ```
// Called once at the start of the solver. 1 Procedure Initialize()
2...
3 for\(x\in X\) // \(X\) is the set of Boolean variables in \(\phi\). 4 do // Initialize the activity of each variable to be 0. 5
6\(activity_{x}\gets 0\)
7
8... // Called after a learnt clause is generated from conflict analysis. 9 Procedure AfterConflictAnalysis(\(conf\)_lictSideVars\(\subseteq X\), learntClauseVars\(\subseteq X\))
10...
11 for\(x\in(conf\)lictSideVars\(\cup\) learntClauseVars)
12 do
13 if\(x_{decisionLevel}>backtrackLevel\)then
14\(bumpActivity(x,1)\) // Bump: increase the activities of all variables that led to the learnt clause including variables in the learnt clause by 1 if their decision levels are greater than the backtrack level. 15
16 else
17\(bumpActivity(x,0.5)\) // Bump: increase the activities of all variables that led to the learnt clause including variables in the learnt clause by 0.5 if their decision levels are less than the backtrack level. 18 for\(x\in X\)do
19\(decayActivity(x,Decay)\) // Decay: Multiply the activities of every variable by \(0<Decay<1\). 20... // Called when the solver requests the next branching variable. 21 Procedure PickBranchingVariable()
22... returnUnassigned\(x\) with highest activity. ```

**Algorithm 1**VSIDS decision heuristic. All procedures are part of the CDCL framework in Algorithm 2. ## Appendix D Reported Results on Industrial Families

Appendix E Additional



## References

* [PERSON] (1971) [PERSON] The Complexity of Theorem-proving Procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, Shaker Heights, OH, USA, 3-5 May 1971; pp. 151-158. [CrossRef]
* [PERSON] and [PERSON] (1983) [PERSON]; [PERSON] Functional testing of digital systems. In Proceedings of the 20 th Design Automation Conference, DAC '83, Miami Beach, FL, USA, 27-29 June 1983; pp. 207-213. * [PERSON] and [PERSON] (1982) [PERSON]; [PERSON] Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Logics of Programs, Yorktown Heights, NY, USA, 1982; [PERSON]; Springer: Berlin/Heidelberg, Germany, 1982; pp. 52-71. * [PERSON] et al. (2008) [PERSON]; [PERSON]; [PERSON] A Survey of Automated Techniques for Formal Software Verification. _IEEE Trans. Comput. Aided Des. Integr. Circuits Syst._**2008**, _27_, 1165-1178. [CrossRef]
* SAT Competitions (2002) SAT Competitions. 2002.