{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:54:25Z","timestamp":1766134465675,"version":"3.48.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100012957","name":"Friedrich-Schiller-Universit\u00e4t Jena","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012957","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Conflict-driven clause learning (CDCL) is the dominating algorithmic paradigm for SAT solving and hugely successful in practice. In its lifted version QCDCL, it is one of the main approaches for solving quantified Boolean formulas (QBF). In both SAT and QBF, proofs can be efficiently extracted from runs of (Q)CDCL solvers. While for CDCL, it is known that the proof size in the underlying proof system propositional resolution matches the CDCL runtime up to a polynomial factor, we show that in QBF there is an exponential gap between QCDCL runtime and the size of the extracted proofs in QBF resolution systems. We demonstrate that this is not just a gap between QCDCL runtime and the size of\n                    <jats:italic>any<\/jats:italic>\n                    QBF resolution proof, but even the\n                    <jats:italic>extracted<\/jats:italic>\n                    proofs are exponentially smaller for some instances. Hence searching for a small proof via QCDCL (even with non-deterministic decision policies) will provably incur an exponential overhead for some instances.\n                  <\/jats:p>","DOI":"10.1007\/s10817-025-09745-6","type":"journal-article","created":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T07:01:57Z","timestamp":1762930917000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs"],"prefix":"10.1007","volume":"69","author":[{"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"B\u00f6hm","sequence":"additional","affiliation":[]},{"given":"Meena","family":"Mahajan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"issue":"3","key":"9745_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/2578043","volume":"57","author":"MY Vardi","year":"2014","unstructured":"Vardi, M.Y.: Boolean satisfiability: theory and engineering. Commun. ACM 57(3), 5 (2014)","journal-title":"Commun. ACM"},{"key":"9745_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. IOS Press (2021)","DOI":"10.3233\/FAIA336"},{"key":"9745_CR3","doi-asserted-by":"crossref","unstructured":"Shukla, A., Biere, A., Pulina, L., Seidl, M.: A survey on applications of quantified Boolean formulas. In: Proc. IEEE International Conference on Tools with Artificial Intelligence (ICTAI), pp. 78\u201384 (2019)","DOI":"10.1109\/ICTAI.2019.00020"},{"key":"9745_CR4","unstructured":"Gelder, A.V.: Verifying RUP proofs of propositional unsatisfiability. In: International Symposium on Artificial Intelligence and Mathematics, ISAIM, Fort Lauderdale, Florida, USA (2008). http:\/\/isaim2008.unl.edu\/PAPERS\/TechnicalProgram\/ISAIM2008_0008_60a1f9b2fd607a61ec9e0feac3f438f8.pdf"},{"key":"9745_CR5","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr., W.A.H., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD, Portland, OR, USA, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"9745_CR6","doi-asserted-by":"crossref","unstructured":"Heule, M., Jr., W.A.H., Wetzler, N.: Verifying refutations with extended resolution. In: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, pp. 345\u2013359 (2013)","DOI":"10.1007\/978-3-642-38574-2_24"},{"key":"9745_CR7","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M.: (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Thessaloniki, Greece, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10806, pp. 75\u201392. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_5","DOI":"10.1007\/978-3-319-89963-3_5"},{"key":"9745_CR8","first-page":"71","volume-title":"DRAT proofs, propagation redundancy, and extended resolution","author":"S Buss","year":"2019","unstructured":"Buss, S., Thapen, N.: Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science. In: Janota, M., Lynce, I. (eds.) DRAT proofs, propagation redundancy, and extended resolution, vol. 11628, pp. 71\u201389. Springer (2019)"},{"issue":"3","key":"9745_CR9","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/S10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2020","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reason. 64(3), 533\u2013554 (2020). https:\/\/doi.org\/10.1007\/S10817-019-09516-0","journal-title":"J. Autom. Reason."},{"key":"9745_CR10","volume-title":"Conflict-driven clause learning SAT solvers","author":"JPM Silva","year":"2021","unstructured":"Silva, J.P.M., Lynce, I., Malik, S.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Conflict-driven clause learning SAT solvers. IOS Press (2021)"},{"key":"9745_CR11","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proc. IEEE\/ACM International Conference on Computer-aided Design (ICCAD), 442\u2013449 (2002)","DOI":"10.1145\/774572.774637"},{"key":"9745_CR12","first-page":"59","volume-title":"Resolve and expand","author":"A Biere","year":"2004","unstructured":"Biere, A.: Theory and Applications of Satisfiability Testing SAT. Lecture Notes in Computer Science. In: Hoos, H.H., Mitchell, D.G. (eds.) Resolve and expand, vol. 3542, pp. 59\u201370. Springer (2004)"},{"key":"9745_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/j.tcs.2015.01.048","volume":"577","author":"M Janota","year":"2015","unstructured":"Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25\u201342 (2015)","journal-title":"Theor. Comput. Sci."},{"key":"9745_CR14","doi-asserted-by":"crossref","unstructured":"Lonsing, F., Egly, U.: DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In: Proc. International Conference on Automated Deduction (CADE), pp. 371\u2013384 (2017)","DOI":"10.1007\/978-3-319-63046-5_23"},{"key":"9745_CR15","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1613\/jair.1.11529","volume":"65","author":"T Peitl","year":"2019","unstructured":"Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. J. Artif. Intell. Res. 65, 180\u2013208 (2019)","journal-title":"J. Artif. Intell. Res."},{"key":"9745_CR16","first-page":"233","volume-title":"Proof complexity and SAT solving","author":"S Buss","year":"2021","unstructured":"Buss, S., Nordstr\u00f6m, J.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Proof complexity and SAT solving, pp. 233\u2013350. IOS Press (2021)"},{"key":"9745_CR17","first-page":"1177","volume-title":"Quantified Boolean formulas","author":"O Beyersdorff","year":"2021","unstructured":"Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Quantified Boolean formulas, pp. 1177\u20131221. IOS Press (2021)"},{"key":"9745_CR18","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P Beame","year":"2004","unstructured":"Beame, P., Kautz, H.A., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR) 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"1","key":"9745_CR19","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.-H.R.: Unified QBF certification and its applications. Form. Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"9745_CR20","first-page":"353","volume-title":"Proof complexity of quantified Boolean logic \u2013 a survey","author":"O Beyersdorff","year":"2022","unstructured":"Beyersdorff, O.: Mathematics for Computation (M4C). In: Benini, M., Beyersdorff, O., Rathjen, M., Schuster, P. (eds.) Proof complexity of quantified Boolean logic \u2013 a survey, pp. 353\u2013391. World Scientific (2022)"},{"key":"9745_CR21","volume-title":"Proof Complexity. Encyclopedia of Mathematics and Its Applications","author":"J Kraj\u00ed\u010dek","year":"2019","unstructured":"Kraj\u00ed\u010dek, J.: Proof Complexity. Encyclopedia of Mathematics and Its Applications, vol. 170. Cambridge University Press (2019)"},{"key":"9745_CR22","first-page":"422","volume-title":"Drat-trim: Efficient checking and trimming using expressive clausal proofs","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Warren, A.H., Jr.: Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science. In: Sinz, C., Egly, U. (eds.) Drat-trim: Efficient checking and trimming using expressive clausal proofs, vol. 8561, pp. 422\u2013429. Springer (2014)"},{"issue":"1","key":"9745_CR23","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-016-9390-4","volume":"58","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97\u2013125 (2017)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9745_CR24","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2), 512\u2013525 (2011)","journal-title":"Artif. Intell."},{"key":"9745_CR25","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1613\/jair.3152","volume":"40","author":"A Atserias","year":"2011","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. 40, 353\u2013373 (2011)","journal-title":"J. Artif. Intell. Res."},{"key":"9745_CR26","doi-asserted-by":"crossref","unstructured":"Vinyals, M.: Hard examples for common variable decision heuristics. In: Proceedings of the AAAI Conference on Artificial Intelligence (2020)","DOI":"10.1609\/aaai.v34i02.5527"},{"key":"9745_CR27","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., B\u00f6hm, B.: Understanding the relative strength of QBF CDCL solvers and QBF resolution. Log. Methods Comput. Sci. 19(2) (2023)","DOI":"10.46298\/lmcs-19(2:2)2023"},{"key":"9745_CR28","doi-asserted-by":"crossref","unstructured":"Janota, M.: On Q-Resolution and CDCL QBF solving. In: Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 402\u2013418 (2016)","DOI":"10.1007\/978-3-319-40970-2_25"},{"key":"9745_CR29","first-page":"47","volume-title":"Theory and Applications of Satisfiability Testing (SAT)","author":"B B\u00f6hm","year":"2021","unstructured":"B\u00f6hm, B., Beyersdorff, O.: Lower bounds for QCDCL via formula gauge. In: Li, C.-M., Many\u00e0, F. (eds.) Theory and Applications of Satisfiability Testing (SAT), pp. 47\u201363. Springer, Cham (2021)"},{"issue":"1","key":"9745_CR30","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9745_CR31","doi-asserted-by":"crossref","unstructured":"Van\u00a0Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: Proc. Principles and Practice of Constraint Programming (CP), pp. 647\u2013663 (2012)","DOI":"10.1007\/978-3-642-33558-7_47"},{"key":"9745_CR32","unstructured":"Slivovsky, F.: Quantified CDCL with universal resolution. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT). LIPIcs, vol. 236, pp. 24\u201312416. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"9745_CR33","doi-asserted-by":"publisher","unstructured":"Beyersdorff, O., B\u00f6hm, B., Mahajan, M.: Runtime vs. extracted proof size: An exponential gap for CDCL on qbfs. In: Wooldridge, M.J., Dy, J.G., Natarajan, S.: (eds.) Thirty-Eighth AAAI Conference on Artificial Intelligence, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI, Vancouver, Canada, pp. 7943\u20137951. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I8.28631","DOI":"10.1609\/AAAI.V38I8.28631"},{"key":"9745_CR34","doi-asserted-by":"publisher","unstructured":"B\u00f6hm, B., Beyersdorff, O.: QCDCL vs QBF Resolution: Further Insights. In: Mahajan, M., Slivovsky, F.: (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol. 271, pp. 4\u20131417. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.4 . https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2023\/18466","DOI":"10.4230\/LIPIcs.SAT.2023.4"},{"key":"9745_CR35","volume-title":"Propositional Logic: Deduction and Algorithms. Cambridge Tracts in Theoretical Computer Science","author":"HK B\u00fcning","year":"1999","unstructured":"B\u00fcning, H.K., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge Tracts in Theoretical Computer Science, vol. 48. Cambridge University Press (1999)"},{"key":"9745_CR36","doi-asserted-by":"crossref","unstructured":"Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: A semantic technique for hard random QBFs. LMCS. 15(1) (2019)","DOI":"10.23638\/LMCS-15(1:13)2019"},{"key":"9745_CR37","doi-asserted-by":"crossref","unstructured":"Balabanov, V., Widl, M., Jiang, J.-H.R.: QBF resolution systems and their proof complexities. In: Proc. Theory and Applications of Satisfiability Testing (SAT), pp. 154\u2013169 (2014)","DOI":"10.1007\/978-3-319-09284-3_12"},{"key":"9745_CR38","doi-asserted-by":"crossref","unstructured":"B\u00f6hm, B., Peitl, T., Beyersdorff, O.: QCDCL with cube learning or pure literal elimination - what is best? In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI), pp. 1781\u20131787. ijcai.org (2022)","DOI":"10.24963\/ijcai.2022\/248"},{"key":"9745_CR39","unstructured":"B\u00f6hm, B., Peitl, T., Beyersdorff, O.: Should decisions in QCDCL follow prefix order? In: Meel, K.S., Strichman, O.: (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT). LIPIcs, 236, 11\u201311119. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"9745_CR40","doi-asserted-by":"publisher","DOI":"10.1016\/J.ARTINT.2024.104194","volume":"336","author":"B B\u00f6hm","year":"2024","unstructured":"B\u00f6hm, B., Peitl, T., Beyersdorff, O.: QCDCL with cube learning or pure literal elimination - what is best? Artif. Intell. 336, 104194 (2024). https:\/\/doi.org\/10.1016\/J.ARTINT.2024.104194","journal-title":"Artif. Intell."},{"key":"9745_CR41","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1613\/jair.1.15522","volume":"81","author":"B B\u00f6hm","year":"2024","unstructured":"B\u00f6hm, B., Beyersdorff, O.: Qcdcl vs qbf resolution: Further insights. J. Artif. Intell. Res. (JAIR) 81, 741\u2013769 (2024). https:\/\/doi.org\/10.1613\/jair.1.15522","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9745_CR42","unstructured":"Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, Boston, Massachusetts, USA, pp. 143\u2013150. AAAI Press (2006). http:\/\/www.aaai.org\/Library\/AAAI\/2006\/aaai06-023.php"},{"key":"9745_CR43","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-39071-5_8","volume-title":"Recovering and utilizing partial duality in QBF","author":"A Goultiaeva","year":"2013","unstructured":"Goultiaeva, A., Bacchus, F.: Theory and Applications of Satisfiability Testing - SAT - 16th International Conference, Helsinki, Finland. Proceedings. Lecture Notes in Computer Science. In: J\u00e4rvisalo, M., Gelder, A.V. (eds.) Recovering and utilizing partial duality in QBF, vol. 7962, pp. 83\u201399. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_8"},{"key":"9745_CR44","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-24318-4_25","volume-title":"QELL: QBF reasoning with extended clause learning and levelized SAT solving","author":"K Tu","year":"2015","unstructured":"Tu, K., Hsu, T., Jiang, J.R.: Theory and Applications of Satisfiability Testing - SAT - 18th International Conference, Austin, TX, USA, Proceedings. Lecture Notes in Computer Science. In: Heule, M., Weaver, S.A. (eds.) QELL: QBF reasoning with extended clause learning and levelized SAT solving, vol. 9340, pp. 343\u2013359. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_25"},{"key":"9745_CR45","doi-asserted-by":"publisher","unstructured":"Vinyals, M., Li, C., Fleming, N., Kolokolova, A., Ganesh, V.: Limits of CDCL Learning via Merge Resolution. In: Mahajan, M., Slivovsky, F.: (eds.) 26th International Conference on Theory and Applications of Satisfiability Testing (SAT). Leibniz International Proceedings in Informatics (LIPIcs), vol. 271, pp. 27\u201312719. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2023.27.","DOI":"10.4230\/LIPIcs.SAT.2023.27"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09745-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09745-6","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09745-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:32Z","timestamp":1766134232000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09745-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9745"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09745-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"6 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 November 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 declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"30"}}