SATzilla is an automated approach for constructing per-instance algorithm portfolios for SAT, using empirical hardness models to select the best solver for each instance. The approach inputs a distribution of problem instances and a set of component solvers, and constructs a portfolio that optimizes a given objective function (such as mean runtime, percent of instances solved, or competition score). The performance of SATzilla was independently verified in the 2007 SAT Competition, where it won three gold, one silver, and one bronze medal. This paper extends SATzilla by making portfolio construction scalable and fully automated, integrating local search solvers as candidate solvers, predicting performance scores instead of runtime, and using hierarchical hardness models that consider different types of SAT instances. The effectiveness of these new techniques is demonstrated through extensive experimental results on various datasets, including instances from the most recent SAT competition.SATzilla is an automated approach for constructing per-instance algorithm portfolios for SAT, using empirical hardness models to select the best solver for each instance. The approach inputs a distribution of problem instances and a set of component solvers, and constructs a portfolio that optimizes a given objective function (such as mean runtime, percent of instances solved, or competition score). The performance of SATzilla was independently verified in the 2007 SAT Competition, where it won three gold, one silver, and one bronze medal. This paper extends SATzilla by making portfolio construction scalable and fully automated, integrating local search solvers as candidate solvers, predicting performance scores instead of runtime, and using hierarchical hardness models that consider different types of SAT instances. The effectiveness of these new techniques is demonstrated through extensive experimental results on various datasets, including instances from the most recent SAT competition.