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.
Holger H. Hoos ( hoos@cs.ubc.ca) is a professor in the
Department of Computer Science at the University of
British Columbia, Canada.
Frank Hutter is ( fh@cs.uni-freiburg.de) Emmy Noether
Research Group Lead, Department of Computer Science,
at the University of Freiburg, Germany.
Lin Xu ( xulin730@cs.ubc.ca) is a Ph.D. student in the
Department of Computer Science at the University of
British Columbia, Canada.
Copyright held by Owner/Author(s). Publication rights
licensed to ACM. $15.00.