130
O. Keszocze et al.
Overall, the experiments showed that it is possible to configure the MCTS-based
CDCL solver to optimize different criteria—especially the learning of clauses that
allow the pruning of the search tree near its root. As we additionally saw that
all heuristics—apart from the f activity heuristic—enable the algorithm to find and
exploit areas of the search space where the respective heuristics lead to high values
within the first 30 s of the solving, we conjecture that the algorithm may be able
to determine useful information about the problems and their search space in little
time. In the following section we use experiments in order to determine, whether this
can be exploited using the preprocessing approach as introduced in Sect. 5.5. For
the experiments the heuristics f depth , f length , f unit , and f num will be used. The first
three were selected, because the experiments that were introduced in this sections
confirmed their ability to optimize their measurement and f num was selected in order
to experiment with at least one “greedy” heuristic and because it performed better
than f combined in most categories and experiments.
5.6.3 Using the MCTS-Based Solver as Preprocessor
In this section, we evaluate the impact of the preprocessing as introduced in Sect. 5.5
on the solving time of a third-party SAT solver. We used all benchmark problems
that were introduced in Sect. 5.6.1. As a solver, Sat4j [6] was used. All experiments
were executed at least thirty times and the following results are the average solving
time over all executions. The results of the experiments can been found in Table 5.1,
where column improvement states whether an actual improvement (values > 1) was
achieved and the results of the randomly generated test sets are averages over the
solving time for all contained instances.
As discussed previously, the preprocessor should be run for differently large time
spans in order to account for the different sizes and difficulties of the considered
benchmarks sets. Therefore we used a small preprocessing time of 250 ms for
the problem sets random SAT and random UNSAT and can observe that the
preprocessing led to a significant speedup for the first set and at least did not
(significantly) slow down the solving of the second set.
For the more difficult pigeon hole instances, we used a preprocessing time of 1 s.
The upper part of Table 5.1 shows that the preprocessed instances were solvable in
shorter time in two out of three cases.
To solve the larger and more difficult remaining sets of randomly generated
instances, a larger preprocessing time of 2 s was used and achieved a speedup in
for each set.
Finally, the significantly larger and more difficult crafted, respectively, industrial
instances were solved using a preprocessing time of 10 s. The lower part of Table 5.1
shows that in the majority of the cases the preprocessed instances could be solved
in shorter time.
O. Keszocze et al.
Overall, the experiments showed that it is possible to configure the MCTS-based
CDCL solver to optimize different criteria—especially the learning of clauses that
allow the pruning of the search tree near its root. As we additionally saw that
all heuristics—apart from the f activity heuristic—enable the algorithm to find and
exploit areas of the search space where the respective heuristics lead to high values
within the first 30 s of the solving, we conjecture that the algorithm may be able
to determine useful information about the problems and their search space in little
time. In the following section we use experiments in order to determine, whether this
can be exploited using the preprocessing approach as introduced in Sect. 5.5. For
the experiments the heuristics f depth , f length , f unit , and f num will be used. The first
three were selected, because the experiments that were introduced in this sections
confirmed their ability to optimize their measurement and f num was selected in order
to experiment with at least one “greedy” heuristic and because it performed better
than f combined in most categories and experiments.
5.6.3 Using the MCTS-Based Solver as Preprocessor
In this section, we evaluate the impact of the preprocessing as introduced in Sect. 5.5
on the solving time of a third-party SAT solver. We used all benchmark problems
that were introduced in Sect. 5.6.1. As a solver, Sat4j [6] was used. All experiments
were executed at least thirty times and the following results are the average solving
time over all executions. The results of the experiments can been found in Table 5.1,
where column improvement states whether an actual improvement (values > 1) was
achieved and the results of the randomly generated test sets are averages over the
solving time for all contained instances.
As discussed previously, the preprocessor should be run for differently large time
spans in order to account for the different sizes and difficulties of the considered
benchmarks sets. Therefore we used a small preprocessing time of 250 ms for
the problem sets random SAT and random UNSAT and can observe that the
preprocessing led to a significant speedup for the first set and at least did not
(significantly) slow down the solving of the second set.
For the more difficult pigeon hole instances, we used a preprocessing time of 1 s.
The upper part of Table 5.1 shows that the preprocessed instances were solvable in
shorter time in two out of three cases.
To solve the larger and more difficult remaining sets of randomly generated
instances, a larger preprocessing time of 2 s was used and achieved a speedup in
for each set.
Finally, the significantly larger and more difficult crafted, respectively, industrial
instances were solved using a preprocessing time of 10 s. The lower part of Table 5.1
shows that in the majority of the cases the preprocessed instances could be solved
in shorter time.