- *bmc:* **An ensemble of software verification problems generated using CBMC**
2 verifying the C functions presented in Fig. 3. These two functions are almost identical, apart for a change in line 8, which causes the sat script to overflow. The different instances use different array sizes and different **number of**
unwindings. This dataset represents an ensemble of problems that **are very**
similar and generated by the same process. We use 234 satisfiable and 237 unsatisfiable problems.

- *velev:* **An ensemble of hardware formal verification problems distributed by**
Miroslav Velev3**. These are well studied verification hardware benchmarks.**
This ensemble is not as homogeneous as bmc **because it is a union of many**
small benchmark families. We use 72 satisfiable and 105 unsatisfiable instances.

- *crypto:* **An ensemble of problems that are generated as part of an attack on**
the Bivium stream cipher, presented by Eibach, Pilz and V¨olkel [6]. This ensemble presents some interesting characteristics. While it is generated by a non-random process, the instances are significantly smaller than **common** industrial instances. The satisfiable instances we use were generated with 35 guesses, the unsatisfiable ones were generated with 40 guesses. **The reason** for this discrepancy is that unsatisfiable instances are harder to solve in this benchmark family, and different number of guesses renders the datasets too easy or too hard. We use 139 sat and 300 unsat instances.

- *rand:* **An ensemble of 457 satisfiable and 601 unsatisfiable randomly generated 3-SAT problems with 250 to 450 variables and a clause-to-var ratio of**
4.1 to 5.0.

Some further data about these data sets is presented in Table 1. We would like to draw the reader's attention to the "SD" column. This column presents the standard deviation observed when the problem is solved by all 9 restart strategies. A small value indicates that all restart strategies perform on par on this data set, while a large value indicates that runtimes are scattered.

Each data set is split into training and testing sets. Instances in the **training set are used to train** Msat, Munsat **and the classifier while the instances in**
the testing set are only used to generate the results. We used a *10-fold* **cross**
validation technique after randomly shuffling all instances.

## 4.3 Restart Strategy Portfolio Performance
