5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
121
Fig. 5.8 Search trees produced by the MCTS-based CDCL solver using the f num scoring heuristic
in the first 30 s of solving a pigeon hole instance with 14 holes using an exploration constant of 0.1
(left) and 0.3 (right)
Fig. 5.9 Search trees produced by the MCTS-based CDCL solver using the f depth scoring
heuristic in the first 30 s of solving a pigeon hole instance with 14 holes using an exploration
constant of 0.1 (left) and 0.3 (right)
results on where to expand the search tree and thus one branch of the root node was
more intensely exploited.
Therefore one could argue that the heuristic f depth works better on this example,
because the main goal of the algorithm is to be able to find and exploit areas of
the search space where the heuristic leads to high scores. A more unbalanced tree
means that the algorithm was more successful to do just that.
To further elaborate on this thought, we take a look at the search trees produced
in the same situation while using the f activity heuristic as illustrated in Fig. 5.10. We