5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
117
Fig. 5.7 Search tree
produced by the MCTS-based
CDCL solver in the first 10 s
of solving a pigeon hole
instance with 14 holes. See,
e.g. [5] for a definition of the
pigeon hole problem
when visualizing the search trees that were produced on harder instances (see
Fig. 5.7, for example), the trees still showed the same characteristics as the ones
we analyzed before. In particular, the algorithm was often still able to prune the
search tree near to its root, because of the learned clauses.
As such clauses are valuable because they reduce the search space by a large
factor, the question arises whether one can take advantage of the algorithm’s ability
to learn them. The next sections of the chapter will discuss how the MCTS-based
CDCL solver can be used to actively search for “good” clauses and how to take
advantage of them.
5.4 MCTS Specific Heuristics
While the performance improvement was the main motivation to use CDCL in
combination with MCTS, the usage of CDCL also gives access to more information
about the problem that is to be solved. Obviously, the learned clauses themselves are
additional knowledge about the problem, but there is also the possibility to collect
statistics about the clause learning process. This section introduces MCTS specific
heuristics that exploit the described information.
5.4.1 Scoring Heuristics
In Sect. 5.2, the scoring mechanism of the MCTS-based SAT solver was introduced
and defined to use the number of satisfied clauses as a measurement for the quality
of a simulation. This is very intuitive as the goal of the solver is to satisfy all clauses
117
Fig. 5.7 Search tree
produced by the MCTS-based
CDCL solver in the first 10 s
of solving a pigeon hole
instance with 14 holes. See,
e.g. [5] for a definition of the
pigeon hole problem
when visualizing the search trees that were produced on harder instances (see
Fig. 5.7, for example), the trees still showed the same characteristics as the ones
we analyzed before. In particular, the algorithm was often still able to prune the
search tree near to its root, because of the learned clauses.
As such clauses are valuable because they reduce the search space by a large
factor, the question arises whether one can take advantage of the algorithm’s ability
to learn them. The next sections of the chapter will discuss how the MCTS-based
CDCL solver can be used to actively search for “good” clauses and how to take
advantage of them.
5.4 MCTS Specific Heuristics
While the performance improvement was the main motivation to use CDCL in
combination with MCTS, the usage of CDCL also gives access to more information
about the problem that is to be solved. Obviously, the learned clauses themselves are
additional knowledge about the problem, but there is also the possibility to collect
statistics about the clause learning process. This section introduces MCTS specific
heuristics that exploit the described information.
5.4.1 Scoring Heuristics
In Sect. 5.2, the scoring mechanism of the MCTS-based SAT solver was introduced
and defined to use the number of satisfied clauses as a measurement for the quality
of a simulation. This is very intuitive as the goal of the solver is to satisfy all clauses