based on the Weighted Backtrack Estimator [5]. This estimates search tree size using the weighted sum:
Pd∈D prob(d)(2 P
d+1−1)
d∈D prob(d) where prob(d) = 2−d and D **is the**
multiset of branches lengths visited. In [3], we extended WBE to support conflict driven backjumping. As the new method requires O(d**) time and space, we**
only compute it every d **conflicts. To deal with quick restarts, we wait until the**
observation window fits within a single restart. In addition, we exploit **estimates** from earlier restarts by augmenting the feature vector with all the search cost predictions from previous restarts.

## 3 Experiments

We ran experiments using MiniSat [2], a state-of-the-art solver with **clause learning, an improved version of VSIDS 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 gave similar results. We used three different ensembles of problems.

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

- bmc: 250 satisfiable and 250 unsatisfiable software verification problems generated by CBMC1**for on a binary search algorithm, using different array sizes**
and number of loop unwindings. To generate satisfiable problems, faulty code that causes memory overflow was added. These problems create a **very homogeneous ensemble.**
- fv: 56 satisfiable and 68 unsatisfiable hardware verification problems distributed by Miroslav Velev2**. This is less homogeneous than the other ensembles.**
Since training examples can be scarce, we restricted our training set to no more than 500 problems, though we had far fewer for the hard verification problems. In the first part of our experiments, when restarts were turned **off, many of the** hardware 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 prediction quality by observing the percentage of predictions 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 cost.

## 3.1 Search Without Restarts

We queried our predictor at different points of the search, ranging **from 2000 to** 50000 backtracks. Comparisons of the performance of LMP for the rand and bmc 1
**http://www.cs.cmu.edu/ modelcheck/cbmc/**
2 http://www.miroslav-velev.com/sat benchmarks.html