120
O. Keszocze et al.
x i in the formula and P (x i = 1) is the probability of assigning variable x i to 1.
P (x i = 1) =
num(x i )
num(x i ) + num(¬x i )
(5.10)
Note that the number of occurrences of a literal in the formula changes during
the course of the algorithm because of the newly added clauses. We experimented
with different probabilities when solving benchmark problems, but were not able
to reach clear results, meaning that for some problems the probabilities according
to Eq. (5.10) performed better and for others the uniform random assignment
outperformed the competitor. The results of this experiments can be found in [14].
Because we were not able to obtain clear results on the benefits of using nonuniform probability heuristics, all experiments in Sect. 5.6 used the uniform random
probability heuristic.
5.4.3 Analysis of Different Scoring Heuristics
Similar to Sect. 5.3.2 we now will analyze the impact of the different heuristics
by using visualizations of search trees that were produced using the heuristics. We
therefore used the MCTS-based CDCL solver with different scoring heuristics to
again solve a pigeon hole instance with 14 holes and in the following will use the
produced search trees to exemplary analyze the impact of the heuristics. Later, in
the experiments section, we will quantify the results of this exemplary analysis with
more data.
As a starting point for the analysis, we will look at the search trees that were
produced using the initially introduced scoring heuristic, i.e., the number of satisfied
clauses after a simulation (f num ). Figure 5.8 shows the search trees produced 30 s
into the solving with an exploration constant of 0.1 and 0.3. We again see that in
both cases the search tree is asymmetric, but the variant with the higher exploration
constant more intensely explored both branches of the root and the variant with the
lower exploration constant was able to exploit its greedy nature to create and prune
more nodes in the branch left of the root.
In comparison, Fig. 5.9 shows the search trees of the same situation when the
f depth heuristic is used instead. We can observe that the share of pruned nodes is
higher for both exploration constants than in the search trees that were produced
using the f num heuristic. This is exactly how the search trees should look like by
design of the heuristic. As f depth was designed to encourage early conflicts, it also
encourages the pruning of nodes near the root, which explains the higher share of
pruned nodes. A second aspect we can observe when comparing the search trees
with an exploration constant of 0.3 is that the search tree that was produced using
the f num heuristic is “more symmetric” than the one that was produced using f depth ,
meaning that the less explored branch of the root contains more nodes and thus the
tree is more balanced. This means that the usage of heuristic f depth led to clearer
O. Keszocze et al.
x i in the formula and P (x i = 1) is the probability of assigning variable x i to 1.
P (x i = 1) =
num(x i )
num(x i ) + num(¬x i )
(5.10)
Note that the number of occurrences of a literal in the formula changes during
the course of the algorithm because of the newly added clauses. We experimented
with different probabilities when solving benchmark problems, but were not able
to reach clear results, meaning that for some problems the probabilities according
to Eq. (5.10) performed better and for others the uniform random assignment
outperformed the competitor. The results of this experiments can be found in [14].
Because we were not able to obtain clear results on the benefits of using nonuniform probability heuristics, all experiments in Sect. 5.6 used the uniform random
probability heuristic.
5.4.3 Analysis of Different Scoring Heuristics
Similar to Sect. 5.3.2 we now will analyze the impact of the different heuristics
by using visualizations of search trees that were produced using the heuristics. We
therefore used the MCTS-based CDCL solver with different scoring heuristics to
again solve a pigeon hole instance with 14 holes and in the following will use the
produced search trees to exemplary analyze the impact of the heuristics. Later, in
the experiments section, we will quantify the results of this exemplary analysis with
more data.
As a starting point for the analysis, we will look at the search trees that were
produced using the initially introduced scoring heuristic, i.e., the number of satisfied
clauses after a simulation (f num ). Figure 5.8 shows the search trees produced 30 s
into the solving with an exploration constant of 0.1 and 0.3. We again see that in
both cases the search tree is asymmetric, but the variant with the higher exploration
constant more intensely explored both branches of the root and the variant with the
lower exploration constant was able to exploit its greedy nature to create and prune
more nodes in the branch left of the root.
In comparison, Fig. 5.9 shows the search trees of the same situation when the
f depth heuristic is used instead. We can observe that the share of pruned nodes is
higher for both exploration constants than in the search trees that were produced
using the f num heuristic. This is exactly how the search trees should look like by
design of the heuristic. As f depth was designed to encourage early conflicts, it also
encourages the pruning of nodes near the root, which explains the higher share of
pruned nodes. A second aspect we can observe when comparing the search trees
with an exploration constant of 0.3 is that the search tree that was produced using
the f num heuristic is “more symmetric” than the one that was produced using f depth ,
meaning that the less explored branch of the root contains more nodes and thus the
tree is more balanced. This means that the usage of heuristic f depth led to clearer