5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
125
means that both children of n were equally often visited and thus c 1 and c 2 both
have equally many successors. Thus, the more dist(n) deviates from 0.5, the less
balanced the sub tree of n is.
dist(n) =
max(c 1 .counter, c 2 .counter)
n.counter
Therefore, if V is the set of nodes in the search tree, dist max (V ) =
max n∈V {dist(n)} and dist avg (V ) = avg n∈V {dist(n)} are indicators whether the
search tree is balanced.
2. Let again n be a node of the search tree and c 1 , respectively, c 2 be the children of
n, then diff (n) is an indicator on how balanced the subtree, that is induced by n,
is because a higher value means that one of the children was more often visited.
diff (n) = |c 1 .counter − c 2 .counter|
Again, if V is the set of nodes, then diff max (V ) = max n∈V {diff (n)} and
diff avg (V ) = avg n∈V {diff (n)} are indicators whether the search tree is balanced.
We collected the data for dist avg and dist max , diff avg and diff max in the first
30 s of solving the benchmark problems with the MCTS-based CDCL solver when
using the different introduced scoring heuristics and exploration constants of 0.1,
respectively, 0.3. Given that we aim to use the different scoring heuristics in the
context of the preprocessing approach as introduced in Sect. 5.5, the time interval at
the beginning of the solving process is of special importance and thus we consider
the first 30 s. Note that, when calculating the values for the different measurements,
we only included nodes with two children, as both, the dist and diff statistic, are
only defined for such nodes.
The results for the dist max measurement are illustrated in Fig. 5.11. As already
observed when analyzing the search trees in Sect. 5.4.3, the data confirms that the
f activity heuristic leads to fairly balanced search trees. In fact, for each problem set
the dist max value is close to 0.5 over the whole observed time interval even for the
small exploration constant of 0.1. We conclude that the MCTS-based CDCL solver
does not work as intended when the f activity heuristic is used and will therefore not
include it in the further experiments.
Apart from this observation the data shows that all other heuristics lead to
asymmetric search trees for all used problem sets. For the pigeon hole instance,
we can observe that the heuristic f num leads to a more balanced tree than the other
heuristics, which again fits to the observations of Sect. 5.4.3. This transfers to the
random and crafted and industrial problem sets as the data shows that f num and
f unit lead to slightly more balanced trees than the other heuristics. Nevertheless,
we can conclude that all heuristics apart from f activity succeed to find areas of the
search space to exploit within the first 30 s of the solving for all considered problem
sets.
As a final observation, we can note that for the crafted, respectively, industrial
problems, which are significantly larger than the other considered benchmark
125
means that both children of n were equally often visited and thus c 1 and c 2 both
have equally many successors. Thus, the more dist(n) deviates from 0.5, the less
balanced the sub tree of n is.
dist(n) =
max(c 1 .counter, c 2 .counter)
n.counter
Therefore, if V is the set of nodes in the search tree, dist max (V ) =
max n∈V {dist(n)} and dist avg (V ) = avg n∈V {dist(n)} are indicators whether the
search tree is balanced.
2. Let again n be a node of the search tree and c 1 , respectively, c 2 be the children of
n, then diff (n) is an indicator on how balanced the subtree, that is induced by n,
is because a higher value means that one of the children was more often visited.
diff (n) = |c 1 .counter − c 2 .counter|
Again, if V is the set of nodes, then diff max (V ) = max n∈V {diff (n)} and
diff avg (V ) = avg n∈V {diff (n)} are indicators whether the search tree is balanced.
We collected the data for dist avg and dist max , diff avg and diff max in the first
30 s of solving the benchmark problems with the MCTS-based CDCL solver when
using the different introduced scoring heuristics and exploration constants of 0.1,
respectively, 0.3. Given that we aim to use the different scoring heuristics in the
context of the preprocessing approach as introduced in Sect. 5.5, the time interval at
the beginning of the solving process is of special importance and thus we consider
the first 30 s. Note that, when calculating the values for the different measurements,
we only included nodes with two children, as both, the dist and diff statistic, are
only defined for such nodes.
The results for the dist max measurement are illustrated in Fig. 5.11. As already
observed when analyzing the search trees in Sect. 5.4.3, the data confirms that the
f activity heuristic leads to fairly balanced search trees. In fact, for each problem set
the dist max value is close to 0.5 over the whole observed time interval even for the
small exploration constant of 0.1. We conclude that the MCTS-based CDCL solver
does not work as intended when the f activity heuristic is used and will therefore not
include it in the further experiments.
Apart from this observation the data shows that all other heuristics lead to
asymmetric search trees for all used problem sets. For the pigeon hole instance,
we can observe that the heuristic f num leads to a more balanced tree than the other
heuristics, which again fits to the observations of Sect. 5.4.3. This transfers to the
random and crafted and industrial problem sets as the data shows that f num and
f unit lead to slightly more balanced trees than the other heuristics. Nevertheless,
we can conclude that all heuristics apart from f activity succeed to find areas of the
search space to exploit within the first 30 s of the solving for all considered problem
sets.
As a final observation, we can note that for the crafted, respectively, industrial
problems, which are significantly larger than the other considered benchmark