Abstract
Non-Chronological Backtracking (NCB) has been implemented in every modern CDCL SAT solver since the original CDCL solver GRASP. NCB’s importance has never been questioned. This paper argues that NCB is not always helpful. We show how one can implement the alternative to NCB–Chronological Backtracking (CB)–in a modern SAT solver. We demonstrate that CB improves the performance of the winner of the latest SAT Competition, Maple_LCM_Dist, and the winner of the latest MaxSAT Evaluation Open-WBO.
Cite
CITATION STYLE
Nadel, A., & Ryvchin, V. (2018). Chronological Backtracking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10929 LNCS, pp. 111–121). Springer Verlag. https://doi.org/10.1007/978-3-319-94144-8_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
