prediction (**LW BE**). The full list of features used is shown in Table 1. All the features used can be calculated in constant time and space with the exception of the WBE which takes O(d) time and space. We therefore only computed WBE every d conflicts where d is the depth recorded at the previous estimate.

To deal with restarts, we wait until the observation window is contained within a single restart. In addition, we exploited estimates from earlier restarts to help improve later estimates. To do this, we augmented the feature vector with all the search cost predictions from previous restarts.

## Experiments

We ran experiments with these two methods using MiniSat (Een and Sorensson 2003). This is a state-of-the-art modern solver, which uses clause learning and clause deletion along with an improved version of VSIDS for variable ordering and a geometrical restart scheme. We used a geometrical factor of 1.5, which is the default for MiniSat. A geometrical factor of 1.2 yielded results of a similar quality. We used three different distributions of SAT problems.

- *rand:* An ensemble of 500 satisfiable and 500 unsatisfiable randomly generated 3-SAT problems with 200 to 550 variables and a clause-to-var ratio of 4.1 to 5.0.

- *bmc:* An ensemble of software verification problems generated by CBMC1 based on a binary search algorithm coded in C. The different examples used different array sizes and different number of loop unwindings. In order to generate satisfiable problems, a faulty piece of code that causes memory overflow was added to the binary search code. These problems create a very homogeneous ensemble of problems. We used 250 satisfiable and 250 unsatisfiable problems.
- fv: An ensemble of hardware formal verification problems distributed by Miroslav Velev2. These problems were produced by the same technique but not for the same underlaying problem, and create an ensemble which is less homogeneous than the previous one. We used 56 satisfiable and 68 unsatisfiable problems.

Since training examples can be scarce, we restricted the size of our training set to no more than 500 problems. For the formal verification problems, we obviously had far less than that. In the first part of our experiments, when restarts were turned off, many of the formal verification problems were not solved. Our results in this part will only compare the other datasets. When restarts were enabled, all three data sets were used. In all experiments we used 10-fold cross validation, never using the same instance for both training and testing purposes. We measured the quality of the predictor by observing the percent of predictions which are within a certain factor of the correct cost (the *error factor*). For example, 80% for error factor 2, denotes that for 80% of the instances, the predicted search cost was within a factor of 2 of the actual search cost.

1http://www.cs.cmu.edu/ modelcheck/cbmc/
2http://www.miroslav-velev.com/sat benchmarks.html

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

We compare our results with the ones obtained by the Progress Bar (PB) (Kokotov and Shlyakhter 2000). In order to make the comparison possible, we instrumented MiniSat with the Progress Bar. Kokotov and Shlyakhter proposed several different heuristics (Constant, HistoricalBasic, Historical-Weighted and Clause Count). We observed similar results with all of these heuristics. We present results here for the Historical-Weighted heuristic since it performs slightly better for these data sets. We used the progress bar's default settings. Note that if the initial search is too deep, the Progress Bar may not provide any estimate.

## Search Without Restarts

Figure 2 compares the quality of the WBE prediction and the Progress Bar prediction over time, for the **rand** dataset.

Both predictors return unbiased results for the unsatisfiable problems and converge to the correct value given enough time. WBE is generally more accurate than PB both for satisfiable and unsatisfiable instances. In all cases, both estimators start by over-estimating the search cost but their prediction improves with time as we backjump over nodes. Figure 3 presents the same data for the bmc dataset. For structured problems, WBE initially over estimates search cost by a large factor (in some cases with by a factor greater than 2 1000). During this period the Progress Bar does not make any prediction as the tree is too deep for it to work, and the "search space left" is estimated to be 100%. At some later point in search, we often observed a sharp improvement in the accuracy of both estimators. Typically this corresponds to search backjumping over an early mistake to a node very close to the root of the tree (or the root itself).

For most instances PB starts returning run-time predictions at this point. The WBE also starts returning good prediction at this point. For unsatisfiable problems in the bmc dataset, this point occurs after 72% of the search (on average), but it appears to occur after a smaller percentage of the search for harder instances. We found a correlation coefficient of
−0.45 between the total size of the search tree and the percent through search where this improvement occurs.