• search hit 1 of 3
Back to Result List

aspeed: Solver scheduling via answer set programming

  • 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, evenAlthough 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.show moreshow less

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Holger Hoos, Roland Kaminski, Marius Lindauer, Torsten SchaubORCiDGND
DOI:https://doi.org/10.1017/S1471068414000015
ISSN:1471-0684 (print)
ISSN:1475-3081 (online)
Parent Title (English):Theory and practice of logic programming
Publisher:Cambridge Univ. Press
Place of publication:New York
Document Type:Article
Language:English
Year of first Publication:2015
Year of Completion:2015
Release Date:2017/03/27
Tag:algorithm schedules; answer set programming; portfolio-based solving
Volume:15
Pagenumber:26
First Page:117
Last Page:142
Funder:German Science Foundation (DFG) [SCHA 550/8-3]
Organizational units:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik und Computational Science
Peer Review:Referiert
Institution name at the time of publication:Mathematisch-Naturwissenschaftliche Fakultät / Institut für Informatik
Notes extern:Zweitveröffentlichung in der Schriftenreihe Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe ; 588