5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
127
1. The number of pruned nodes to evaluate which scoring heuristic encourages the
pruning of the search tree.
2. The average depth of pruned nodes, excluding nodes that were only pruned
because they were children of other pruned nodes, as another measurement for
the ability to reduce the search tree near its root.
3. The average size of learned clauses to determine which scoring heuristic benefits
the learning of short clauses.
4. The average number of assigned variables per decision to determine which
scoring heuristic enables the most usage of unit propagation.
Figures 5.12, 5.13, 5.14, and 5.15 exemplary show the values for the four
introduced measurements over the first 30 s of solving the random set 1, respectively,
the industrial and crafted instances with exploration constants of 0.1 and 0.3. We
will now review whether the different heuristics fulfill their design goals.
We first can observe that the heuristic f length , that was designed to encourage the
learning of short clauses, indeed produces the shortest clauses—with restrictions
for the crafted and industrial instances with an exploration constant of 0.3 where the
heuristic does not produce the shortest clauses and all heuristics determine similar
sized clauses—and thus fulfills its design goals in the observed time interval. We
continue with considering the values of the f depth heuristic, which was designed
to encourage early conflicts. Therefore the heuristic should enable the algorithm to
prune nodes near to the root of the search tree, which in turn should lead to a higher
total number of pruned nodes. In the data for random set 1 the heuristic clearly
0
5 ,000
10,000 15,000 20,000 25,000 30,000
20
30
Time in ms
Average depth of pruned nodes
0
5 ,000
10,000 15,000 20,000 25,000 30,000
20
25
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
5
6
7
8
Time in ms
Average number of assignments per decision
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0
1,000
2,000
Time in ms
Average number of pruned nodes
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Fig. 5.12 Data collected when solving all instances in the random set 1 using an exploration
constant of 0.1
127
1. The number of pruned nodes to evaluate which scoring heuristic encourages the
pruning of the search tree.
2. The average depth of pruned nodes, excluding nodes that were only pruned
because they were children of other pruned nodes, as another measurement for
the ability to reduce the search tree near its root.
3. The average size of learned clauses to determine which scoring heuristic benefits
the learning of short clauses.
4. The average number of assigned variables per decision to determine which
scoring heuristic enables the most usage of unit propagation.
Figures 5.12, 5.13, 5.14, and 5.15 exemplary show the values for the four
introduced measurements over the first 30 s of solving the random set 1, respectively,
the industrial and crafted instances with exploration constants of 0.1 and 0.3. We
will now review whether the different heuristics fulfill their design goals.
We first can observe that the heuristic f length , that was designed to encourage the
learning of short clauses, indeed produces the shortest clauses—with restrictions
for the crafted and industrial instances with an exploration constant of 0.3 where the
heuristic does not produce the shortest clauses and all heuristics determine similar
sized clauses—and thus fulfills its design goals in the observed time interval. We
continue with considering the values of the f depth heuristic, which was designed
to encourage early conflicts. Therefore the heuristic should enable the algorithm to
prune nodes near to the root of the search tree, which in turn should lead to a higher
total number of pruned nodes. In the data for random set 1 the heuristic clearly
0
5 ,000
10,000 15,000 20,000 25,000 30,000
20
30
Time in ms
Average depth of pruned nodes
0
5 ,000
10,000 15,000 20,000 25,000 30,000
20
25
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
5
6
7
8
Time in ms
Average number of assignments per decision
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0
1,000
2,000
Time in ms
Average number of pruned nodes
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Fig. 5.12 Data collected when solving all instances in the random set 1 using an exploration
constant of 0.1