nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Chronological Backtracking

verfasst von : Alexander Nadel, Vadim Ryvchin

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2018

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Machine Learning-Based Restart Policy for CDCL SAT Solvers

Nächstes Kapitel Centrality-Based Improvements to CDCL Heuristics

In the standard algorithm, cl is always equal to the current decision level, but, as we shall see, that is not the case for CB.

Ansotegui, C., Bacchus, F., Järvisalo, M., Martins, R. (eds.): MaxSAT evaluation 2017: solver and benchmark descriptions, Department of Computer Science Series of Publications B. University of Helsinki, vol. B-2017-2 (2017)

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37CrossRef

Frost, D., Dechter, R.: In search of the best constraint satisfaction search. In: AAAI, pp. 301–306 (1994)

Heule, M., Järvisalo, M., Balyo, T.: SAT competition (2017). https://baldur.iti.kit.edu/sat-competition-2017/

Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 343–356. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_27CrossRefMATH

Luo, M., Li, C.-M., Xiao, F., Manyà, F., Lü, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Sierra, C. (ed.), Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence IJCAI 2017, Melbourne, Australia, 19–25 August 2017, pp. 703–711 (2017). ijcai.org

Nadel, A., Ryvchin, V.: Chronological backtracking: solvers. goo.gl/ssukuu

Neves, M., Martins, R., Janota, M., Lynce, I., Manquinho, V.: Exploiting resolution-based representations for MaxSAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 272–286. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_20CrossRef

10.

Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72788-0_28CrossRef

11.

Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Comput. Intell. 9(3), 268–299 (1993)CrossRef

12.

Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. 2, pp. 131–153

13.

Marques Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD, pp. 220–227 (1996)

14.

Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_36CrossRef

Titel: Chronological Backtracking
verfasst von: Alexander Nadel
Vadim Ryvchin
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2018
Print ISBN: 978-3-319-94143-1

Electronic ISBN: 978-3-319-94144-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94144-8_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"