Textdokument
A Monte Carlo Tree Search Based Conflict-Driven Clause Learning SAT Solver
Lade...
Volltext URI
Dokumententyp
Dateien
Zusatzinformation
Datum
2017
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Gesellschaft für Informatik, Bonn
Zusammenfassung
Most modern state-of-the-art Boolean Satisfiability (SAT) solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and exploit techniques like unit propagation and Conflict-Driven Clause Learning. Even though this approach proved to be successful in practice and most recent publications focus on improving it, the success of the Monte Carlo Tree Search (MCTS) algorithm in other domains led to research in using it to solve SAT problems. While a MCTS-based algorithm was successfully used to solve SAT problems, a number of established SAT solving techniques like clause learning and parallelization were not included in the algorithm. Therefore this paper presents ways to combine the MCTS-based SAT solving approach with established SAT solving techniques like Conflict-Driven Clause Learning and shows that the addition of those techniques improves the performance of a plain MCTS-based SAT solving algorithm.