5 Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning
129
0
5 ,000
10,000 15,000 20,000 25,000 30,000
4
6
Time in ms
Average depth of pruned nodes
0
5 ,000
10,000 15,000 20,000 25,000 30,000
15
20
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
15
20
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0
100
200
300
Time in ms
Average number of pruned nodes
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Fig. 5.15 Data collected when solving all industrial and crafted instances using an exploration
constant of 0.3
fulfills this criteria as it has the lowest values for the average depth of pruned nodes
and the highest values for the total number of pruned nodes, albeit the values are
close especially for the constant of 0.1.
The average number of assignments per decision is high if a large number of
variables is assigned via unit propagation and therefore the heuristic f unit should
score high values for this measurements. Indeed, the heuristic leads to high values
in that regard, whereupon the heuristic f depth still performs slightly better. Per
definition of the heuristics it makes sense that f unit and f depth correlate not
only in the average number of assignments per decisions but for all introduced
measurements as simulation depth is a divisor in the definition of f unit . Additionally,
it seems reasonable that a high number of variables that are assigned due to unit
propagation corresponds to early conflict, i.e., conflicts after a low number of
decisions. Thus, the correlation between the two heuristics is not surprising at all.
We conclude that f unit fulfills its design goal as well.
The heuristics f num and f combined again lead to similar values of the measurements and all problem sets. The correlation is again not surprising because of the
heuristics definitions. We can observe that both heuristics perform among the worst
in every category over the observed time interval. This is not surprising, because the
other heuristics were designed to optimize the introduced measurements, in contrast
to f num and f combined .
As the heuristics performed similarly on the other benchmark sets, the result
indicates that the heuristics, that were introduced in Sect. 5.4, can actually be used
to optimize different characteristics of the behavior of the algorithm.
129
0
5 ,000
10,000 15,000 20,000 25,000 30,000
4
6
Time in ms
Average depth of pruned nodes
0
5 ,000
10,000 15,000 20,000 25,000 30,000
15
20
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
15
20
Time in ms
Average size of learned clauses
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0
100
200
300
Time in ms
Average number of pruned nodes
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Fig. 5.15 Data collected when solving all industrial and crafted instances using an exploration
constant of 0.3
fulfills this criteria as it has the lowest values for the average depth of pruned nodes
and the highest values for the total number of pruned nodes, albeit the values are
close especially for the constant of 0.1.
The average number of assignments per decision is high if a large number of
variables is assigned via unit propagation and therefore the heuristic f unit should
score high values for this measurements. Indeed, the heuristic leads to high values
in that regard, whereupon the heuristic f depth still performs slightly better. Per
definition of the heuristics it makes sense that f unit and f depth correlate not
only in the average number of assignments per decisions but for all introduced
measurements as simulation depth is a divisor in the definition of f unit . Additionally,
it seems reasonable that a high number of variables that are assigned due to unit
propagation corresponds to early conflict, i.e., conflicts after a low number of
decisions. Thus, the correlation between the two heuristics is not surprising at all.
We conclude that f unit fulfills its design goal as well.
The heuristics f num and f combined again lead to similar values of the measurements and all problem sets. The correlation is again not surprising because of the
heuristics definitions. We can observe that both heuristics perform among the worst
in every category over the observed time interval. This is not surprising, because the
other heuristics were designed to optimize the introduced measurements, in contrast
to f num and f combined .
As the heuristics performed similarly on the other benchmark sets, the result
indicates that the heuristics, that were introduced in Sect. 5.4, can actually be used
to optimize different characteristics of the behavior of the algorithm.