124
O. Keszocze et al.
Furthermore, we considered harder randomly generated instances that were used
in the SAT competitions of 2007 and 2009. 1 These randomly generated instances
consist of the following problem sets, where each set consists of ten different
instances.
– Random set 1: The satisfiable 3-SAT instances with 360 variables from the SAT
competition of 2009.
– Random set 2: The randomly generated instances in the 2 + p category with
p = 0.7 and 3500 variables from the SAT competition of 2007.
– Random set 3: The randomly generated instances in the 2 + p category with
p = 0.8 and 1295 variables from the SAT competition of 2007.
Finally, we considered larger, especially designed benchmarks as well as industrial benchmarks by again taking instances from the SAT competitions of 2007 and
2009. More precisely, we used the following problem instances:
– q_query_3_l42_lambda
– gss-13-s100
– gss-14-s100
– gss-16-s100
– mod3block_3vars_9gates_restr
– mod3_4vars_6gates
– AProVE07-09
– AProVE07-08
In the following, we will present the results of different experiments we executed
using the introduced problems.
5.6.2 Scoring Heuristics
In Sect. 5.4.3 we were able to exemplarily observe that different heuristics lead
to differently balanced search trees and argued that an asymmetric search tree is
an indicator that the algorithm works as intended when using a heuristic. If the
search tree is asymmetric the algorithm was able to find areas of the search tree,
where the heuristic reached higher values and thus can be exploited. In order
to determine which heuristics can be used to find such areas for the different
benchmark problems, we used them on the problems and collected the following
data:
1. Let n be a node of the search tree and let c 1 and c 2 be the children of n, then
dist(n) as defined in the equation below is an indicator of how balanced the
subtree, that is induced by n, is. If, for example, dist(n) = 0.5 holds, then it
1 http://www.satcompetition.org/.
O. Keszocze et al.
Furthermore, we considered harder randomly generated instances that were used
in the SAT competitions of 2007 and 2009. 1 These randomly generated instances
consist of the following problem sets, where each set consists of ten different
instances.
– Random set 1: The satisfiable 3-SAT instances with 360 variables from the SAT
competition of 2009.
– Random set 2: The randomly generated instances in the 2 + p category with
p = 0.7 and 3500 variables from the SAT competition of 2007.
– Random set 3: The randomly generated instances in the 2 + p category with
p = 0.8 and 1295 variables from the SAT competition of 2007.
Finally, we considered larger, especially designed benchmarks as well as industrial benchmarks by again taking instances from the SAT competitions of 2007 and
2009. More precisely, we used the following problem instances:
– q_query_3_l42_lambda
– gss-13-s100
– gss-14-s100
– gss-16-s100
– mod3block_3vars_9gates_restr
– mod3_4vars_6gates
– AProVE07-09
– AProVE07-08
In the following, we will present the results of different experiments we executed
using the introduced problems.
5.6.2 Scoring Heuristics
In Sect. 5.4.3 we were able to exemplarily observe that different heuristics lead
to differently balanced search trees and argued that an asymmetric search tree is
an indicator that the algorithm works as intended when using a heuristic. If the
search tree is asymmetric the algorithm was able to find areas of the search tree,
where the heuristic reached higher values and thus can be exploited. In order
to determine which heuristics can be used to find such areas for the different
benchmark problems, we used them on the problems and collected the following
data:
1. Let n be a node of the search tree and let c 1 and c 2 be the children of n, then
dist(n) as defined in the equation below is an indicator of how balanced the
subtree, that is induced by n, is. If, for example, dist(n) = 0.5 holds, then it
1 http://www.satcompetition.org/.