Algorithm selection, scheduling and configuration of Boolean constraint solvers

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Potsdam

Year

2015

Author dc:creator

• Lindauer, T. Marius

Contributors dc:contributor

• Schaub, Torsten
• Hoos, Holger

• algorithm configuration
• algorithm scheduling
• algorithm selection
• parallel solving
• Boolean constraint solver
• Algorithmenselektion
• Algorithmenablaufplanung
• Algorithmenkonfiguration
• paralleles Lösen

Statement dc:rights

• CC-BY-NC-SA - Namensnennung, nicht kommerziell, Weitergabe zu gleichen Bedingungen 4.0 International

Repository record source_url

https://publishup.uni-potsdam.de/frontdoor/index/index/docId/7126

OAI identifier oai:identifier

oai:kobv.de-opus4-uni-potsdam:7126