{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T14:15:11Z","timestamp":1783606511189,"version":"3.55.0"},"reference-count":65,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/501100010877","name":"Science, Technology and Innovation Commission of Shenzhen Municipality","doi-asserted-by":"publisher","award":["KQTD20200820113105004"],"award-info":[{"award-number":["KQTD20200820113105004"]}],"id":[{"id":"10.13039\/501100010877","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Integration"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1016\/j.vlsi.2026.102747","type":"journal-article","created":{"date-parts":[[2026,5,19]],"date-time":"2026-05-19T06:48:19Z","timestamp":1779173299000},"page":"102747","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Accelerating hardware formal verification via AutoML-driven SMT runtime prediction and solver selection"],"prefix":"10.1016","volume":"110","author":[{"given":"Wenda","family":"Leng","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Meihua","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yufeng","family":"Jin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/j.vlsi.2026.102747_b1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3661308","article-title":"Survey of machine learning for software-assisted hardware design verification: Past, present, and prospect","volume":"29","author":"Wu","year":"2024","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"10.1016\/j.vlsi.2026.102747_b2","series-title":"Formal Verification: an Essential Toolkit for Modern VLSI Design","author":"Seligman","year":"2023"},{"key":"10.1016\/j.vlsi.2026.102747_b3","series-title":"Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings 17","first-page":"20","article-title":"SMT-COMP: Satisfiability modulo theories competition","author":"Barrett","year":"2005"},{"key":"10.1016\/j.vlsi.2026.102747_b4","unstructured":"L. Hadarean, A. Hyv\u00e4rinen, A. Niemetz, G. Reger, Smt-comp 2019, Tech. Rep., 2019, Int. Satisfiability Modulo Theories (SMT) Competition."},{"key":"10.1016\/j.vlsi.2026.102747_b5","series-title":"International Conference on Principles and Practice of Constraint Programming","first-page":"438","article-title":"Understanding random SAT: Beyond the clauses-to-variables ratio","author":"Nudelman","year":"2004"},{"key":"10.1016\/j.vlsi.2026.102747_b6","series-title":"Local search strategies for satisfiability testing","first-page":"521","author":"Selman","year":"1993"},{"key":"10.1016\/j.vlsi.2026.102747_b7","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"303","article-title":"MachSMT: A machine learning-based algorithm selector for SMT solvers","author":"Scott","year":"2021"},{"key":"10.1016\/j.vlsi.2026.102747_b8","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","article-title":"SATzilla: portfolio-based algorithm selection for SAT","volume":"32","author":"Xu","year":"2008","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/j.vlsi.2026.102747_b9","series-title":"International Conference on Theory and Applications of Satisfiability Testing","first-page":"228","article-title":"Evaluating component solver contributions to portfolio-based algorithm selectors","author":"Xu","year":"2012"},{"key":"10.1016\/j.vlsi.2026.102747_b10","doi-asserted-by":"crossref","unstructured":"Z. Zhang, D. Ch\u00e9telat, J. Cotnareanu, A. Ghose, W. Xiao, H.-L. Zhen, Y. Zhang, J. Hao, M. Coates, M. Yuan, Grass: Combining graph neural networks with expert knowledge for sat solver selection, in: Proceedings of the 30th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, 2024, pp. 6301\u20136311.","DOI":"10.1145\/3637528.3671627"},{"key":"10.1016\/j.vlsi.2026.102747_b11","first-page":"1","article-title":"Graph neural network based time estimator for SAT solver","author":"Liu","year":"2024","journal-title":"Int. J. Mach. Learn. Cybern."},{"key":"10.1016\/j.vlsi.2026.102747_b12","series-title":"Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18\u201320, 1997 Proceedings 17","first-page":"54","article-title":"Model checking","author":"Clarke","year":"1997"},{"issue":"7","key":"10.1016\/j.vlsi.2026.102747_b13","doi-asserted-by":"crossref","first-page":"814","DOI":"10.1109\/43.851997","article-title":"Sequential equivalence checking based on structural similarities","volume":"19","author":"Van Eijk","year":"2002","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"7","key":"10.1016\/j.vlsi.2026.102747_b14","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"issue":"8","key":"10.1016\/j.vlsi.2026.102747_b15","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1536616.1536637","article-title":"Boolean satisfiability from theoretical hardness to practical success","volume":"52","author":"Malik","year":"2009","journal-title":"Commun. ACM"},{"issue":"9","key":"10.1016\/j.vlsi.2026.102747_b16","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","article-title":"Satisfiability modulo theories: introduction and applications","volume":"54","author":"De Moura","year":"2011","journal-title":"Commun. ACM"},{"key":"10.1016\/j.vlsi.2026.102747_b17","series-title":"The satisfiability modulo theories library (SMT-lib). www","first-page":"68","author":"Barrett","year":"2016"},{"key":"10.1016\/j.vlsi.2026.102747_b18","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Y.-A. Chen, Verification of arithmetic circuits with binary moment diagrams, in: Proceedings of the 32nd Annual ACM\/IEEE Design Automation Conference, 1995, pp. 535\u2013541.","DOI":"10.1145\/217474.217583"},{"issue":"2","key":"10.1016\/j.vlsi.2026.102747_b19","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","article-title":"Formal verification in hardware design: a survey","volume":"4","author":"Kern","year":"1999","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"key":"10.1016\/j.vlsi.2026.102747_b20","series-title":"Learning a SAT solver from single-bit supervision","author":"Selsam","year":"2018"},{"key":"10.1016\/j.vlsi.2026.102747_b21","series-title":"Theory and Applications of Satisfiability Testing\u2013SAT 2019: 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9\u201312, 2019, Proceedings 22","first-page":"336","article-title":"Guiding high-performance SAT solvers with unsat-core predictions","author":"Selsam","year":"2019"},{"key":"10.1016\/j.vlsi.2026.102747_b22","first-page":"131","article-title":"Conflict-driven clause learning SAT solvers","author":"Marques-Silva","year":"2009","journal-title":"Handb. Satisf."},{"key":"10.1016\/j.vlsi.2026.102747_b23","doi-asserted-by":"crossref","unstructured":"H. Wu, Improving sat-solving with machine learning, in: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, 2017, pp. 787\u2013788.","DOI":"10.1145\/3017680.3022464"},{"key":"10.1016\/j.vlsi.2026.102747_b24","series-title":"2016 17th International Symposium on Quality Electronic Design","first-page":"129","article-title":"Equivalence checking between SLM and RTL using machine learning techniques","author":"Hu","year":"2016"},{"key":"10.1016\/j.vlsi.2026.102747_b25","series-title":"2021 8th International Conference on Signal Processing and Integrated Networks","first-page":"732","article-title":"Utilization of machine learning in RTL-GL signals correlation","author":"Alhaddad","year":"2021"},{"issue":"1","key":"10.1016\/j.vlsi.2026.102747_b26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3517154","article-title":"A novel gapg approach to automatic property generation for formal verification: The gan perspective","volume":"19","author":"Gao","year":"2023","journal-title":"ACM Trans. Multimed. Comput. Commun. Appl."},{"key":"10.1016\/j.vlsi.2026.102747_b27","doi-asserted-by":"crossref","first-page":"135703","DOI":"10.1109\/ACCESS.2019.2942762","article-title":"LTL model checking based on binary classification of machine learning","volume":"7","author":"Zhu","year":"2019","journal-title":"IEEE Access"},{"key":"10.1016\/j.vlsi.2026.102747_b28","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/j.artint.2013.10.003","article-title":"Algorithm runtime prediction: Methods & evaluation","volume":"206","author":"Hutter","year":"2014","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.vlsi.2026.102747_b29","doi-asserted-by":"crossref","unstructured":"Z. Wu, S. Pan, G. Long, J. Jiang, X. Chang, C. Zhang, Connecting the dots: Multivariate time series forecasting with graph neural networks, in: Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, 2020, pp. 753\u2013763.","DOI":"10.1145\/3394486.3403118"},{"key":"10.1016\/j.vlsi.2026.102747_b30","doi-asserted-by":"crossref","unstructured":"D. Zou, S. Wang, X. Li, H. Peng, Y. Wang, C. Liu, K. Sheng, B. Zhang, Multispans: a multi-range spatial-temporal transformer network for traffic forecast via structural entropy optimization, in: Proceedings of the 17th ACM International Conference on Web Search and Data Mining, 2024, pp. 1032\u20131041.","DOI":"10.1145\/3616855.3635820"},{"key":"10.1016\/j.vlsi.2026.102747_b31","article-title":"Predicting execution time of computer programs using sparse polynomial regression","volume":"23","author":"Huang","year":"2010","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.vlsi.2026.102747_b32","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/s10472-011-9230-5","article-title":"Discovering the suitability of optimisation algorithms by learning from evolved instances","volume":"61","author":"Smith-Miles","year":"2011","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/j.vlsi.2026.102747_b33","series-title":"International Conference on Principles and Practice of Constraint Programming","first-page":"213","article-title":"Performance prediction and automated tuning of randomized and parametric algorithms","author":"Hutter","year":"2006"},{"issue":"2","key":"10.1016\/j.vlsi.2026.102747_b34","doi-asserted-by":"crossref","first-page":"1145","DOI":"10.1007\/s13042-024-02327-9","article-title":"Graph neural network based time estimator for SAT solver","volume":"16","author":"Liu","year":"2025","journal-title":"Int. J. Mach. Learn. Cybern."},{"key":"10.1016\/j.vlsi.2026.102747_b35","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10472-011-9228-z","article-title":"Algorithm portfolio selection as a bandit problem with unbounded losses","volume":"61","author":"Gagliolo","year":"2011","journal-title":"Ann. Math. Artif. Intell."},{"key":"10.1016\/j.vlsi.2026.102747_b36","volume":"vol. 17","author":"Applegate","year":"2006"},{"key":"10.1016\/j.vlsi.2026.102747_b37","series-title":"Learning and Intelligent Optimization: 7th International Conference, LION 7, Catania, Italy, January 7-11, 2013, Revised Selected Papers 7","first-page":"153","article-title":"Boosting sequential solver portfolios: Knowledge sharing and accuracy prediction","author":"Malitsky","year":"2013"},{"issue":"4","key":"10.1016\/j.vlsi.2026.102747_b38","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/s10462-011-9290-2","article-title":"Simple algorithm portfolio for SAT","volume":"40","author":"Nikoli\u0107","year":"2013","journal-title":"Artif. Intell. Rev."},{"key":"10.1016\/j.vlsi.2026.102747_b39","article-title":"Deep learning for algorithm portfolios","volume":"vol. 30","author":"Loreggia","year":"2016"},{"key":"10.1016\/j.vlsi.2026.102747_b40","first-page":"2825","article-title":"Scikit-learn: Machine learning in Python","volume":"12","author":"Pedregosa","year":"2011","journal-title":"J. Mach. Learn. Res."},{"issue":"4","key":"10.1016\/j.vlsi.2026.102747_b41","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1002\/wics.101","article-title":"Principal component analysis","volume":"2","author":"Abdi","year":"2010","journal-title":"Wiley Interdiscip. Rev.: Comput. Stat."},{"key":"10.1016\/j.vlsi.2026.102747_b42","series-title":"SMT-COMP 2023: The 18th international satisfiability modulo theories competitio","author":"Jon\u00e1\u0161","year":"2023"},{"key":"10.1016\/j.vlsi.2026.102747_b43","series-title":"SMT-LIB release 2023 (incremental benchmarks)","author":"Preiner","year":"2024"},{"key":"10.1016\/j.vlsi.2026.102747_b44","series-title":"SMT-LIB release 2023 (non-incremental benchmarks)","author":"Preiner","year":"2024"},{"issue":"1","key":"10.1016\/j.vlsi.2026.102747_b45","first-page":"221","article-title":"The SMT competition 2015\u20132018","volume":"11","author":"Weber","year":"2019","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.1016\/j.vlsi.2026.102747_b46","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"De Moura","year":"2008"},{"key":"10.1016\/j.vlsi.2026.102747_b47","series-title":"Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23","first-page":"171","article-title":"cvc4","author":"Barrett","year":"2011"},{"issue":"3","key":"10.1016\/j.vlsi.2026.102747_b48","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s10817-012-9246-5","article-title":"6 years of SMT-COMP","volume":"50","author":"Barrett","year":"2013","journal-title":"J. Automat. Reason."},{"key":"10.1016\/j.vlsi.2026.102747_b49","first-page":"207","article-title":"The 2014 SMT competition","volume":"9","author":"Cok","year":"2014","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.1016\/j.vlsi.2026.102747_b50","series-title":"International Conference on Computer Aided Verification","first-page":"737","article-title":"Yices 2.2","author":"Dutertre","year":"2014"},{"key":"10.1016\/j.vlsi.2026.102747_b51","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"93","article-title":"The mathsat5 smt solver","author":"Cimatti","year":"2013"},{"issue":"1","key":"10.1016\/j.vlsi.2026.102747_b52","first-page":"53","article-title":"Boolector 2.0","volume":"9","author":"Niemetz","year":"2014","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10.1016\/j.vlsi.2026.102747_b53","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1010933404324","article-title":"Random forests","volume":"45","author":"Breiman","year":"2001","journal-title":"Mach. Learn."},{"key":"10.1016\/j.vlsi.2026.102747_b54","first-page":"1111","article-title":"Tuning search algorithms for real-world applications: A regression tree based approach","volume":"vol. 1","author":"Bartz-Beielstein","year":"2004"},{"issue":"1","key":"10.1016\/j.vlsi.2026.102747_b55","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1006\/jcss.1997.1504","article-title":"A decision-theoretic generalization of on-line learning and an application to boosting","volume":"55","author":"Freund","year":"1997","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/j.vlsi.2026.102747_b56","first-page":"1189","article-title":"Greedy function approximation: a gradient boosting machine","author":"Friedman","year":"2001","journal-title":"Ann. Stat."},{"key":"10.1016\/j.vlsi.2026.102747_b57","doi-asserted-by":"crossref","unstructured":"T. Chen, C. Guestrin, Xgboost: A scalable tree boosting system, in: Proceedings of the 22nd Acm Sigkdd International Conference on Knowledge Discovery and Data Mining, 2016, pp. 785\u2013794.","DOI":"10.1145\/2939672.2939785"},{"key":"10.1016\/j.vlsi.2026.102747_b58","doi-asserted-by":"crossref","unstructured":"T. Akiba, S. Sano, T. Yanase, T. Ohta, M. Koyama, Optuna: A next-generation hyperparameter optimization framework, in: Proceedings of the 25th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, 2019, pp. 2623\u20132631.","DOI":"10.1145\/3292500.3330701"},{"key":"10.1016\/j.vlsi.2026.102747_b59","series-title":"Tree-structured parzen estimator: Understanding its algorithm components and their roles for better empirical performance","author":"Watanabe","year":"2023"},{"issue":"1","key":"10.1016\/j.vlsi.2026.102747_b60","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1002\/wics.14","article-title":"Ridge regression","volume":"1","author":"McDonald","year":"2009","journal-title":"Wiley Interdiscip. Rev.: Comput. Stat."},{"issue":"10","key":"10.1016\/j.vlsi.2026.102747_b61","doi-asserted-by":"crossref","first-page":"1348","DOI":"10.1002\/bjs.10895","article-title":"LASSO regression","volume":"105","author":"Ranstam","year":"2018","journal-title":"J. Br. Surg."},{"issue":"6","key":"10.1016\/j.vlsi.2026.102747_b62","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1002\/wics.1278","article-title":"Decision trees","volume":"5","author":"De Ville","year":"2013","journal-title":"Wiley Interdiscip. Rev.: Comput. Stat."},{"key":"10.1016\/j.vlsi.2026.102747_b63","article-title":"CatBoost: unbiased boosting with categorical features","volume":"31","author":"Prokhorenkova","year":"2018","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.vlsi.2026.102747_b64","article-title":"Lightgbm: A highly efficient gradient boosting decision tree","volume":"30","author":"Ke","year":"2017","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"10.1016\/j.vlsi.2026.102747_b65","series-title":"Efficient Learning Machines: Theories, Concepts, and Applications for Engineers and System Designers","first-page":"67","article-title":"Support vector regression","author":"Awad","year":"2015"}],"container-title":["Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926026001021?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926026001021?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T13:23:55Z","timestamp":1783603435000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167926026001021"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9]]},"references-count":65,"alternative-id":["S0167926026001021"],"URL":"https:\/\/doi.org\/10.1016\/j.vlsi.2026.102747","relation":{},"ISSN":["0167-9260"],"issn-type":[{"value":"0167-9260","type":"print"}],"subject":[],"published":{"date-parts":[[2026,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Accelerating hardware formal verification via AutoML-driven SMT runtime prediction and solver selection","name":"articletitle","label":"Article Title"},{"value":"Integration","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.vlsi.2026.102747","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"102747"}}