@phdthesis{Lindauer2014,
  author    = {Lindauer, T. Marius},
  title     = {Algorithm selection, scheduling and configuration of Boolean constraint solvers},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-71260},
  school      = {Universit{\"a}t Potsdam},
  pages     = {ii, 130},
  year      = {2014},
  abstract  = {Boolean constraint solving technology has made tremendous progress over the last decade, leading to industrial-strength solvers, for example, in the areas of answer set programming (ASP), the constraint satisfaction problem (CSP), propositional satisfiability (SAT) and satisfiability of quantified Boolean formulas (QBF). However, in all these areas, there exist multiple solving strategies that work well on different applications; no strategy dominates all other strategies. Therefore, no individual solver shows robust state-of-the-art performance in all kinds of applications. Additionally, the question arises how to choose a well-performing solving strategy for a given application; this is a challenging question even for solver and domain experts. One way to address this issue is the use of portfolio solvers, that is, a set of different solvers or solver configurations. We present three new automatic portfolio methods: (i) automatic construction of parallel portfolio solvers (ACPP) via algorithm configuration,(ii) solving the \$NP\$-hard problem of finding effective algorithm schedules with Answer Set Programming (aspeed), and (iii) a flexible algorithm selection framework (claspfolio2) allowing for fair comparison of different selection approaches. All three methods show improved performance and robustness in comparison to individual solvers on heterogeneous instance sets from many different applications. Since parallel solvers are important to effectively solve hard problems on parallel computation systems (e.g., multi-core processors), we extend all three approaches to be effectively applicable in parallel settings. We conducted extensive experimental studies different instance sets from ASP, CSP, MAXSAT, Operation Research (OR), SAT and QBF that indicate an improvement in the state-of-the-art solving heterogeneous instance sets. Last but not least, from our experimental studies, we deduce practical advice regarding the question when to apply which of our methods.},
  language  = {en}
}
@article{LindauerHoosLeytonBrownetal.2017,
  author    = {Lindauer, Marius and Hoos, Holger and Leyton-Brown, Kevin and Schaub, Torsten H.},
  title     = {Automatic construction of parallel portfolios via algorithm configuration},
  series = {Artificial intelligence},
  volume    = {244},
  journal   = {Artificial intelligence},
  publisher = {Elsevier},
  address   = {Amsterdam},
  issn      = {0004-3702},
  doi       = {10.1016/j.artint.2016.05.004},
  pages     = {272 -- 290},
  year      = {2017},
  abstract  = {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.},
  language  = {en}
}
@article{LindauerHoosHutteretal.2015,
  author    = {Lindauer, Marius and Hoos, Holger H. and Hutter, Frank and Schaub, Torsten H.},
  title     = {An automatically configured algorithm selector},
  series = {The journal of artificial intelligence research},
  volume    = {53},
  journal   = {The journal of artificial intelligence research},
  publisher = {AI Access Foundation},
  address   = {Marina del Rey},
  issn      = {1076-9757},
  pages     = {745 -- 778},
  year      = {2015},
  abstract  = {Algorithm selection (AS) techniques - which involve choosing from a set of algorithms the one expected to solve a given problem instance most efficiently - have substantially improved the state of the art in solving many prominent AI problems, such as SAT, CSP, ASP, MAXSAT and QBF. Although several AS procedures have been introduced, not too surprisingly, none of them dominates all others across all AS scenarios. Furthermore, these procedures have parameters whose optimal values vary across AS scenarios. This holds specifically for the machine learning techniques that form the core of current AS procedures, and for their hyperparameters. Therefore, to successfully apply AS to new problems, algorithms and benchmark sets, two questions need to be answered: (i) how to select an AS approach and (ii) how to set its parameters effectively. We address both of these problems simultaneously by using automated algorithm configuration. Specifically, we demonstrate that we can automatically configure claspfolio 2, which implements a large variety of different AS approaches and their respective parameters in a single, highly-parameterized algorithm framework. Our approach, dubbed AutoFolio, allows researchers and practitioners across a broad range of applications to exploit the combined power of many different AS methods. We demonstrate AutoFolio can significantly improve the performance of claspfolio 2 on 8 out of the 13 scenarios from the Algorithm Selection Library, leads to new state-of-the-art algorithm selectors for 7 of these scenarios, and matches state-of-the-art performance (statistically) on all other scenarios. Compared to the best single algorithm for each AS scenario, AutoFolio achieves average speedup factors between 1.3 and 15.4.},
  language  = {en}
}
@article{HoosLindauerSchaub2014,
  author    = {Hoos, Holger and Lindauer, Marius and Schaub, Torsten H.},
  title     = {claspfolio 2},
  series = {Theory and practice of logic programming},
  volume    = {14},
  journal   = {Theory and practice of logic programming},
  publisher = {Cambridge Univ. Press},
  address   = {New York},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068414000210},
  pages     = {569 -- 585},
  year      = {2014},
  abstract  = {Building on the award-winning, portfolio-based ASP solver claspfolio, we present claspfolio 2, a modular and open solver architecture that integrates several different portfolio-based algorithm selection approaches and techniques. The claspfolio 2 solver framework supports various feature generators, solver selection approaches, solver portfolios, as well as solver-schedule-based pre-solving techniques. The default configuration of claspfolio 2 relies on a light-weight version of the ASP solver clasp to generate static and dynamic instance features. The flexible open design of claspfolio 2 is a distinguishing factor even beyond ASP. As such, it provides a unique framework for comparing and combining existing portfolio-based algorithm selection approaches and techniques in a single, unified framework. Taking advantage of this, we conducted an extensive experimental study to assess the impact of different feature sets, selection approaches and base solver portfolios. In addition to gaining substantial insights into the utility of the various approaches and techniques, we identified a default configuration of claspfolio 2 that achieves substantial performance gains not only over clasp's default configuration and the earlier version of claspfolio, but also over manually tuned configurations of clasp.},
  language  = {en}
}
@misc{HoosLindauerSchaub2014,
  author    = {Hoos, Holger and Lindauer, Marius and Schaub, Torsten H.},
  title     = {claspfolio 2},
  series = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  journal   = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  number    = {606},
  issn      = {1866-8372},
  doi       = {10.25932/publishup-41612},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-416129},
  pages     = {17},
  year      = {2014},
  abstract  = {Building on the award-winning, portfolio-based ASP solver claspfolio, we present claspfolio 2, a modular and open solver architecture that integrates several different portfolio-based algorithm selection approaches and techniques. The claspfolio 2 solver framework supports various feature generators, solver selection approaches, solver portfolios, as well as solver-schedule-based pre-solving techniques. The default configuration of claspfolio 2 relies on a light-weight version of the ASP solver clasp to generate static and dynamic instance features. The flexible open design of claspfolio 2 is a distinguishing factor even beyond ASP. As such, it provides a unique framework for comparing and combining existing portfolio-based algorithm selection approaches and techniques in a single, unified framework. Taking advantage of this, we conducted an extensive experimental study to assess the impact of different feature sets, selection approaches and base solver portfolios. In addition to gaining substantial insights into the utility of the various approaches and techniques, we identified a default configuration of claspfolio 2 that achieves substantial performance gains not only over clasp's default configuration and the earlier version of claspfolio, but also over manually tuned configurations of clasp.},
  language  = {en}
}
@article{HoosKaminskiLindaueretal.2015,
  author    = {Hoos, Holger and Kaminski, Roland and Lindauer, Marius and Schaub, Torsten H.},
  title     = {aspeed: Solver scheduling via answer set programming},
  series = {Theory and practice of logic programming},
  volume    = {15},
  journal   = {Theory and practice of logic programming},
  publisher = {Cambridge Univ. Press},
  address   = {New York},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068414000015},
  pages     = {117 -- 142},
  year      = {2015},
  abstract  = {Although Boolean Constraint Technology has made tremendous progress over the last decade, the efficacy of state-of-the-art solvers is known to vary considerably across different types of problem instances, and is known to depend strongly on algorithm parameters. This problem was addressed by means of a simple, yet effective approach using handmade, uniform, and unordered schedules of multiple solvers in ppfolio, which showed very impressive performance in the 2011 Satisfiability Testing (SAT) Competition. Inspired by this, we take advantage of the modeling and solving capacities of Answer Set Programming (ASP) to automatically determine more refined, that is, nonuniform and ordered solver schedules from the existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings, and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, the fact that our approach can be customized easily enabled us to swiftly adapt it to generate parallel schedules for multi-processor machines.},
  language  = {en}
}
@misc{HoosKaminskiLindaueretal.2015,
  author    = {Hoos, Holger and Kaminski, Roland and Lindauer, Marius and Schaub, Torsten H.},
  title     = {aspeed},
  series = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  journal   = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  number    = {588},
  issn      = {1866-8372},
  doi       = {10.25932/publishup-41474},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-414743},
  pages     = {26},
  year      = {2015},
  abstract  = {Although Boolean Constraint Technology has made tremendous progress over the last decade, the efficacy of state-of-the-art solvers is known to vary considerably across different types of problem instances, and is known to depend strongly on algorithm parameters. This problem was addressed by means of a simple, yet effective approach using handmade, uniform, and unordered schedules of multiple solvers in ppfolio, which showed very impressive performance in the 2011 Satisfiability Testing (SAT) Competition. Inspired by this, we take advantage of the modeling and solving capacities of Answer Set Programming (ASP) to automatically determine more refined, that is, nonuniform and ordered solver schedules from the existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings, and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, the fact that our approach can be customized easily enabled us to swiftly adapt it to generate parallel schedules for multi-processor machines.},
  language  = {en}
}