: The Design and Analysis of an Algorithm Portfolio for SAT

It has been widely observed that there is no “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 a per-instance solver portfolio for SAT, SATzilla-07, which uses socalled empirical hardness models to choose among its constituent solvers. We leverage new model-building techniques such as censored sampling and hierarchical hardness models, and demonstrate the effectiveness of our techniques by building a portfolio of state-of-the-art SAT solvers and evaluating it on several widely-studied SAT data sets. Overall, we show that our portfolio significantly outperforms its constituent algorithms on every data set. Our approach has also proven itself to be effective in practice: in the 2007 SAT competition, SATzilla-07 won three gold medals, o...

• Type: Conference
• Year: 2007
• Where: CP
• Authors: Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown
• Keywords: CP 2007, Hardness Models, Programming Languages, SAT Solvers, State-of-the-art Sat Solvers