s is the size of the current restart. At the end of each observation **window, two**
feature vectors were created. The first (xr**) holds all features from Table 1, while**
the second (ˆxr) is defined as ˆxr = {xr} ∪fw1(x1), fwˆ2(ˆx2)**, . . . , f**wˆr−1(ˆxr−1)	.

Figure 3 compares the two methods. We see that predictions from earlier restarts improve the quality of later predictions but not greatly.

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

## 3.3 Solver Selection Using Lmp

In our final experiment, we used these estimations of search cost **to improve**
solver performance. We used two different versions of MiniSat. Solver A **used** the default MiniSat setting (geometrical factor of 1.5), while solver B **used a**
geometrical factor of 1.2. The challenge is to select which is faster at solving a problem instance.

Table 2 describes the percentage improvement achieved by each of **the following strategies. All values are fractions of the cost of solving the entire dataset,**
picking a solver randomly for each problem, with equal probability. Hence, for each dataset, average(A, B**) = 1:**
- best: **Use an oracle to indicate which solver will solve the problem faster**
(min(A, B)).

- LMP (oracle): **Use both solvers until each reaches the end of its observation**
window and generate a prediction, using two different models for sat and unsat**. Use a satisfiability oracle to indicate which model should be queried.**
Terminate the solver that is predicted to be worse.

- LMP (two models): Use both solvers until each reaches the end of its observation window and generate a prediction, using two different models for sat