and unsat. Query both models and use the geometric mean as the prediction3**. Terminate the solver that is predicted to be worse.**
These results show that for satisfiable problems, where solver performance varies most, our method reduces the total cost. For unsatisfiable problems, where solver performance does not vary as much, our method does not improve search cost. However, as performance does not change significantly on unsatisfiable instances, the overall impact of our method on satisfiable and unsatisfiable problems is positive.

| Dataset     | Best LMP (oracle) LMP(two models)   |       |       |       |
|-------------|-------------------------------------|-------|-------|-------|
| rand sat    | 0.591                               | 0.930 | 0.895 |       |
| unsat 0.925 | 1.009                               | 1.014 |       |       |
| fv          | sat                                 | 0.333 | 0.828 | 0.832 |
| unsat 0.852 | 1.006                               | 1.033 |       |       |
| bmc         | sat                                 | 0.404 | 0.867 | 0.864 |
| unsat 0.828 | 0.997                               | 1.004 |       |       |

Table 2. **Improvement in total search cost using different schemes**

## References

1. Aloul, F., Sierawski, B., Sakallah, K.: Satometer: How much have we searched? In Design Automation Conf.,IEEE (2002) 737-742.

2. Een, N., Sorensson, N.: An extensible SAT-solver. Theory **and Applications of Satisfiability Testing, (2003), 502-518** 3. Haim, S., Walsh, T.: SAT Solving Cost Estimation using Online Techniques, Technical Report 0805, UNSW, Australia, February 2008 4. Horvitz, E., Ruan, Y., Gomes, C., Kautz, H., Selman, B., Chickering, M.: A Bayesian approach to tackling hard computational problems. Proc. the 17th Conf. on Uncertainty in Artificial Intelligence (UAI-2001), (2001)
5. Kilby, P., Slaney, J., Thibaux, S., Walsh, T.: Estimating **Search Tree Size. Proc. of**
the 21st National Conf. of Artificial Intelligence, AAAI, (2006)
6. Kokotov, D., Shlyakhter, I. Progress bar for sat solvers. **Unpublished manuscript,**
http://sdg.lcs.mit.edu/satsolvers/progressbar.html. **2000.**
7. Leyton-Brown, K., Nudelman, E., Shoham, Y.: Learning the **Empirical Hardness**
of Optimization Problems: The Case of Combinatorial Auctions. Proc. of the 8th Int. Conf. on Principles and Practice of Constraint Programming, Springer-Verlag,
(2002) 556-572 8. Samulowitz, H., Memisevic, R.: Learning to Solve QBF. In Proc. of 22nd Conf. on Artificial Intelligence (AAAI07), (2007)
9. Xu, L., Hoos, H.H., Leyton-Brown, K.: Hierarchical Hardness Models for SAT Principles and Practice of Constraint Programming, (2007), 696-711