Evaluating component solver contributions to portfolio-based algorithm selectors

Abstract

Portfolio-based methods exploit the complementary strengths of a set of algorithms and - as evidenced in recent competitions - represent the state of the art for solving many NP-hard problems, including SAT. In this work, we argue that a state-of-the-art method for constructing portfolio-based algorithm selectors, SATzilla, also gives rise to an automated method for quantifying the importance of each of a set of available solvers. We entered a substantially improved version of SATzilla to the inaugural "analysis track" of the 2011 SAT competition, and draw two main conclusions from the results that we obtained. First, automatically-constructed portfolios of sequential, non-portfolio competition entries perform substantially better than the winners of all three sequential categories. Second, and more importantly, a detailed analysis of these portfolios yields valuable insights into the nature of successful solver designs in the different categories. For example, we show that the solvers contributing most to SATzilla were often not the overall best-performing solvers, but instead solvers that exploit novel solution strategies to solve instances that would remain unsolved without them. © 2012 Springer-Verlag.