Tired of looking for new heuristics and data structures for solving NP-complete problems? There is another way to solve these problems fast!

It has been widely observed that there is no single ``dominant'' SAT solver; instead, different solvers perform best on different instances. Rather than following the traditional approach of choosing the best solver for a given class of instances, we advocate making this decision online on a per-instance basis. I will describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use empirical hardness models to choose among their constituent solvers. This approach takes as input a distribution of problem instances and a set of component solvers, and constructs a portfolio optimizing a given objective function (such as mean runtime, percent of instances solved, or score in a competition).

 

SATzilla's excellent performance was independently verified in the 2007 SAT Competition, where it won three gold, one silver and one bronze medal. After describing this family of solvers, I will introduce a new generation of SATzilla solvers that make portfolio construction scalable and completely automated, improve performance by integrating local search solvers as candidate solvers, achieve stronger competition results by predicting performance score instead of runtime, and leverage hierarchical hardness models to take into account different types of SAT instances.