Non-model-based algorithm portfolios for SAT

Abstract

When tackling a computationally challenging combinatorial problem, one often observes that some solution approaches work well on some instances, while other approaches work better on other instances. This observation has given rise to the idea of building algorithm portfolios [5]. Leyton-Brown et al. [1], for instance, proposed to select one of the algorithms in the portfolio based on some features of the instance to be solved. This approach has been blessed with tremendous success in the past. Especially in SAT, the SATzilla portfolios [7] have performed extremely well in past SAT Competitions [6]. © 2011 Springer-Verlag.