tions. We would prefer the chosen strategy (sb**) to be amongst the best strategies** for that instance. Table 4 demonstrates the quality of the chosen **strategy** sb. The table presents the percentage of strategies that outperform sb**. This table** shows that in all cases sb **is better than picking a random strategy, and that for**
the *crypto-unsat* **instances it performs very well.**
The difference in the performance on the *crypto-sat* **data set is not easily**
explained by the data presented so far. While both the classifier and **runtime**
prediction models perform better than on the *velev-sat***, the overall performance**
is worse. We conjecture that the cause of this difference is the differing likelihood of an instance being solved by multiple strategies.

![0_image_0.png](0_image_0.png) 

Figure 4 compares the 3 non-random satisfiable data sets. In Fig. 4(a) bars represent the percent of instances in the data set that were solved within the cutoff time by each number of strategies. There is a clear difference **between**
crypto-sat **and the other 2 data sets. While for both industrial verification based**
data sets, most instances were solved by the majority of strategies, for *crypto-sat* many of the instances are solved by a small set of strategies. The effect of this difference is demonstrated in Fig. 4(b). This plot presents the probability of a randomly picked instance being solved within the cutoff time given the quality of selected strategy. From left to right, the picked strategy shift from best to worse. If *LMPick* **picks one of the the two best strategies, the probability of**
all three data sets is quite similar, but when the chosen strategy is 3rd or 4th, the probability of solving a *crypto-sat* **instance drops significantly compared to**
the other two. Many instances in the *crypto-sat* data set are only solved within