126
O. Keszocze et al.
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Pigeon instance with 10 holes, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Pigeon instance with 10 holes, Exploration Constant 0.3
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Random Set 3, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Random Set 3, Exploration Constant 0.3
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.4
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Crafted and industrial instances, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,
25,000 30,000
0.6
0.8
Time in ms
Average maximum symmetry ratio
Crafted and industrial instances, Exploration Constant 0.3
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Activity of satisfied clauses
Fig. 5.11 Average maximum symmetry ratio over the first 30 s of solving different problem sets
using different exploration constants
problems, more time is needed until the created search trees reach an asymmetric
form. This observation should be considered in the context of the preprocessed
backtracking-based CDCL solver as introduced in Sect. 5.5 when defining the
preprocessing time.
Using the symmetry data we were able to confirm that the scoring heuristics—
apart from the f activity heuristic—can be used by the algorithm while taking
advantage of its ability to create asymmetric search trees. So only the question
whether the scoring heuristics indeed fulfill their design goals remains. In Sect. 5.4.3
we exemplary observed that the f depth heuristic succeeded to prune the search tree
closer to its root node than, for example, the f num heuristic, which is exactly the
intent behind the f depth heuristic. In order to determine whether this also holds
over all considered benchmark problems and for all scoring heuristics that were
introduced in Sect. 5.4, they were used to solve different benchmark problems,
whereupon the following data was collected.
O. Keszocze et al.
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Pigeon instance with 10 holes, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Pigeon instance with 10 holes, Exploration Constant 0.3
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Random Set 3, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Random Set 3, Exploration Constant 0.3
0
5 ,000
10,000 15,000 20,000 25,000 30,000
0.4
0.6
0.8
1
Time in ms
Average maximum symmetry ratio
Crafted and industrial instances, Exploration Constant 0.1
0
5 ,000
10,000 15,000 20,
25,000 30,000
0.6
0.8
Time in ms
Average maximum symmetry ratio
Crafted and industrial instances, Exploration Constant 0.3
Number of satisfied clauses
Clause Length
Conflict Depth
Unit Propagation
Combined
Activity of satisfied clauses
Fig. 5.11 Average maximum symmetry ratio over the first 30 s of solving different problem sets
using different exploration constants
problems, more time is needed until the created search trees reach an asymmetric
form. This observation should be considered in the context of the preprocessed
backtracking-based CDCL solver as introduced in Sect. 5.5 when defining the
preprocessing time.
Using the symmetry data we were able to confirm that the scoring heuristics—
apart from the f activity heuristic—can be used by the algorithm while taking
advantage of its ability to create asymmetric search trees. So only the question
whether the scoring heuristics indeed fulfill their design goals remains. In Sect. 5.4.3
we exemplary observed that the f depth heuristic succeeded to prune the search tree
closer to its root node than, for example, the f num heuristic, which is exactly the
intent behind the f depth heuristic. In order to determine whether this also holds
over all considered benchmark problems and for all scoring heuristics that were
introduced in Sect. 5.4, they were used to solve different benchmark problems,
whereupon the following data was collected.