strategy (*Static-4096***), and the total runtime shows 19.33% improvement over** the average *Random-pick* **strategy. For unsatisfiable instances, it performs worse.** Although it is second amongst the strategies, it is clearly worse than *Luby-512* that solves 6 more instances. Comparing the standard deviation of **these two** data sets in Table 1 does not explain this descripency in performance. Both show large, almost similar, coefficients (sat's standard deviation is 154.42, and its variation coefficient is 0.171 while unsat's standard deviation is 113.82 and its variation coefficient is 0.1633), this indicates a high potential of improvement for both data sets. We conjecture that the reason for the poorer performance lies in the fact that both the classifier, and the runtime models are more **accurate**
for *bmc-sat* than for *bmc-unsat*.

Table 3. Accuracy results for the satisfiability classifier. Figures **represent the percent**
of correctly classified instances.

Class bmc velev crypto **rand**

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

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

SAT 100.00% 97.22% 99.28% **82.49%**
UNSAT 83.54% 82.85% 100.00% **94.51%**
ALL 91.72% 88.70% 99.77% **89.31%**
Table 3 presents the performance of the satisfiability classifier. The figures in the table represent the percent of instances that were predicted correctly. It is important to note that since we did not apply a "winner takes all" approach, in some of the cases where the classification was correct but not with 100% certainty, the wrong model was also considered. We can see that for bmc**, satisfiable**
instances are classifed correctly every time, while unsatisfiable ones are classified correctly only 83.54% of the times. In order to check the influence of these classifaction errors on the performance of *LMPick* for this dataset, we ran another experiment, where we used a classification oracle. *LMPick***'s performance**
is improved, and it solved 224 instances, which are 3 more than the original results. This shows the effect of a good classification technique over the overall performance.

Table 4. Performance of LMPick's chosen restart strategy (sb**) in comparison with** other strategies. The figures represent the percent of strategies that outperform sb for a given data set.

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

In order for *LMPick* **to enhance the solver's performance, runtime estimation**
models need to perform well. Nevertheless, it is not crucial that each model's prediction is accurate. The important factor is the relative order of these predic-