TY - JOUR

T1 - Automatic construction of parallel portfolios via algorithm configuration

AU - Lindauer, Marius

AU - Hoos, Holger

AU - Leyton-Brown, Kevin

AU - Schaub, Torsten

N1 - Funding information: M. Lindauer was supported by the DFG (German Research Foundation) under Emmy Noether grant HU 1900/2-1 and project SCHA 550/8-3 , H. Hoos and K. Leyton-Brown by NSERC Discovery Grants, and T. Schaub by the DFG under project SCHA 550/8-3 , respectively.

PY - 2016/5/20

Y1 - 2016/5/20

N2 - Since 2004, increases in computational power described by Moore's law have substantially been realized in the form of additional cores rather than through faster clock speeds. To make effective use of modern hardware when solving hard computational problems, it is therefore necessary to employ parallel solution strategies. In this work, we demonstrate how effective parallel solvers for propositional satisfiability (SAT), one of the most widely studied NP-complete problems, can be produced automatically from any existing sequential, highly parametric SAT solver. Our Automatic Construction of Parallel Portfolios (ACPP) approach uses an automatic algorithm configuration procedure to identify a set of configurations that perform well when executed in parallel. Applied to two prominent SAT solvers, Lingeling and clasp, our ACPP procedure identified 8-core solvers that significantly outperformed their sequential counterparts on a diverse set of instances from the application and hard combinatorial category of the 2012 SAT Challenge. We further extended our ACPP approach to produce parallel portfolio solvers consisting of several different solvers by combining their configuration spaces. Applied to the component solvers of the 2012 SAT Challenge gold medal winning SAT Solver pfolioUZK, our ACPP procedures produced a significantly better-performing parallel SAT solver.

AB - Since 2004, increases in computational power described by Moore's law have substantially been realized in the form of additional cores rather than through faster clock speeds. To make effective use of modern hardware when solving hard computational problems, it is therefore necessary to employ parallel solution strategies. In this work, we demonstrate how effective parallel solvers for propositional satisfiability (SAT), one of the most widely studied NP-complete problems, can be produced automatically from any existing sequential, highly parametric SAT solver. Our Automatic Construction of Parallel Portfolios (ACPP) approach uses an automatic algorithm configuration procedure to identify a set of configurations that perform well when executed in parallel. Applied to two prominent SAT solvers, Lingeling and clasp, our ACPP procedure identified 8-core solvers that significantly outperformed their sequential counterparts on a diverse set of instances from the application and hard combinatorial category of the 2012 SAT Challenge. We further extended our ACPP approach to produce parallel portfolio solvers consisting of several different solvers by combining their configuration spaces. Applied to the component solvers of the 2012 SAT Challenge gold medal winning SAT Solver pfolioUZK, our ACPP procedures produced a significantly better-performing parallel SAT solver.

KW - Algorithm configuration

KW - Algorithm portfolios

KW - Automated parallelization

KW - Parallel SAT solving

KW - Programming by optimization

UR - http://www.scopus.com/inward/record.url?scp=84970024864&partnerID=8YFLogxK

U2 - 10.1016/j.artint.2016.05.004

DO - 10.1016/j.artint.2016.05.004

M3 - Article

AN - SCOPUS:84970024864

VL - 244

SP - 272

EP - 290

JO - Artificial intelligence

JF - Artificial intelligence

SN - 0004-3702

ER -