SATzilla is a portfolio-based algorithm selection method for SAT (Satisfiability) problems that uses empirical hardness models to choose among constituent solvers. The approach takes a distribution of problem instances and a set of component solvers, and constructs a portfolio that optimizes an objective function, such as mean runtime or percentage of instances solved. SATzilla07, which was submitted to the 2007 SAT Competition, won three gold, one silver, and one bronze medal. The paper presents an improved version of SATzilla07 that is scalable, fully automated, and integrates local search solvers, predicts performance scores instead of runtime, and uses hierarchical hardness models. The new techniques are demonstrated through extensive experimental results on data sets including instances from the 2007 SAT Competition. The paper discusses the algorithm selection problem, where the goal is to choose the best algorithm for a given instance to minimize a performance objective. The traditional "winner-take-all" approach selects the best algorithm based on average performance, but this can neglect algorithms that perform well on specific instances. Instead, the paper proposes using empirical hardness models to predict an algorithm's runtime on a given instance, based on instance features and the algorithm's past performance. This approach allows for the construction of algorithm portfolios that automatically select the best algorithm for each instance. The paper also discusses algorithm portfolios, which are sets of algorithms that are run in parallel or sequentially to solve a problem instance. The term "algorithm portfolio" was introduced by Huberman et al. (1997) to describe the strategy of running several algorithms in parallel. The paper introduces the concept of (a,b)-of-n portfolios, where a and b define the minimum and maximum number of algorithms executed. The paper also discusses the use of hierarchical hardness models, which take into account different types of SAT instances, and the use of ridge regression for feature selection and model fitting. The paper describes the development of SATzilla07, which was submitted to the 2007 SAT Competition and placed first in three categories and second or third in two further categories. The paper also describes the construction of SATzilla07, including the selection of instances, solvers, and features, and the use of empirical hardness models to predict runtime. The paper evaluates the performance of SATzilla07 on different categories of instances, including RANDOM, HANDMADE, and INDUSTRIAL, and compares it to other solvers. The results show that SATzilla07 performs well across different categories of instances, with significant improvements in runtime and instance solving compared to individual solvers. The paper also discusses the use of hierarchical hardness models and the importance of feature selection in improving the accuracy of empirical hardness models.SATzilla is a portfolio-based algorithm selection method for SAT (Satisfiability) problems that uses empirical hardness models to choose among constituent solvers. The approach takes a distribution of problem instances and a set of component solvers, and constructs a portfolio that optimizes an objective function, such as mean runtime or percentage of instances solved. SATzilla07, which was submitted to the 2007 SAT Competition, won three gold, one silver, and one bronze medal. The paper presents an improved version of SATzilla07 that is scalable, fully automated, and integrates local search solvers, predicts performance scores instead of runtime, and uses hierarchical hardness models. The new techniques are demonstrated through extensive experimental results on data sets including instances from the 2007 SAT Competition. The paper discusses the algorithm selection problem, where the goal is to choose the best algorithm for a given instance to minimize a performance objective. The traditional "winner-take-all" approach selects the best algorithm based on average performance, but this can neglect algorithms that perform well on specific instances. Instead, the paper proposes using empirical hardness models to predict an algorithm's runtime on a given instance, based on instance features and the algorithm's past performance. This approach allows for the construction of algorithm portfolios that automatically select the best algorithm for each instance. The paper also discusses algorithm portfolios, which are sets of algorithms that are run in parallel or sequentially to solve a problem instance. The term "algorithm portfolio" was introduced by Huberman et al. (1997) to describe the strategy of running several algorithms in parallel. The paper introduces the concept of (a,b)-of-n portfolios, where a and b define the minimum and maximum number of algorithms executed. The paper also discusses the use of hierarchical hardness models, which take into account different types of SAT instances, and the use of ridge regression for feature selection and model fitting. The paper describes the development of SATzilla07, which was submitted to the 2007 SAT Competition and placed first in three categories and second or third in two further categories. The paper also describes the construction of SATzilla07, including the selection of instances, solvers, and features, and the use of empirical hardness models to predict runtime. The paper evaluates the performance of SATzilla07 on different categories of instances, including RANDOM, HANDMADE, and INDUSTRIAL, and compares it to other solvers. The results show that SATzilla07 performs well across different categories of instances, with significant improvements in runtime and instance solving compared to individual solvers. The paper also discusses the use of hierarchical hardness models and the importance of feature selection in improving the accuracy of empirical hardness models.