39390
2015
2015
eng
117
142
26
15
article
Cambridge Univ. Press
New York
1
--
--
--
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, 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.
Theory and practice of logic programming
10.1017/S1471068414000015
1471-0684 (print)
1475-3081 (online)
wos:2015
WOS:000349668400005
Hoos, H (reprint author), Univ British Columbia, Dept Comp Sci, Vancouver, BC V5Z 1M9, Canada., hoos@cs.ubc.ca; kaminski@cs.uni-potsdam.de; manju@cs.uni-potsdam.de; torsten@cs.uni-potsdam.de
German Science Foundation (DFG) [SCHA 550/8-3]
<a href="http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-414743">Zweitveröffentlichung in der Schriftenreihe Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe ; 588</a>
Holger Hoos
Roland Kaminski
Marius Lindauer
Torsten Schaub
eng
uncontrolled
algorithm schedules
eng
uncontrolled
answer set programming
eng
uncontrolled
portfolio-based solving
Institut für Informatik und Computational Science
Referiert
Institut für Informatik
41474
2015
2019
eng
26
588
postprint
1
2019-02-11
2019-02-11
--
aspeed
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.
Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
solver scheduling via answer set programming
10.25932/publishup-41474
urn:nbn:de:kobv:517-opus4-414743
1866-8372
online registration
Theory and Practice of Logic Programming 15 (2015) 1, pp. 117–142 DOI 10.1017/S1471068414000015
<a href="http://publishup.uni-potsdam.de/opus4-ubp/frontdoor/index/index/docId/39390">Bibliographieeintrag der Originalveröffentlichung/Quelle</a>
false
true
Keine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Holger Hoos
Roland Kaminski
Marius Lindauer
Torsten Schaub
Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
588
eng
uncontrolled
algorithm schedules
eng
uncontrolled
answer set programming
eng
uncontrolled
portfolio-based solving
Datenverarbeitung; Informatik
open_access
Mathematisch-Naturwissenschaftliche Fakultät
Referiert
Open Access
Cambridge University Press (CUP)
Universität Potsdam
https://publishup.uni-potsdam.de/opus4-ubp/files/41474/pmnr588.pdf