The Design and Analysis of an Algorithm Portfolio for SAT

@incollection{citeulike:2793881, abstract = {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 so-called 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, one silver, and one bronze; it is available online at http://www.cs.ubc.ca/labs/beta/Projects/SATzilla .}, author = {Xu, Lin and Hutter, Frank and Hoos, Holger and Leyton-Brown, Kevin }, citeulike-article-id = {2793881}, doi = {10.1007/978-3-540-74970-7\_50}, journal = {Principles and Practice of Constraint Programming – CP 2007}, keywords = {algorithm-portfolio, data-mining-general, meta-learning, sat}, pages = {712--727}, posted-at = {2008-05-13 09:12:42}, priority = {2}, title = {The Design and Analysis of an Algorithm Portfolio for SAT}, url = {http://dx.doi.org/10.1007/978-3-540-74970-7\_50}, year = {2007} }

TY - CHAP ID - citeulike:2793881 L3 - citeulike-article-id:2793881 TI - The Design and Analysis of an Algorithm Portfolio for SAT JF - Principles and Practice of Constraint Programming – CP 2007 SP - 712 EP - 727 N2 - 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 so-called 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, one silver, and one bronze; it is available online at http://www.cs.ubc.ca/labs/beta/Projects/SATzilla . KW - algorithm-portfolio KW - data-mining-general KW - meta-learning KW - sat AU - Xu, Lin AU - Hutter, Frank AU - Hoos, Holger AU - Leyton-Brown, Kevin PY - 2007/// UR - http://dx.doi.org/10.1007/978-3-540-74970-7_50 ER -