Logo des Repositoriums
 
Textdokument

A Monte Carlo Tree Search Based Conflict-Driven Clause Learning SAT Solver

Lade...
Vorschaubild

Volltext URI

Dokumententyp

Zusatzinformation

Datum

2017

Zeitschriftentitel

ISSN der Zeitschrift

Bandtitel

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.

Beschreibung

Schloeter, Jens (2017): A Monte Carlo Tree Search Based Conflict-Driven Clause Learning SAT Solver. INFORMATIK 2017. DOI: 10.18420/in2017_257. Gesellschaft für Informatik, Bonn. PISSN: 1617-5468. ISBN: 978-3-88579-669-5. pp. 2549-2560. Studierendenkonferenz Informatik 2017 (SKILL 2017). Chemnitz. 25.-29. September 2017

Zitierform

Tags