

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

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

PB 3.8 6.8 8.9 WBE 3.4 5.5 5.9 LMP 40.7 68.7 85.8 PB 4.9 10.3 12.8 WBE 4.9 10.3 13.8 LMP 36.9 68.5 93.6

| x2   | x4   | x8   |
|------|------|------|

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

PB 0.9 2.6 4.9

WBE 2.2 7.8 14.4

LMP 39.7 71.3 86.6

PB 3.7 7.4 15.5

WBE 12.7 29.4 47.3

LMP 92.0 100.0 100.0

Table 2: Percentage of estimates within error factor after 2000 backtracks

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

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

In order to compare the quality of prediction of WBE, PB
and LMP, we generated an estimate after a constant time, regardless of the true size of the problem. In all cases the estimate generated by LMP was superior to those generated by WBE and PB. Comparisons of the performance of those three methods after 2000 and 35000 backtracks are shown in tables 2 and 3 respectively. Satisfiable problems are harder to predict for all methods, due to the abrupt way in which search terminates with open nodes. The linear model deals better with random problems than crafted ones. We conjecture this is due to greater balance in the search tree. WBE performs better than PB for unstructured problems, while they perform similarly for structured instances. The significant improvement of both PB and WBE for structured problems after 35000 backtracks is due to the fact that easier instances are already converging rapidly on the correct answer.

Since we observe very different behaviour with satisfiable and unsatisfiable instances, we trained models on each type of instance separately. With a new (non-training) instance, we may not know if it satisfiable or unsatisfiable. Indeed, the point of search is often to decide this. Given a problem of unknown satisfiability, we therefore queried both models and returned the geometrical mean of the two estimates.

Figures 4 and 5 compare using the geometric mean of the two models and using an oracle to decide which model to query for the **rand** and bmc datasets respectively. We see that the geometric mean returns reasonable predictions. Alternatively we could train with just one model using both satisfiable and unsatisfiable instances. The performance is similar to the geometric mean of the two models (it is a bit better for sat problems and a bit worse for **unsat** problems)
but is sensitive to the proportion of satisfiable and unsatisfiable instances.