# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
Available online: [[http://www.satcompetition.org](http://www.satcompetition.org)]([http://www.satcompetition.org](http://www.satcompetition.org)) (accessed on 19 November 2019). * [PERSON] et al. (2001) [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] Chaff: Engineering an efficient SAT solver. In Proceedings of the 38 th Design Automation Conference (IEEE Cat. No.01 CH37232), Las Vegas, NV, USA, 22 June 2001; pp. 530-535. [CrossRef]
* [PERSON] (1993) [PERSON]; [PERSON]; [PERSON] Optimal speedup of Las Vegas algorithms. _Inf. Process. Lett._**1993**, _47_, 173-180. [CrossRef]
* [PERSON] and [PERSON] (2009) [PERSON]; [PERSON] Predicting Learnt Clauses Quality in Modern SAT Solvers. In Proceedings of the 21 st International Jont Conference on Artificial Intelligence, Pasadena, CA, USA, 11-17 July 2009; IJCAI'09; pp. 399-404. * [PERSON] et al. (2017) [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, Melbourne, Australia 19-25 August 2017; pp. 703-711. [CrossRef]
* [PERSON] et al. (2017) [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] MapleLRB LCM, Maple LCM Dist, MapleLRB LCMoccRestart and Glucose-3.0+width in SAT Competition 2017. In Proceedings of the SAT Competition 2017: Solver and Benchmark Descriptions, Melbourne, Australia, 28 August-1 September 2017; Volume B-2017-1, pp. 25-26. \begin{table}
\begin{tabular}{l c c c c c c c} \hline \hline \multirow{2}{*}{**Family**} & **MapleLCM** & \multirow{2}{*}{**Maple\_**} & \multirow{2}{*}{**LSTech**} & \multirow{2}{*}{**LSTech**} & \multirow{2}{*}{**LSTech**} & \multirow{2}{*}{**LSTech**} & **Relaxed\_** & \\  & **DistChrono** & & & & & **UBBsfrc\_v2** & & **LCMDCBDL\_** & **Kissat\_GB** & **Kissat\_MAB** \\  & **BT-DL-v3** & & & & & **wFeh** & & \\ \hline \hline \multirow{2}{*}{CircuitMultiplie} & 6 & 5 & 7 & 7 & 6 & 6 & 6 \\  & 7 & 7 & 7 & 7 & 7 & 7 & 7 \\  & 7 & 7 & 7 & 7 & 7 & 7 & 7 \\  & 7 & 7 & 7 & 7 & 7 & 7 & 7 \\  & 7 & 7 & 7 & 7 & 7 & 1 & 7 \\  & 5 & 7 & 7 & 7 & 7 & 3 & 7 \\  & 7 & 7 & 7 & 7 & 7 & 7 & 7 \\  & 4 & 4 & 5 & 5 & 6 & 4 & 6 \\ \hline \hline Total & 175 & 177 & 179 & 183 & 178 & 166 & 183 \\ \hline \end{tabular}
\end{table} 
Table 6: _Cont._* [PERSON] and [PERSON] (2018) [PERSON]; [PERSON] Chronological Backtracking. In Proceedings of the Theory and Applications of Satisfiability Testing--SAT 2018, Oxford, UK, 9-12 July 2018; [PERSON], [PERSON], Eds. ; Springer International Publishing: Cham, Switzerland, 2018; pp. 111-121. * [PERSON] et al. (2020) [PERSON]; [PERSON] [PERSON]; [PERSON]; [PERSON] Speeding Up CDCL Inference with Duplicate Learnt Clauses. In Proceedings of the ECAI 2020--24 th European Conference on Artificial Intelligence, Santiago de Compostela, Spain, 29 August-8 September 2020; [PERSON], [PERSON], [PERSON], [PERSON], [PERSON], [PERSON], [PERSON], [PERSON]; IOS Press: Shepherdsville, KY, USA, 2020; Volume 325, pp. 339-346. [CrossRef]
* [PERSON] et al. (2016) [PERSON]; [PERSON]; [PERSON]; [PERSON] Exponential Recency Weighted Average Branching Heuristic for SAT Solvers. In Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA, 12-17 February 2016; AAAI'16; pp. 3434-3440. * [PERSON] et al. (2016) [PERSON]; [PERSON]; [PERSON]; [PERSON] Learning Rate Based Branching Heuristic for SAT Solvers. In Proceedings of the Theory and Applications of Satisfiability Testing--SAT 2016--19 th International Conference, Bordeaux, France, 5-8 July 2016; [PERSON], [PERSON], [PERSON]; Springer: Berlin/Heidelberg, Germany, 2016; Volume 9710, pp. 123-140. [CrossRef]
* [PERSON] and [PERSON] (2020) [PERSON]; [PERSON] Relaxed Backtracking with Rephasing. In Proceedings of the SAT Competition 2020, Alghero, Italy, 3-10 July 2020; Solver and Benchmark Descriptions; University of Helsinki, Department of Computer Science: Helsinki, Finland, 2020, Volume B-2020-1, pp. 15-16. * [PERSON] et al. (1991) [PERSON]; [PERSON]; [PERSON] Where the Really Hard Problems Are.