# Boosting the Performance of CDCL-Based SAT Solvers by Exploiting Backbones and Backdoors
## 3 Related Work
### MapleLCMDistClronoBT-DL-v3 and LSTech
(2009) [PERSON]; [PERSON]; [PERSON] Extending SAT Solvers to Cryptographic Problems. In Proceedings of the Theory and Applications of Satisfiability Testing 2009, Swansea, Wales, UK, 30 June-3 July 2009; Volume 5584, pp. 244-257. * _[PERSON] et al. (2020)_ [PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON]; [PERSON] [PERSON] [PERSON], [PERSON], [PERSON], [PERSON] and [PERSON] entering the SAT Competition 2020. In Proceedings of the SAT Competition 2020: Solver and Benchmark Descriptions, Alghero, Italy, 5-9 July 2020; University of Helsinki, Department of Computer Science: Helsinki, Finland, 2020; Volume B-2020-1, pp. 50-53. * [PERSON] (2015) [PERSON] Between SAT and UNSAT: The Fundamental Difference in CDCL SAT. In Proceedings of the Theory and Applications of Satisfiability Testing--SAT 2015, Austin, TX, USA, 24-27 September 2015; pp. 307-323. * _[PERSON] et al. (2018)_ [PERSON]; [PERSON]_LCM_Dist_ChronoBT: Featuring chronological backtracking. In Proceedings of the SAT Competition 2018: Solver and Benchmark Descriptions, Oxford, UK, 9-12 July 2018; Volume B-2028-1, p. 29. * _[PERSON] et al. (2021)_ [PERSON]; [PERSON]; [PERSON] Improving CDCL via Local Search. In Proceedings of the SAT Competition 2021: Solver and Benchmark Descriptions, Barcelona, Spain, 5-9 July 2021; Volume B-2021-1, p. 42. * _[PERSON] et al. (2021)_ [PERSON]; [PERSON]; [PERSON] Four CDCL solvers based on expLRB, expVSIDS and Glue Bumping. In Proceedings of the SAT Competition 2021: Solver and Benchmark Descriptions, Barcelona, Spain, 5-9 July 2021; Volume B-2021-1, pp. 17-18. * _[PERSON] et al. (2021)_ [PERSON]; [PERSON]; [PERSON] Combining VSIDS and CHB Using Restarts in SAT. In Proceedings of the 27 th International Conference on Principles and Practice of Constraint Programming (CP 2021), online, 25-29 October 2021; Volume 210, pp. 20:1-20:19. [CrossRef]
* [PERSON] and [PERSON] (2001) [PERSON]; [PERSON] _Detecting Inadmissible and Necessary Variables in Large Propositional Formulae_; Technical Report; University of Siena: Siena, Italy, 2001. * _[PERSON] et al. (2002)_ [PERSON]; [PERSON] Searching for Backbones and Fat: A Limit-Crossing Approach with Applications. In Proceedings of the Eighteenth National Conference on Artificial Intelligence, Edmonton, Alberta, Canada, 28 July-1 August 2002; pp. 707-712. * _[PERSON] et al. (2018)_ [PERSON]; [PERSON] A Preference-Based Approach to Backbone Computation with Application to Argumentation. In Proceedings of the 33 rd Annual ACM Symposium on Applied Computing, Pau, France, 9-13 April 2018; Association for Computing Machinery: New York, NY, USA, 2018; SAC '18; pp. 896-902. [CrossRef]
* _[PERSON] et al. (2020)_ [PERSON]; [PERSON]; [PERSON] Optimizing Backbone Filtering. _Sci. Comput. Program._**2020**, _187_, 102374. [CrossRef]
* _[PERSON] (2017)_ [PERSON] Improving SAT-Solving with Machine Learning. In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, Seattle, WA, USA, 8-11 March 2017; Association for Computing Machinery: New York, NY, USA, 2017; SIGCSE '17; pp. 787-788. [CrossRef]
* _[PERSON] et al. (2009)_ [PERSON]; [PERSON]; [PERSON]; [PERSON]; [PERSON] Backdoors to Combinatorial Optimization: Feasibility and Optimality. In Proceedings of the Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 6 th International Conference, CPAIOR 2009, Pittsburgh, PA, USA, 27-31 May 2009; pp. 56-70. [CrossRef]
* _[PERSON] et al. (2003)_ [PERSON]; [PERSON]; [PERSON] MIPLIB 2003. _Oper. Res. Lett._**2006**, 34, 361-372. [CrossRef]
* _[PERSON] et al. (2005)_ [PERSON]; [PERSON] A Backbone-Based Co-evolutionary Heuristic for Partial MAX-SAT. In Proceedings of the Artificial Evolution, 7 th International Conference, Evolution Artificielle, EA 2005, Lille, France, 26-28 October 2005; Revised Selected Papers; [PERSON] [PERSON], [PERSON] [PERSON], [PERSON], [PERSON], [PERSON], [PERSON]; Springer: Berlin/Heidelberg, Germany, 2005; Volume 3871, pp. 155-166. [CrossRef]
* _[PERSON] et al.