Details
| Original language | English |
|---|---|
| Pages (from-to) | 117-142 |
| Number of pages | 26 |
| Journal | Theory and Practice of Logic Programming |
| Volume | 15 |
| Issue number | 1 |
| Publication status | Published - 17 Feb 2014 |
| Externally published | Yes |
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.
Keywords
- algorithm schedules, answer set programming, portfolio-based solving
ASJC Scopus subject areas
- Computer Science(all)
- Software
- Mathematics(all)
- Theoretical Computer Science
- Computer Science(all)
- Hardware and Architecture
- Computer Science(all)
- Computational Theory and Mathematics
- Computer Science(all)
- Artificial Intelligence
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: Theory and Practice of Logic Programming, Vol. 15, No. 1, 17.02.2014, p. 117-142.
Research output: Contribution to journal › Article › Research › peer review
}
TY - JOUR
T1 - aspeed: Solver scheduling via answer set programming
AU - Hoos, Holger
AU - Kaminski, Roland
AU - Lindauer, Marius
AU - Schaub, Torsten
PY - 2014/2/17
Y1 - 2014/2/17
N2 - 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.
AB - 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.
KW - algorithm schedules
KW - answer set programming
KW - portfolio-based solving
UR - http://www.scopus.com/inward/record.url?scp=84919865656&partnerID=8YFLogxK
U2 - 10.1017/s1471068414000015
DO - 10.1017/s1471068414000015
M3 - Article
AN - SCOPUS:84919865656
VL - 15
SP - 117
EP - 142
JO - Theory and Practice of Logic Programming
JF - Theory and Practice of Logic Programming
SN - 1471-0684
IS - 1
ER -