Sciweavers

CP
2007
Springer

: The Design and Analysis of an Algorithm Portfolio for SAT

13 years 9 months ago
: 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...
Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CP
Authors Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown
Comments (0)