Details
| Originalsprache | Englisch |
|---|---|
| Titel des Sammelwerks | Theory and Applications of Satisfiability Testing – SAT 2015 |
| Herausgeber/-innen | Marijn Heule, Sean Weaver |
| Herausgeber (Verlag) | Springer Verlag |
| Seiten | 215-222 |
| Seitenumfang | 8 |
| ISBN (Print) | 9783319243177 |
| Publikationsstatus | Veröffentlicht - 27 Okt. 2015 |
| Extern publiziert | Ja |
| Veranstaltung | 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015 - Austin, USA / Vereinigte Staaten Dauer: 24 Sept. 2015 → 27 Sept. 2015 |
Publikationsreihe
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Band | 9340 |
| ISSN (Print) | 0302-9743 |
| ISSN (elektronisch) | 1611-3349 |
Abstract
Most modern SAT solvers expose a range of parameters to allow some customization for improving performance on specific types of instances. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC to address this gap by providing a lightweight and easy-to-use toolbox for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter’s importance using the fANOVA framework. To showcase our tool, we apply it to Lingeling and probSAT, two state-of-the-art solvers with very different characteristics.
ASJC Scopus Sachgebiete
- Mathematik (insg.)
- Theoretische Informatik
- Informatik (insg.)
- Allgemeine Computerwissenschaft
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
Theory and Applications of Satisfiability Testing – SAT 2015. Hrsg. / Marijn Heule; Sean Weaver. Springer Verlag, 2015. S. 215-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9340).
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
T1 - SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
AU - Falkner, Stefan
AU - Lindauer, Marius
AU - Hutter, Frank
N1 - Funding information: The author would like to thank the Alexander von Humboldt Foundation of Germany for the financial support with regard to this work.
PY - 2015/10/27
Y1 - 2015/10/27
N2 - Most modern SAT solvers expose a range of parameters to allow some customization for improving performance on specific types of instances. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC to address this gap by providing a lightweight and easy-to-use toolbox for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter’s importance using the fANOVA framework. To showcase our tool, we apply it to Lingeling and probSAT, two state-of-the-art solvers with very different characteristics.
AB - Most modern SAT solvers expose a range of parameters to allow some customization for improving performance on specific types of instances. Performing this customization manually can be challenging and time-consuming, and as a consequence several automated algorithm configuration methods have been developed for this purpose. Although automatic algorithm configuration has already been applied successfully to many different SAT solvers, a comprehensive analysis of the configuration process is usually not readily available to users. Here, we present SpySMAC to address this gap by providing a lightweight and easy-to-use toolbox for (i) automatic configuration of SAT solvers in different settings, (ii) a thorough performance analysis comparing the best found configuration to the default one, and (iii) an assessment of each parameter’s importance using the fANOVA framework. To showcase our tool, we apply it to Lingeling and probSAT, two state-of-the-art solvers with very different characteristics.
UR - http://www.scopus.com/inward/record.url?scp=84950997369&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-24318-4_16
DO - 10.1007/978-3-319-24318-4_16
M3 - Conference contribution
AN - SCOPUS:84950997369
SN - 9783319243177
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 215
EP - 222
BT - Theory and Applications of Satisfiability Testing – SAT 2015
A2 - Heule, Marijn
A2 - Weaver, Sean
PB - Springer Verlag
T2 - 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015
Y2 - 24 September 2015 through 27 September 2015
ER -