Communications of the ACM

with the Calysto static checker. 3 For both of these instance distributions, the runtime of SPEAR with different configurations was predicted with a high degree of accuracy. Our random forest models accurately predicted the empirical hardness of instances, the empirical performance of configurations, and even captured ways in which the two interact.

Take-Away Messages

Statistical methods can characterize the difficulty of solving instances from a given distribution using the best available algorithms—even when those algorithms are extremely complex and traditional theoretical analysis is infeasible. Such EHMs are surprisingly effective in practice, across different hard combinatorial problems, real-world instance distributions, and state-of-the art solvers. An analysis of these models can serve as a starting point for new theoretical investigations into complexity beyond the worst case, by identifying problem features that are predictive of hardness or that suffice to predict an objective function (for example, satisfiability status) directly. In the context of highly parameterized algorithms that span a large space of possible algorithm designs, we have found that it is even possible to predict the runtime of previously untested algorithm designs on previously unseen instances. EHMs have proven useful in a variety of practical applications, including the automatic design of algorithm portfolios, the automatic synthesis of hard benchmark distributions, and the automatic search for a performance-optimizing design in a large algorithm design space. We have written open source software for building EHMs, analyzing them, constructing algorithm portfolios, automatically configuring parameterized algorithms, and more: see http:// www.cs.ubc.ca/labs/beta/Projects/EPMs/.

Acknowledgments

Some work described in this article was performed with additional coauthors: Eugene Nudelman and Yoav Shoham made particularly sustained contributions, and Galen Andrew, Alex Devkar, and Jim McFadden also deserve mention.

References

1. Ahmadizadeh, K., Dilkina, B., Gomes, C. P. and Sabharwal, A. An empirical study of optimization for maximizing diffusion in networks. In Proceedings for Principles and Practice of Constraint Programming

(2010), 514–521.

2. Applegate, D. L. Bixby, R. E., Chvátal, V. and Cook, W.J.

The Traveling Salesman Problem: A Computational Study. Princeton University Press, 2006.

3. Babić, D. and Hu, A.J. Structural abstraction of software verification conditions. In Proceedings for Computer Aided Verification (2007), 366–378.

4. Babić, D. and Hutter, F. Spear theorem prover. Solver description. SAT 2007 Competition.

5. Bishop, C. M. Pattern Recognition and Machine Learning. Springer, 2006.

6. Breiman, L. Random forests. Machine Learning 45, 1

(2001), 5–32.

7. Breiman, L., Friedman, J.H., Olshen, R. and Stone, C. J. Classification and Regression Trees. Wadsworth, Belmont, CA, 1984.

8. Cheeseman, P., Kanefsky, B. and Taylor, W. M. Where the really hard problems are. In Proceedings for International Joint Conference on Artificial Intelligence (1991), 331–337.

9. Eén, N. and Sörensson, N. An extensible SAT-solver.

Theory and Applications of Satisfiability Testing

(2004), 502–518.

10. Friedman, J. Multivariate adaptive regression splines.

Annals of Statistics 19, 1 (1991), 1–141.

11. Heule, M. and Maaren, M.v. march_hi. Solver description, SAT 2009 competition.

12. Hoos, H.H. Programming by optimization. Commun.

ACM 55, 2 (Feb. 2012), 70–80.

13. Hopcroft, J.E., Motwani, R. and Ullman, J.D.

Introduction to Automata Theory, Languages, and Computation. Pearson Education, 2007.

14. Hutter, F. Automated Configuration of Algorithms for Solving Hard Computational Problems.

Ph.D. thesis, University Of British Columbia, Department of Computer Science, Vancouver, Canada (Oct. 2009).

15. Hutter, F., Babić, D., Hoos, H.H. and Hu, A.J. Boosting verification by automatic tuning of decision procedures. In Proceedings for Conference on Formal Methods in Computer-Aided Design (2007), 27–34.

16. Hutter, F., Hamadi, Y., Hoos, H.H., and Leyton-Brown, K. Performance prediction and automated tuning of randomized and parametric algorithms. In

Proceedings for Principles and Practice of Constraint Programming (2006), 213–228.

17. Hutter, F, Hoos, H.H. and Leyton-Brown, K. Automated configuration of mixed integer programming solvers. In

Proceedings for Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (2010), 186–202.

18. Hutter, F, Hoos, H. H. and Leyton-Brown, K. Trade-offs in the empirical evaluation of competing algorithm designs. Annals of Mathematics and Artificial Intelligence 60, (2010), 65–89.

19. Hutter, F, Hoos, H. H. and Leyton-Brown, K. Sequential model-based optimization for general algorithm configuration. In Proceedings for Learning and Intelligent Optimization Conference (2011), 507–523.

20. Hutter, F, Tompkins, D.A. D. and Hoos, H. H. Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In Proceedings for Principles and Practice of Constraint Programming (2002), 233–248.

21. Hutter, F., Xu, L., Hoos, H. H. and Leyton-Brown, K.

Algorithm runtime prediction: Methods and evaluation.

Artificial Intelligence J. 206 (Jan. 2014), 77–111).

22. IBM. CPLEX Optimizer, 2014. http://www-01.ibm. com/software/commerce/optimization/cplex-optimizer/.

23. Johnson, D.S. Random TSP generators for the DIMACS TSP Challenge, 2011; http://dimacs.rutgers. edu/Challenges/TSP/.

24. KhudaBukhsh, A., Xu, L., Hoos, H. H. and Leyton-Brown, K. SATenstein: Automatically building local search SAT sol vers from components. In Proceedings for International Joint Conference on Artificial Intelligence (2009), 517–524.

25. Knuth, D. Estimating the efficiency of backtrack programs. Mathematics of Computation 29, 129

(1975), 121–136.

26. Leyton-Brown, K., Nudelman, E., Andrew, G., McFadden, J. and Shoham. Boosting as a metaphor for algorithm design. In Proceedings for Principles and Practice of Constraint Programming (2003), 899–903.

27. Leyton-Brown, K., Nudelman, E., Andrew, G.,
McFadden, J. and Shoham, Y. A portfolio approach to
algorithm selection. In Proceedings for International
Joint Conference on Artificial Intelligence (2003),
1542–1543.

28. Leyton-Brown, K., Nudelman, E. and Shoham, Y. Learning the empirical hardness of optimization problems: The case of combinatorial auctions. In Proceedings for Principles and Practice of Constraint Programming (2002), 556–572.

29. Leyton-Brown, K., Nudelman, E. and Shoham, Y. Empirical hardness models: Methodology and a case study on combinatorial auctions. Journal of the ACM 56, 4 (2009), 1–52.

30. Leyton-Brown, K., Pearson, M. and Shoham, Y.
Towards a universal test suite for combinatorial
auction algorithms. In Proceedings for ACM
Conference on Electronic Commerce (2000), 66–76.
31. Mitchell, D., Selman, B. and Levesque, H. Hard and
easy distributions of SAT problems. In Proceedings for
Conference on Artificial Intelligence (1992), 459–465.
32. Nudelman, E., Leyton-Brown, K., Andrew, G., Gomes,
C., McFadden, J., Selman, B. and Shoham, Y. Satzilla
0.9. Solver description. SAT Competition, 2003.

33. Nudelman, E. Leyton-Brown, K., Hoos, H.H., Devkar, A. and Shoham, Y. Understanding random SAT: Beyond the clauses-to-variables ratio. In Proceedings for Principles and Practice of Constraint Programming (2004), 438–452.

34. Prasad, M.R., Biere, A. and Gupta, A. A survey of recent advances in SAT-based formal verification. International Journal on Software Tools for Technology Transfer 7, 2 (2005), 156–173.

35. Rice, J.R. The algorithm selection problem. Advances in Computers 15 (1976), 65–118.

36. Selman, B., Levesque, H.J. and Mitchell, D. A new method for solving hard satisfiability problems. In Proceedings for Conference on Artificial Intelligence (1992), 440–446.

37. Vallati, M., Fawcett, C., Gerevini, A.E., Hoos, H.H. and Saetti, A. Generating fast domain-optimized planners by automatically configuring a generic parameterised planner. In Proceedings for Automated Planning and Scheduling Workshop on Planning and Learning (2011), 21–27.

38. Xu, L., Hoos, H.H. and Leyton-Brown, K. Hierarchical hardness models for SAT. In Proceedings for Principles and Practice of Constraint Programming (2007), 696–711.

39. Xu, L., Hoos, H.H. and Leyton-Brown, K. Predicting satisfiability at the phase transition. In Proceedings for Conference on Artificial Intelligence (2012), 584–590.

40. Xu, L., Hutter, F., Hoos, H.H. and Leyton-Brown, K. SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research 32 (June 2008), 565–606.

41. Xu, L., Hutter, F., Hoos, H.H. and Leyton-Brown, K. Evaluating component solver contributions to portfolio-based algorithm selectors. In Proceedings for Theory and Applications of Satisfiability Testing (2012, 228–241.

42. Zarpas, E. Benchmarking SAT solvers for bounded model checking. In Proceedings for Theory and Applications of Satisfiability Testing (2005), 340–354.

Kevin Leyton-Brown ( kevinlb@cs.ubc.ca) is an associate professor in the Department of Computer Science at the University of British Columbia, Canada.