Details
| Original language | English |
|---|---|
| Title of host publication | Theory and Applications of Satisfiability Testing – SAT 2015 |
| Editors | Marijn Heule, Sean Weaver |
| Publisher | Springer Verlag |
| Pages | 215-222 |
| Number of pages | 8 |
| ISBN (print) | 9783319243177 |
| Publication status | Published - 27 Oct 2015 |
| Externally published | Yes |
| Event | 18th International Conference on Theory and Applications of Satisfiability Testing, SAT 2015 - Austin, United States Duration: 24 Sept 2015 → 27 Sept 2015 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 9340 |
| ISSN (Print) | 0302-9743 |
| ISSN (electronic) | 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 subject areas
- Mathematics(all)
- Theoretical Computer Science
- Computer Science(all)
- General Computer Science
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
Theory and Applications of Satisfiability Testing – SAT 2015. ed. / Marijn Heule; Sean Weaver. Springer Verlag, 2015. p. 215-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9340).
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › 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 -