Improving SAT Solving Using Monte Carlo Tree Search-based Clause Learning

Beitrag in einem Sammelwerk
(Buchkapitel)


Details zur Publikation

Autorinnen und Autoren: Keszöcze O, Schmitz K, Schloeter J, Drechsler R
Herausgeber: Rolf Drechsler, Mathias Soeken
Titel Sammelwerk: Advanced Boolean Techniques - Selected Papers from the 13th International Workshop on Boolean Problems
Verlag: Springer International Publishing
Jahr der Veröffentlichung: 2019
ISBN: 978-3-030-20322-1
Sprache: Englisch


Abstract

Most modern state-of-the-art Boolean Satisfiability (SAT) solvers are based on the Davis-Putnam-Logemann-Loveland algorithm and exploit techniques like unit propagation and Conflict-Driven Clause
Learning (CDCL). Even though this approach proved to be successful in practice, the success of the Monte Carlo Tree Search (MCTS) algorithm in other domains led to research in using it to solve SAT problems. A
recent approach extended the attempt to solve SAT using a MCTS-based algorithm by adding CDCL. We further analyzed the behavior of that approach by using visualizations of the produced search trees and based
on the analysis introduced multiple heuristics improving different aspects of the quality of the learned clauses. While the resulting solver can be used to solve SAT on its own, the real strength lies in the learned clauses.
By using the MCTS solver as a preprocessor, the learned clauses can be used to improve the performance of existing SAT solvers.


FAU-Autorinnen und Autoren / FAU-Herausgeberinnen und Herausgeber

Keszöcze, Oliver Prof. Dr.
Juniorprofessur für Informatik


Einrichtungen weiterer Autorinnen und Autoren

OHB System AG
Universität Bremen


Zitierweisen

APA:
Keszöcze, O., Schmitz, K., Schloeter, J., & Drechsler, R. (2019). Improving SAT Solving Using Monte Carlo Tree Search-based Clause Learning. In Rolf Drechsler, Mathias Soeken (Eds.), Advanced Boolean Techniques - Selected Papers from the 13th International Workshop on Boolean Problems. Springer International Publishing.

MLA:
Keszöcze, Oliver, et al. "Improving SAT Solving Using Monte Carlo Tree Search-based Clause Learning." Advanced Boolean Techniques - Selected Papers from the 13th International Workshop on Boolean Problems. Ed. Rolf Drechsler, Mathias Soeken, Springer International Publishing, 2019.

BibTeX: 

Zuletzt aktualisiert 2019-22-07 um 11:08

Link teilen