SATzilla: Portfolio-based Algorithm Selection for SAT

Understand

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.
• Building on previous work, we describe SATzilla, an automated approach for constructing per-instance algorithm portfolios for SAT that use so-called 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).