{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:51:15Z","timestamp":1775868675267,"version":"3.50.1"},"reference-count":81,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T00:00:00Z","timestamp":1732147200000},"content-version":"unspecified","delay-in-days":20,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2024,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including computer algebra systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine learning (sparse-linear and symbolic) regression techniques to <jats:italic>guess<\/jats:italic> a candidate closed-form function, and a combination of an SMT-solver and a CAS to <jats:italic>check<\/jats:italic> whether such function is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmark set, our approach outperforms state-of-the-art cost analyzers and recurrence solvers and can find closed-form solutions, in a reasonable time, for recurrences that cannot be solved by them.<\/jats:p>","DOI":"10.1017\/s1471068424000413","type":"journal-article","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T12:57:03Z","timestamp":1732193823000},"page":"1163-1207","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":4,"title":["A Machine Learning-Based Approach for Solving Recurrence Relations and Its use in Cost Analysis of Logic Programs"],"prefix":"10.1017","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1599-2431","authenticated-orcid":false,"given":"LOUIS","family":"RUSTENHOLZ","sequence":"first","affiliation":[]},{"given":"MAXIMILIANO","family":"KLEMEN","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-9375","authenticated-orcid":false,"given":"MIGUEL \u00c1.","family":"CARREIRA-PERPI\u00d1\u00c1N","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1092-2071","authenticated-orcid":false,"given":"PEDRO","family":"LOPEZ-GARCIA","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,11,21]]},"reference":[{"key":"S1471068424000413_ref77","doi-asserted-by":"publisher","DOI":"10.1145\/3586028"},{"key":"S1471068424000413_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302467"},{"key":"S1471068424000413_ref28","volume-title":"Finite Calculus: A Tutorial for Solving Nasty Sums","author":"Gleich","year":"2005"},{"key":"S1471068424000413_ref22","unstructured":"Flores-Montoya, A. 2017. Cost analysis of programs based on the refinement of cost relations. PhD thesis. Technische Universit\u00e4t Darmstadt, Advisor: Reiner H\u00e4hnle."},{"key":"S1471068424000413_ref12","unstructured":"Cranmer, M. 2023. Interpretable Machine Learning for Science with PySR and SymbolicRegression.jl, arXiv, 2305.01582."},{"key":"S1471068424000413_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-84858-7"},{"key":"S1471068424000413_ref30","doi-asserted-by":"publisher","DOI":"10.1201\/b18401"},{"key":"S1471068424000413_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_3"},{"key":"S1471068424000413_ref66","doi-asserted-by":"crossref","unstructured":"Rajkhowa, P. and Lin, F. 2017. VIAP - Automated system for verifying integer assignment programs with loops. In 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC, IEEE Computer Society, 137\u2013144.","DOI":"10.1109\/SYNASC.2017.00032"},{"key":"S1471068424000413_ref80","unstructured":"Z3Py 2023. Z3 API in Python. URL: https:\/\/ericpony.github.io\/z3py-tutorial. [Accessed on May 25, 2023]."},{"key":"S1471068424000413_ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43369-6_1"},{"key":"S1471068424000413_ref79","unstructured":"Wilf, H. S. 1994. generatingfunctionology, 2nd ed. Academic Press. URL: https:\/\/www2.math.upenn.edu\/~wilf\/gfology2.pdf. [Accessed on May 25, 2023]."},{"key":"S1471068424000413_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3290368"},{"key":"S1471068424000413_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3571237"},{"key":"S1471068424000413_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"S1471068424000413_ref25","doi-asserted-by":"crossref","unstructured":"Frohn, F. , Hark, M. and Giesl, J. 2020. Termination of polynomial loops. In Static Analysis - 27th International Symposium, SAS, vol. 12389. Lecture Notes in Computer Science. Springer, 89\u2013112.","DOI":"10.1007\/978-3-030-65474-0_5"},{"key":"S1471068424000413_ref36","doi-asserted-by":"crossref","unstructured":"Humenberger, A. , Jaroschek, M. and Kovacs, L. 2018. Invariant generation for multi-path loops with polynomial assignments. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI, vol. 10747. Lecture Notes in Computer Science. Springer, 226\u2013246.","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"S1471068424000413_ref62","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90038-6"},{"key":"S1471068424000413_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062373"},{"key":"S1471068424000413_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"S1471068424000413_ref23","first-page":"249","volume-title":"LPAR-21 2017","volume":"46","author":"Frohn","year":"2017"},{"key":"S1471068424000413_ref51","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000042"},{"key":"S1471068424000413_ref56","doi-asserted-by":"crossref","unstructured":"Navas, J. , Mera, E. , Lopez-Garcia, P. and Hermenegildo, M. 2007. User-definable resource bounds analysis for logic programs. In Proc. of ICLP\u201907, vol. 4670. LNCS. Springer, 348\u2013363.","DOI":"10.1007\/978-3-540-74610-2_24"},{"key":"S1471068424000413_ref63","unstructured":"Petkovsek, M. , Wilf, H. S. and Zeilberger, D. 1997, A K Peters, Ltd. URL: https:\/\/www2.math.upenn.edu\/~wilf\/AeqB.html."},{"key":"S1471068424000413_ref75","unstructured":"Vasconcelos, P. B. 2008. Space cost analysis using sized types. PhD thesis. University of St Andrews, Advisor: Kevin Hammond."},{"key":"S1471068424000413_ref20","first-page":"57","volume-title":"Formal Methods in Computer-Aided Design, FMCAD","author":"Farzan","year":"2015"},{"key":"S1471068424000413_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655"},{"key":"S1471068424000413_ref46","unstructured":"Kovacs, L. 2007. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis. RISC, Johannes Kepler University Linz, Advisors: Tudor Jebelean and Andrei Voronkov."},{"key":"S1471068424000413_ref72","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"S1471068424000413_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"S1471068424000413_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"S1471068424000413_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/161468.161472"},{"key":"S1471068424000413_ref45","doi-asserted-by":"crossref","unstructured":"Klemen, M. , Carreira-Perpi\u00f1\u00e1n, M. and Lopez-Garcia, P. 2023. Solving recurrence relations using machine learning, with application to cost analysis. In Pontelli, E. , Costantini, S. , Dodaro, C. , Gaggl, S. , Calegari, R. , Garcez, A. D. , Fabiano, F. , Mileo, A. , Russo, A. and Toni, F. , Eds.Technical Communications of the 39th International Conference on Logic Programming (ICLP 2023), vol. 385. Electronic Proceedings in Theoretical Computer Science (EPTCS). Open Publishing Association (OPA), 155\u2013168.","DOI":"10.4204\/EPTCS.385.0"},{"key":"S1471068424000413_ref10","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2000.0368"},{"key":"S1471068424000413_ref53","unstructured":"Manna, Z. and Mccarthy, J. 1969. Properties of programs and partial function logic. In Machine Intelligence 5, Proceedings of the Fifth Annual Machine Intelligence Workshop 1970. Edinburgh University Press, 27\u201338."},{"key":"S1471068424000413_ref54","unstructured":"Mathematica 2023. Wolfram Mathematica (v13.2): The World\u2019s Definitive System for Modern Technical Computing. URL: https:\/\/www.wolfram.com\/mathematica. [Accessed on May 25, 2023]."},{"key":"S1471068424000413_ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"S1471068424000413_ref13","first-page":"337","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS","author":"De Moura","year":"2008"},{"key":"S1471068424000413_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322255"},{"key":"S1471068424000413_ref59","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3106964"},{"key":"S1471068424000413_ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-1616-6_11"},{"key":"S1471068424000413_ref15","doi-asserted-by":"crossref","unstructured":"Debray, S. K. , Lin, N.-W. and Hermenegildo, M. V. 1990. Task Granularity Analysis in Logic Programs. In Proc. PLDI\u201990, ACM, 174\u2013188.","DOI":"10.1145\/93542.93564"},{"key":"S1471068424000413_ref65","first-page":"239","volume-title":"VMCAI\u201904-2937","volume":"2937","author":"Podelski","year":"2004"},{"key":"S1471068424000413_ref57","first-page":"683","volume-title":"34th International Conference on Software Engineering (ICSE)","author":"Nguyen","year":"2012"},{"key":"S1471068424000413_ref69","first-page":"266","volume-title":"ISSAC 2004","author":"Rodriguez-Carbonell","year":"2004"},{"key":"S1471068424000413_ref76","first-page":"86","volume-title":"IFL 2003","author":"Vasconcelos","year":"2003"},{"key":"S1471068424000413_ref8","volume-title":"Introduction to the Operational Calculus","author":"Berg","year":"1967"},{"key":"S1471068424000413_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"S1471068424000413_ref9","first-page":"688","volume-title":"PLDI","author":"Breck","year":"2020"},{"key":"S1471068424000413_ref34","volume-title":"Fakult\u00e4t f\u00fcr Mathematik, Informatik und Statistik der Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen","author":"Hoffmann","year":"2011"},{"key":"S1471068424000413_ref55","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103"},{"key":"S1471068424000413_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"S1471068424000413_ref58","first-page":"608","volume-title":"36th International Conference on Software Engineering (ICSE)","author":"Nguyen","year":"2014"},{"key":"S1471068424000413_ref70","doi-asserted-by":"crossref","unstructured":"Rosendahl, M. 1989. Automatic complexity analysis. In 4th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA\u201989), ACM Press, 144\u2013156.","DOI":"10.1145\/99370.99381"},{"key":"S1471068424000413_ref6","doi-asserted-by":"crossref","unstructured":"Amrollahi, D. , Bartocci, E. , Kenison, G. , Kovacs, L. , Moosbrugger, M. and Stankovic, M. 2023. (Un)Solvable Loop Analysis, arXiv, 2306.01597.","DOI":"10.1007\/s10703-024-00455-0"},{"key":"S1471068424000413_ref49","volume-title":"Algebra and Applications","author":"Levin","year":"2008"},{"key":"S1471068424000413_ref40","volume-title":"The Concrete Tetrahedron: Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates","author":"Kauers","year":"2010"},{"key":"S1471068424000413_ref74","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"S1471068424000413_ref73","volume-title":"Talk given at Canadian Discrete and Algorithmic Mathematics (CanaDAM) 2013","author":"Tanny","year":"2013"},{"key":"S1471068424000413_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0041-5553(89)80002-3"},{"key":"S1471068424000413_ref17","first-page":"392","volume-title":"History of the Theory of Numbers, volume I: Divisibility and Primality, chapter XVII, recurring series: Lucas\u2019 un, vn","author":"Dickson","year":"1919"},{"key":"S1471068424000413_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08166-8_10"},{"key":"S1471068424000413_ref71","first-page":"4","article-title":"Resource usage analysis of logic programs via abstract interpretation using sized types","volume":"14","author":"Serrano","year":"2014","journal-title":"TPLP, ICLP\u201914 Special Issue"},{"key":"S1471068424000413_ref33","unstructured":"Higham, D. J. and Higham, N. J. 2016. MATLAB Guide. SIAM."},{"key":"S1471068424000413_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0519-4"},{"key":"S1471068424000413_ref47","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L. 2008. Reasoning Algebraically About P-Solvable Loops. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS, vol. 4963. Lecture Notes in Computer Science. Springer, 249\u2013264.","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"S1471068424000413_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42347"},{"key":"S1471068424000413_ref68","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"S1471068424000413_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2021.01.002"},{"key":"S1471068424000413_ref61","first-page":"2825","article-title":"Scikit-learn: Machine learning in Python","volume":"12","author":"Pedregosa","year":"2011","journal-title":"Journal of Machine Learning Research"},{"key":"S1471068424000413_ref78","doi-asserted-by":"publisher","DOI":"10.1145\/361002.361016"},{"key":"S1471068424000413_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3485515"},{"key":"S1471068424000413_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"S1471068424000413_ref16","first-page":"291","volume-title":"ILPS\u201997","author":"Debray","year":"1997"},{"key":"S1471068424000413_ref11","doi-asserted-by":"crossref","unstructured":"Celaya, M. and Ruskey, F. 2012. An undecidable nested recurrence relation. arXiv, 1203.0586.","DOI":"10.1007\/978-3-642-30870-3_12"},{"key":"S1471068424000413_ref52","first-page":"849","article-title":"A general framework for static profiling of parametric resource Usage","volume":"16","author":"Lopez-Garcia","year":"2016","journal-title":"TPLP (ICLP\u201916 Special Issue)"},{"key":"S1471068424000413_ref67","unstructured":"Rajkhowa, P. and Lin, F. 2019. A recurrence solver and its uses in program verification. Unpublished. URL: https:\/\/github.com\/VerifierIntegerAssignment\/rec_paper\/blob\/master\/Detail_proof\/full_version_with_proof.pdf. [Accessed on September 27, 2023]."},{"key":"S1471068424000413_ref38","first-page":"359","volume-title":"FOSSACS","author":"Kahn","year":"2020"},{"key":"S1471068424000413_ref7","unstructured":"Bagnara, R. , Pescetti, A. , Zaccagnini, A. and Zaffanella, E. 2005. PURRS: Towards computer algebra support for fully automatic worst-case complexity analysis. Technical report. arXiv:cs\/0512056."},{"key":"S1471068424000413_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2499937.2499943"},{"key":"S1471068424000413_ref81","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068424000413","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T02:02:54Z","timestamp":1736992974000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068424000413\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11]]},"references-count":81,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,11]]}},"alternative-id":["S1471068424000413"],"URL":"https:\/\/doi.org\/10.1017\/s1471068424000413","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}