Chapter 5
Improving SAT Solving Using Monte
Carlo Tree Search-Based Clause
Learning
Oliver Keszocze, Kenneth Schmitz, Jens Schloeter, and Rolf Drechsler
5.1 Introduction and Related Work
The Boolean Satisfiability (SAT) problem is an NP-complete decision problem,
which has applications in a number of topics like automatic test case generation
[15], formal verification [4], and many more. One main reason for the usage of SAT
in those fields is the existence of efficiently performing solvers.
As Marques-Silva et al. [10] point out, most SAT solvers are based on the
Davis–Putnam–Logemann–Loveland algorithm and use backtracking to determine
a solution. While those solvers proved to be successful in practice, the success of
the Monte Carlo Tree Search (MCTS) algorithm in other domains such as General
Game Playing and different combinatorial problems [1] led to recent work towards
using it to solve SAT, MaxSAT [3], and other related problems [9]. For example,
Previti et al. [13] presented a solver that uses the MCTS algorithm in combination
with classical SAT solving techniques like unit propagation [2]. Their experiments
showed that the MCTS-based approach performed well if the SAT instance has an
underlying structure.
While they had some success to combine the MCTS-based approach with
SAT solving techniques like unit propagation [2], they did not include other
key features of modern state-of-the-art SAT solvers like Conflict-Driven Clause
Learning (CDCL) [11]. Therefore a more recent approach extended the algorithm
by using CDCL [14].
O. Keszocze ()
Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany
e-mail: oliver.keszoecze@fau.de
K. Schmitz · J. Schloeter · R. Drechsler
Institute of Computer Architecture, University of Bremen, Bremen, Germany
e-mail: kenneth@uni-bremen.de; jschloet@uni-bremen.de; drechsler@uni-bremen.de
© Springer Nature Switzerland AG 2020
R. Drechsler, M. Soeken (eds.), Advanced Boolean Techniques,
https://doi.org/10.1007/978-3-030-20323-8_5
107
Improving SAT Solving Using Monte
Carlo Tree Search-Based Clause
Learning
Oliver Keszocze, Kenneth Schmitz, Jens Schloeter, and Rolf Drechsler
5.1 Introduction and Related Work
The Boolean Satisfiability (SAT) problem is an NP-complete decision problem,
which has applications in a number of topics like automatic test case generation
[15], formal verification [4], and many more. One main reason for the usage of SAT
in those fields is the existence of efficiently performing solvers.
As Marques-Silva et al. [10] point out, most SAT solvers are based on the
Davis–Putnam–Logemann–Loveland algorithm and use backtracking to determine
a solution. While those solvers proved to be successful in practice, the success of
the Monte Carlo Tree Search (MCTS) algorithm in other domains such as General
Game Playing and different combinatorial problems [1] led to recent work towards
using it to solve SAT, MaxSAT [3], and other related problems [9]. For example,
Previti et al. [13] presented a solver that uses the MCTS algorithm in combination
with classical SAT solving techniques like unit propagation [2]. Their experiments
showed that the MCTS-based approach performed well if the SAT instance has an
underlying structure.
While they had some success to combine the MCTS-based approach with
SAT solving techniques like unit propagation [2], they did not include other
key features of modern state-of-the-art SAT solvers like Conflict-Driven Clause
Learning (CDCL) [11]. Therefore a more recent approach extended the algorithm
by using CDCL [14].
O. Keszocze ()
Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Germany
e-mail: oliver.keszoecze@fau.de
K. Schmitz · J. Schloeter · R. Drechsler
Institute of Computer Architecture, University of Bremen, Bremen, Germany
e-mail: kenneth@uni-bremen.de; jschloet@uni-bremen.de; drechsler@uni-bremen.de
© Springer Nature Switzerland AG 2020
R. Drechsler, M. Soeken (eds.), Advanced Boolean Techniques,
https://doi.org/10.1007/978-3-030-20323-8_5
107