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

Keszöcze O, Schmitz K, Schloeter J, Drechsler R (2020)

Publication Language: English

Publication Type: Book chapter / Article in edited volumes

Publication year: 2020

Publisher: Springer International Publishing

Edited Volumes: Advanced Boolean Techniques - Selected Papers from the 13th International Workshop on Boolean Problems

ISBN: 978-3-030-20322-1

URI: https://www.springerprofessional.de/advanced-boolean-techniques/16907760

DOI: 10.1007/978-3-030-20323-8

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.

Authors with CRIS profile

Oliver Keszöcze Juniorprofessur für Informatik

Involved external institutions

Universität Bremen DE Germany (DE) OHB System AG DE Germany (DE)

How to cite

APA:

Keszöcze, O., Schmitz, K., Schloeter, J., & Drechsler, R. (2020). 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, 2020.

BibTeX: Download