Document Open Access Logo

Sustainable Benchmarking Tool (Tool Paper)

Authors Ashlin Iser , Marie Anastacio , Théo Matricon , Laurent Simon , Holger H. Hoos

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.36.pdf
  • Filesize: 0.73 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software performance
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Sustainability
  • Empirical performance comparison
  • Benchmarking
  • Problem instance selection

Metrics

Abstract

Solvers for NP-hard problems from areas such as automated reasoning or optimisation are complex systems in which many different components interact. The performance of these solvers is the result of an intricate interplay between implementation details, algorithmic concepts and heuristics. This, alongside the complexity of the problem instances to be solved, makes it challenging to assess the effect of a single idea on the overall performance of a given solver. It is therefore not only crucial, but also challenging to evaluate the performance impact of new ideas. Existing reliable evaluation methods require large sets of diverse benchmark instances and considerable amounts of computing resources. This makes empirical evaluation a bottleneck for solver development, as it is time-consuming and energy-intensive, often requiring several CPU years of computation to evaluate the impact of a single idea. In recent years, this bottleneck has led to the development of data-driven approaches that can dynamically select a smaller number of instances that provide sufficient statistical evidence to evaluate the relative performance of a given set of solvers. However, these methods are typically not easily accessible. In this work, we present a tool that implements these methods and makes them readily accessible to solver developers, thus enabling them to obtain swifter feedback on their ideas.

Cite As Get BibTex

Ashlin Iser, Marie Anastacio, Théo Matricon, Laurent Simon, and Holger H. Hoos. Sustainable Benchmarking Tool (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 36:1-36:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.36

Author Details

Ashlin Iser
  • Karlsruhe Institute of Technology, Germany
Marie Anastacio
  • AIM, RWTH Aachen University, Germany
Théo Matricon
  • Univ. Rennes, Inria, CNRS, IRISA, France
Laurent Simon
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
Holger H. Hoos
  • AIM, RWTH Aachen University, Germany
  • LIACS, Leiden University, The Netherlands
  • University of British Columbia, Vancouver, Canada

Funding

This work has been made possible by the Randomised Optimisation Algorithms Research Network (ROAR-NET), CA22137, COST Action (European Cooperation in Science and Technology).
  • Hoos, Holger H.: Alexander von Humbold professorship.

Supplementary Materials

References

  1. Josep Alòs, Carlos Ansótegui, Josep M. Salvia, and Eduard Torres. OptiLog V2: Model, Solve, Tune and Run. In International Conference on Theory and Applications of Satisfiability Testing (SAT), 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.25.
  2. Marie Anastacio, Théo Matricon, and Holger Hoos. Instance selection for configuration performance comparison. In ECMLPKDD Workshop on Meta-Knowledge Transfer, pages 11-23. PMLR, 2022. Google Scholar
  3. Tomas Balyo, Marijn Heule, Ashlin Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Helsinki, 2023. Google Scholar
  4. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB), 2016. URL: https://www.SMT-LIB.org.
  5. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer, 21(1):1-29, 2019. URL: https://doi.org/10.1007/s10009-017-0469-y.
  6. Gjorgjina Cenikj, Ryan Dieter Lang, Andries Petrus Engelbrecht, Carola Doerr, Peter Korošec, and Tome Eftimov. Selector: selecting a representative benchmark suite for reproducible statistical comparison. Proceedings of the Genetic and Evolutionary Computation Conference, 2022. Google Scholar
  7. Katharina Eggensperger, Marius Lindauer, and Frank Hutter. Pitfalls and best practices in algorithm configuration. Journal of Artificial Intelligence Research JAIR, 64(1):861-893, 2019. URL: https://doi.org/10.1613/jair.1.11420.
  8. Chris Fawcett, Mauro Vallati, Holger H. Hoos, and Alfonso E. Gerevini. Competitions in ai - robustly ranking solvers using statistical resampling, 2023. URL: https://doi.org/10.48550/arXiv.2308.05062.
  9. Tobias Fuchs, Jakob Bach, and Ashlin Iser. Active learning for sat solver benchmarking. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 407-425, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30823-9_21.
  10. Ian P. Gent, Bilal Syed Hussain, Christopher Jefferson, Lars Kotthoff, Ian Miguel, Glenna F. Nightingale, and Peter Nightingale. Discriminating instance generation for automated constraint model selection. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, CP, volume 8656 of Lecture Notes in Computer Science, pages 356-365. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_27.
  11. Marijn J.H. Heule, Ashlin Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Report Series B. Department of Computer Science, University of Helsinki, Helsinki, 2024. Google Scholar
  12. Holger H. Hoos. Automated algorithm configuration and parameter tuning. In Autonomous Search, pages 37-71. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-21434-9_3.
  13. Ashlin Iser. Benchmark Compilation for SAT Competition 2023. In Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions, 2023. Google Scholar
  14. Ashlin Iser and Christoph Jabs. Global benchmark database. In International Conference on Theory and Applications of Satisfiability Testing, SAT, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.18.
  15. Erdem Kuş, Özgür Akgün, Nguyen Dang, and Ian Miguel. Frugal Algorithm Selection. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024), volume 307 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:16, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2024.38.
  16. Théo Matricon, Mathieu Acher, Helge Spieker, and Arnaud Gotlieb. Efficiently ranking software variants with minimal benchmarks. arXiv preprint arXiv:2509.06716, 2025. URL: https://doi.org/10.48550/arXiv.2509.06716.
  17. Théo Matricon, Mario Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H Hoos. Statistical comparison of algorithm performance through instance selection. In International Conference on Principles and Practice of Constraint Programming (CP 2021), 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.43.
  18. Olivier Roussel. Controlling a solver execution with the runsolver tool: System description. Journal on Satisfiability, Boolean Modelling and Computation, 7(4):139-144, 2011. URL: https://doi.org/10.3233/SAT190083.
  19. Ayal Taitler, Ron Alford, Joan Espasa, Gregor Behnke, Daniel Fišer, Michael Gimelfarb, Florian Pommerening, Scott Sanner, Enrico Scala, Dominik Schreiber, Javier Segovia-Aguas, and Jendrik Seipp. The 2023 International Planning Competition. AI Magazine, 45(2):280-296, 2024. URL: https://doi.org/10.1002/aaai.12169.
  20. Koen van der Blom, Holger H. Hoos, Chuan Luo, and Jeroen G. Rook. Sparkle: Towards accessible meta-algorithmics for improving the state of the art in solving challenging problems. IEEE Transactions on Evolutionary Computation, 26(6):1351-1364, 2022. URL: https://doi.org/10.1109/TEVC.2022.3215013.
  21. Allen Van Gelder. Careful ranking of multiple solvers with timeouts and ties. In Proceedings of Theory and Applications of Satisfiability Testing, SAT. Springer Berlin Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_25.
  22. Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. The SMT competition 2015-2018. J. Satisf. Boolean Model. Comput., 11(1):221-259, 2019. URL: https://doi.org/10.3233/SAT190123.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact