{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T05:11:16Z","timestamp":1778735476191,"version":"3.51.4"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T00:00:00Z","timestamp":1750636800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T00:00:00Z","timestamp":1750636800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Karlsruher Institut f\u00fcr Technologie (KIT)"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Benchmarking is crucial for developing new algorithms. This also applies to solvers for the propositional satisfiability (SAT) problem. Benchmark selection is about choosing representative problem instances that reliably discriminate solvers based on their runtime. In this paper, we present a dynamic benchmark selection approach based on active learning. Our approach estimates the rank of a new solver among its competitors, striving to minimize benchmarking runtime but maximize ranking accuracy. Instead of using real-valued solver runtimes, our approach works with discretized runtime labels, which yielded better solver rank predictions. We evaluated this approach on the Anniversary Track dataset from the SAT Competition 2022. Our benchmark selection approach can predict the rank of a new solver after approximately 10\u00a0% of the time it would take to run the solver on all instances of this dataset, with a prediction accuracy of approximately 92\u00a0%. Additionally, we discuss the importance of instance families in the selection process. In conclusion, our tool offers a reliable method for solver engineers to assess a new solver\u2019s performance efficiently.<\/jats:p>","DOI":"10.1007\/s10817-025-09729-6","type":"journal-article","created":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T04:27:25Z","timestamp":1750652845000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Active Learning for SAT Solver Benchmarking"],"prefix":"10.1007","volume":"69","author":[{"given":"Tobias","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Bach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashlin","family":"Iser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,23]]},"reference":[{"key":"9729_CR1","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.artint.2015.01.002","volume":"223","author":"A Balint","year":"2015","unstructured":"Balint, A., Belov, A., J\u00e4rvisalo, M., et al.: Overview and analysis of the SAT Challenge 2012 solver competition. Artif. Intell. 223, 120\u2013155 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.01.002","journal-title":"Artif. Intell."},{"key":"9729_CR2","unstructured":"Balyo, T., Heule, M., Iser, M., et\u00a0al.: (eds) Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions, Department of Computer Science, University of Helsinki, (2022) http:\/\/hdl.handle.net\/10138\/347211"},{"issue":"1","key":"9729_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45(1), 5\u201332 (2001). https:\/\/doi.org\/10.1023\/A:1010933404324","journal-title":"Mach. Learn."},{"key":"9729_CR4","doi-asserted-by":"publisher","unstructured":"Breiman, L., Friedman, JH., Olshen, RA., et\u00a0al.: Classification and Regression Trees, 1st edn. Wadsworth, (1984) https:\/\/doi.org\/10.1201\/9781315139470","DOI":"10.1201\/9781315139470"},{"key":"9729_CR5","doi-asserted-by":"publisher","unstructured":"Collautti, M., Malitsky, Y., Mehta, D., et\u00a0al.: SNNAP: solver-based nearest neighbor for algorithm portfolios. In: European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases, pp 435\u2013450, (2013) https:\/\/doi.org\/10.1007\/978-3-642-40994-3_28","DOI":"10.1007\/978-3-642-40994-3_28"},{"key":"9729_CR6","doi-asserted-by":"publisher","unstructured":"Dang, N., Akg\u00fcn, \u00d6., Espasa, J., et\u00a0al.: A framework for generating informative benchmark instances. In: International Conference on Principles and Practice of Constraint Programming, pp 18:1\u201318:18, (2022)https:\/\/doi.org\/10.4230\/LIPIcs.CP.2022.18","DOI":"10.4230\/LIPIcs.CP.2022.18"},{"issue":"3","key":"9729_CR7","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1037\/met0000079","volume":"21","author":"JCF De Winter","year":"2016","unstructured":"De Winter, J.C.F., Gosling, S.D., Potter, J.: Comparing the pearson and spearman correlation coefficients across distributions and sample sizes: A tutorial using simulations and empirical data. Psychol. Methods 21(3), 273\u2013290 (2016). https:\/\/doi.org\/10.1037\/met0000079","journal-title":"Psychol. Methods"},{"key":"9729_CR8","doi-asserted-by":"publisher","unstructured":"Dehghani, M., Tay, Y., Gritsenko, AA., et\u00a0al.: The benchmark lottery. CoRR abs\/2107.07002. (2021) https:\/\/doi.org\/10.48550\/arXiv.2107.07002","DOI":"10.48550\/arXiv.2107.07002"},{"key":"9729_CR9","doi-asserted-by":"publisher","unstructured":"Froleyks, N., Heule, M., Iser, M., et al.: SAT Competition 2020. Artificial Intelligence 301,(2021). https:\/\/doi.org\/10.1016\/j.artint.2021.103572","DOI":"10.1016\/j.artint.2021.103572"},{"key":"9729_CR10","doi-asserted-by":"publisher","unstructured":"Fuchs, T., Bach, J., Iser, M.: Active learning for SAT solver benchmarking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp 407\u2013425, (2023) https:\/\/doi.org\/10.1007\/978-3-031-30823-9_21","DOI":"10.1007\/978-3-031-30823-9_21"},{"key":"9729_CR11","doi-asserted-by":"publisher","unstructured":"Garz\u00f3n, I., Mesejo, P., Gir\u00e1ldez-Cru, J.: On the performance of deep generative models of realistic SAT instances. In: International Conference on Theory and Applications of Satisfiability Testing, pp 3:1\u20133:19, (2022)https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.3","DOI":"10.4230\/LIPIcs.SAT.2022.3"},{"key":"9729_CR12","doi-asserted-by":"publisher","unstructured":"Gelder, AV.: Careful ranking of multiple solvers with timeouts and ties. In: International Conference on Theory and Applications of Satisfiability Testing, pp 317\u2013328, (2011) https:\/\/doi.org\/10.1007\/978-3-642-21581-0_25","DOI":"10.1007\/978-3-642-21581-0_25"},{"key":"9729_CR13","doi-asserted-by":"publisher","unstructured":"Golbandi, N., Koren, Y., Lempel, R.: Adaptive bootstrapping of recommender systems using decision trees. In: International Conference on Web Search and Data Mining, pp 595\u2013604, (2011)https:\/\/doi.org\/10.1145\/1935826.1935910","DOI":"10.1145\/1935826.1935910"},{"issue":"5\u20136","key":"9729_CR14","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.compbiolchem.2004.09.006","volume":"28","author":"J Gorodkin","year":"2004","unstructured":"Gorodkin, J.: Comparing two k-category assignments by a k-category correlation coefficient. Comput. Biol. Chem. 28(5\u20136), 367\u2013374 (2004). https:\/\/doi.org\/10.1016\/j.compbiolchem.2004.09.006","journal-title":"Comput. Biol. Chem."},{"key":"9729_CR15","doi-asserted-by":"publisher","unstructured":"Harpale, A., Yang, Y.: Personalized active learning for collaborative filtering. In: Conference on Research and Development in Information Retrieval, pp 91\u201398, (2008) https:\/\/doi.org\/10.1145\/1390334.1390352","DOI":"10.1145\/1390334.1390352"},{"key":"9729_CR16","doi-asserted-by":"publisher","unstructured":"Hoos, HH., Kaufmann, B., Schaub, T., et\u00a0al.: Robust benchmark set selection for boolean constraint solvers. In: Learning and Intelligent Optimization Conference, pp 138\u2013152, (2013) https:\/\/doi.org\/10.1007\/978-3-642-44973-4_16","DOI":"10.1007\/978-3-642-44973-4_16"},{"key":"9729_CR17","doi-asserted-by":"publisher","unstructured":"Hoos, HH., Hutter, F., Leyton-Brown, K.: Automated configuration and selection of SAT solvers. In: Handbook of Satisfiability, 2nd edn. IOS Press, chap\u00a012, p 481\u2013507, (2021)https:\/\/doi.org\/10.3233\/FAIA200995","DOI":"10.3233\/FAIA200995"},{"key":"9729_CR18","doi-asserted-by":"publisher","unstructured":"Hutter, F., Hoos, HH., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Learning and Intelligent Optimization Conference, pp 507\u2013523, (2011) https:\/\/doi.org\/10.1007\/978-3-642-25566-3_40","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"9729_CR19","doi-asserted-by":"publisher","unstructured":"Iser, M., Jabs, C.: Global benchmark database. In: International Conference on Theory and Applications of Satisfiability Testing, pp 18:1\u201318:10, (2024)https:\/\/doi.org\/10.4230\/LIPICS.SAT.2024.18","DOI":"10.4230\/LIPICS.SAT.2024.18"},{"key":"9729_CR20","doi-asserted-by":"publisher","unstructured":"Iser, M., Heule, M., J\u00e4rvisalo, M., et\u00a0al.: Benchmarks of SAT Competition 2022: Anniversary track. (2024) https:\/\/doi.org\/10.5281\/zenodo.11175170","DOI":"10.5281\/zenodo.11175170"},{"key":"9729_CR21","unstructured":"Kodinariya, T.M., Makwana, P.R.: Review on determining number of cluster in k-means clustering. International Journal of Advance Research in Computer Science and Management Studies 1(6), 90\u201395 (2013) http:\/\/www.ijarcsms.com\/docs\/paper\/volume1\/issue6\/V1I6-0015.pdf"},{"issue":"8","key":"9729_CR22","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1109\/MC.2009.263","volume":"42","author":"Y Koren","year":"2009","unstructured":"Koren, Y., Bell, R.M., Volinsky, C.: Matrix factorization techniques for recommender systems. Computer 42(8), 30\u201337 (2009). https:\/\/doi.org\/10.1109\/MC.2009.263","journal-title":"Computer"},{"key":"9729_CR23","unstructured":"Manthey, N., M\u00f6hle, S.: Better evaluations by analyzing benchmark structure. In: Pragmatics of SAT, (2016) http:\/\/www.pragmaticsofsat.org\/2016\/reg\/POS-16_paper_4.pdf"},{"key":"9729_CR24","doi-asserted-by":"publisher","unstructured":"Matricon, T., Anastacio, M., Fijalkow, N., et\u00a0al.: Statistical comparison of algorithm performance through instance selection. In: International Conference on Principles and Practice of Constraint Programming, pp 43:1\u201343:21, (2021) https:\/\/doi.org\/10.4230\/LIPIcs.CP.2021.43","DOI":"10.4230\/LIPIcs.CP.2021.43"},{"issue":"2","key":"9729_CR25","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1016\/0005-2795(75)90109-9","volume":"405","author":"BW Matthews","year":"1975","unstructured":"Matthews, B.W.: Comparison of the predicted and observed secondary structure of T4 phage lysozyme. Biochem. Biophys. Acta. 405(2), 442\u2013451 (1975). https:\/\/doi.org\/10.1016\/0005-2795(75)90109-9","journal-title":"Biochem. Biophys. Acta."},{"key":"9729_CR26","doi-asserted-by":"publisher","unstructured":"M\u0131s\u0131r, M.: Data sampling through collaborative filtering for algorithm selection. In: IEEE Congress on Evolutionary Computation, pp 2494\u20132501, (2017) https:\/\/doi.org\/10.1109\/CEC.2017.7969608","DOI":"10.1109\/CEC.2017.7969608"},{"key":"9729_CR27","doi-asserted-by":"publisher","unstructured":"M\u0131s\u0131r, M.: Benchmark set reduction for cheap empirical algorithmic studies. In: IEEE Congress on Evolutionary Computation, pp 871\u2013877, (2021) https:\/\/doi.org\/10.1109\/CEC45853.2021.9505012","DOI":"10.1109\/CEC45853.2021.9505012"},{"key":"9729_CR28","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.artint.2016.12.001","volume":"244","author":"M M\u0131s\u0131r","year":"2017","unstructured":"M\u0131s\u0131r, M., Sebag, M.: ALORS: An algorithm recommender system. Artif. Intell. 244, 291\u2013314 (2017). https:\/\/doi.org\/10.1016\/j.artint.2016.12.001","journal-title":"Artif. Intell."},{"issue":"2","key":"9729_CR29","doi-asserted-by":"publisher","first-page":"261","DOI":"10.2478\/amcs-2019-0019","volume":"29","author":"Y Ngoko","year":"2019","unstructured":"Ngoko, Y., C\u00e9rin, C., Trystram, D.: Solving SAT in a distributed cloud: A portfolio approach. International Journal of Applied and Computational Mathematics 29(2), 261\u2013274 (2019). https:\/\/doi.org\/10.2478\/amcs-2019-0019","journal-title":"International Journal of Applied and Computational Mathematics"},{"key":"9729_CR30","doi-asserted-by":"publisher","unstructured":"Nie\u00dfl, C., Herrmann, M., Wiedemann, C., et\u00a0al.: Over-optimism in benchmark studies and the multiplicity of design and analysis options when interpreting their results. WIREs Data Mining and Knowledge Discovery 12(2). (2022) https:\/\/doi.org\/10.1002\/widm.1441","DOI":"10.1002\/widm.1441"},{"key":"9729_CR31","unstructured":"Pedregosa, F., Varoquaux, G., Gramfort, A., et\u00a0al.: Scikit-learn: Machine learning in Python. Journal of Machine Learning Research 12(85), 2825\u20132830 (2011) http:\/\/jmlr.org\/papers\/v12\/pedregosa11a.html"},{"key":"9729_CR32","doi-asserted-by":"publisher","unstructured":"Rubens, N., Elahi, M., Sugiyama, M., et\u00a0al.: Active learning in recommender systems. In: Recommender Systems Handbook, 2nd edn. Springer, chap\u00a024, p 809\u2013846, (2015) https:\/\/doi.org\/10.1007\/978-1-4899-7637-6_24","DOI":"10.1007\/978-1-4899-7637-6_24"},{"key":"9729_CR33","unstructured":"Settles, B.: Active learning literature survey. Tech. rep., University of Wisconsin-Madison, Department of Computer Sciences, (2009) http:\/\/digital.library.wisc.edu\/1793\/60660"},{"key":"9729_CR34","doi-asserted-by":"publisher","unstructured":"Sinha, S., Ebrahimi, S., Darrell, T.: Variational adversarial active learning. In: International Conference on Computer Vision, pp 5971\u20135980, (2019)https:\/\/doi.org\/10.1109\/ICCV.2019.00607","DOI":"10.1109\/ICCV.2019.00607"},{"key":"9729_CR35","doi-asserted-by":"publisher","unstructured":"St\u00fctzle, T., L\u00f3pez-Ib\u00e1\u00f1ez, M., P\u00e9rez-C\u00e1ceres, L.: Automated algorithm configuration and design. In: Genetic and Evolutionary Computation Conference, pp 997\u20131019, (2022) https:\/\/doi.org\/10.1145\/3520304.3533663","DOI":"10.1145\/3520304.3533663"},{"key":"9729_CR36","doi-asserted-by":"publisher","unstructured":"Tharwat, A.: Linear vs. quadratic discriminant analysis classifier: A tutorial. International Journal of Applied Pattern Recognition 3(2), 145\u2013180 (2016). https:\/\/doi.org\/10.1504\/IJAPR.2016.079050","DOI":"10.1504\/IJAPR.2016.079050"},{"key":"9729_CR37","unstructured":"Tran, T., Do, T., Reid, ID., et\u00a0al.: Bayesian generative active deep learning. In: International Conference on Machine Learning, pp 6295\u20136304, (2019) http:\/\/proceedings.mlr.press\/v97\/tran19a.html"},{"key":"9729_CR38","doi-asserted-by":"publisher","unstructured":"Volpato, R., Song, G.: Active learning to optimise time-expensive algorithm selection. CoRR abs\/1909.03261. (2019) https:\/\/doi.org\/10.48550\/arXiv.1909.03261","DOI":"10.48550\/arXiv.1909.03261"},{"issue":"2","key":"9729_CR39","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0893-6080(05)80023-1","volume":"5","author":"DH Wolpert","year":"1992","unstructured":"Wolpert, D.H.: Stacked generalization. Neural Netw. 5(2), 241\u2013259 (1992). https:\/\/doi.org\/10.1016\/S0893-6080(05)80023-1","journal-title":"Neural Netw."},{"key":"9729_CR40","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu, L., Hutter, F., Hoos, H.H., et al.: SATzilla: Portfolio-based algorithm selection for SAT. Journal Of Artificial Intelligence Research 32, 565\u2013606 (2008). https:\/\/doi.org\/10.1613\/jair.2490","journal-title":"Journal Of Artificial Intelligence Research"},{"key":"9729_CR41","unstructured":"Xu, L., Hutter, F., Hoos, HH., et\u00a0al.: Features for SAT. Tech. rep., University of British Columbia, (2012) https:\/\/www.cs.ubc.ca\/labs\/beta\/Projects\/SATzilla\/Report_SAT_features.pdf"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09729-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09729-6","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09729-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T04:45:57Z","timestamp":1778733957000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09729-6"}},"subtitle":["Extended and Revised Version"],"short-title":[],"issued":{"date-parts":[[2025,6,23]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9729"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09729-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,23]]},"assertion":[{"value":"28 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"16"}}