122
O. Keszocze et al.
Fig. 5.10 Search trees produced by the MCTS-based CDCL solver using the f activity 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)
can observe that the search trees produced for both exploration constants explored
both branches of the root fairly equally and also led to quite balanced sub trees.
Thus, the algorithm was not able to find areas of the search space such that the
f activity heuristic reached high enough results to exploit. We can conclude that, by
using the f activity heuristic, we do not gain any information about the problem as
the results seem to be similar in all explored areas of the search space and the search
tree is built more or less in a breadth-first search fashion. Therefore, the f activity
heuristic probably is not a good choice for at least this example.
To sum up the analysis, recap that we observed that the f depth heuristic reached
its design goal by successfully pruning more nodes near to the root node than
the other heuristics. In the experiments section we will quantify this observation
and investigate whether the other heuristics reach their design goals as well. We
also observed that the heuristics differ in their ability to create asymmetric search
trees and argued that this ability is an indicator if a heuristic can be successfully
used for a specific problem. In the experiments section we will collect statistics on
the symmetry of the search trees and quantify which heuristics succeed to create
asymmetric trees for different problems.
5.5 Using Multiple Solver Instances for Preprocessing
In the previous sections we designed heuristics that enable an MCTS-based CDCL
solver to actively search for “good” clauses. However, the current implementation
of the algorithm cannot compete with established solvers. Therefore this section
will focus on how to combine the MCTS-based approach with different solvers and
O. Keszocze et al.
Fig. 5.10 Search trees produced by the MCTS-based CDCL solver using the f activity 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)
can observe that the search trees produced for both exploration constants explored
both branches of the root fairly equally and also led to quite balanced sub trees.
Thus, the algorithm was not able to find areas of the search space such that the
f activity heuristic reached high enough results to exploit. We can conclude that, by
using the f activity heuristic, we do not gain any information about the problem as
the results seem to be similar in all explored areas of the search space and the search
tree is built more or less in a breadth-first search fashion. Therefore, the f activity
heuristic probably is not a good choice for at least this example.
To sum up the analysis, recap that we observed that the f depth heuristic reached
its design goal by successfully pruning more nodes near to the root node than
the other heuristics. In the experiments section we will quantify this observation
and investigate whether the other heuristics reach their design goals as well. We
also observed that the heuristics differ in their ability to create asymmetric search
trees and argued that this ability is an indicator if a heuristic can be successfully
used for a specific problem. In the experiments section we will collect statistics on
the symmetry of the search trees and quantify which heuristics succeed to create
asymmetric trees for different problems.
5.5 Using Multiple Solver Instances for Preprocessing
In the previous sections we designed heuristics that enable an MCTS-based CDCL
solver to actively search for “good” clauses. However, the current implementation
of the algorithm cannot compete with established solvers. Therefore this section
will focus on how to combine the MCTS-based approach with different solvers and