

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

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

All our experiments were conducted on a cluster of 14 Dual Intel Xeon CPUs with EM64T (64-bit) extensions, running at 3.2GHz with 4GB of RAM under Debian GNU/Linux 4.0. By implementing a runtime cutoff of 90 minutes per instance, we managed to complete all experiments in approximately 290 CPU days.

Table 1. **Summary of features of datasets. For each dataset the following details are**
presented: The dataset's classification (Class), the number of instances (Ins.) and its size in MB (all file are zipped). Also, we present the time (in hours) it took for all 9 restart strategies to solve these datasets. We present the **mean time (Mean), the**
standard deviation (SD) and the minimal and maximal time. Runtime cutoff is 5400 seconds and it is the maximal runtime per instance.

| Name Class Ins. Size                        | Runtime                  |                                        |                          |       |      |       |       |
|---------------------------------------------|--------------------------|----------------------------------------|--------------------------|-------|------|-------|-------|
| (MB)                                        | Mean                     | SD                                     | Min                      | Max   |      |       |       |
| bmc                                         | sat                      | 234 4,420.0 154.42 26.41 127.93 213.27 |                          |       |      |       |       |
| unsat 237 1,951.7 113.82 18.59 93.48 155.04 |                          |                                        |                          |       |      |       |       |
| velev                                       | sat                      | 72                                     | 1,866.2                  | 32.68 | 3.74 | 24.77 | 37.87 |
| unsat 105 953.4                             | 70.74                    | 1.64                                   | 68.16                    | 73.29 |      |       |       |
| crypto sat                                  | 139 2.7                  | 140.71 11.54 122.52 164.78             |                          |       |      |       |       |
| unsat 300 5.5                               | 14.19                    | 1.53                                   | 11.61                    | 16.65 |      |       |       |
| rand                                        | sat                      | 457 1.90                               | 76.93 14.98 54.00 105.10 |       |      |       |       |
| unsat 601 2.3                               | 84.82 10.82 70.87 103.56 |                                        |                          |       |      |       |       |

## 4.2 Benchmarks

In this study we used four different distributions of SAT instances. **Instances in** each data set are of various difficulty. We have omitted very easy instances that are solved before the "observation window" terminates.