{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:18:08Z","timestamp":1758053888088,"version":"3.44.0"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Nielsen transformation is a standard approach for solving word equations: by repeatedly splitting equations and applying simplification steps, equations are rewritten until a solution is reached. When solving a conjunction of word equations in this way, the performance of the solver will depend considerably on the order in which equations are processed. In this work, the use of Graph Neural Networks (GNNs) for ranking word equations before and during the solving process is explored. For this, a novel graph-based representation for word equations is presented, preserving global information across conjuncts, enabling the GNN to have a holistic view during ranking. To handle the variable number of conjuncts, three approaches to adapt a multi-classification task to the problem of ranking equations are proposed. The training of the GNN is done with the help of minimum unsatisfiable subsets (MUSes) of word equations. The experimental results show that, compared to state-of-the-art string solvers, the new framework solves more problems in benchmarks where each variable appears at most once in each equation.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_18","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:18Z","timestamp":1757887458000},"page":"327-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["When GNNs Met a\u00a0Word Equations Solver: Learning to\u00a0Rank Equations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6665-8089","authenticated-orcid":false,"given":"Julie","family":"Cailler","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4926-8089","authenticated-orcid":false,"given":"Chencheng","family":"Liang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2733-7098","authenticated-orcid":false,"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"18_CR1","unstructured":"DragonLi solver experimental report for benchmark a and task 2. https:\/\/github.com\/ChenchengLiang\/DragonLi\/tree\/rank\/experimental_results_tables\/eval_data_GNN\/A1\/task_2\/model. Accessed 16 May 2025"},{"key":"18_CR2","unstructured":"Github repository for the ablastion study. https:\/\/github.com\/ChenchengLiang\/DragonLi\/blob\/rank\/Appendix\/Ablation-study.md. Accessed 30 June 2025"},{"key":"18_CR3","unstructured":"Github repository for the statistics of evaluation data. https:\/\/github.com\/ChenchengLiang\/DragonLi\/blob\/rank\/Appendix\/Statistics-of-evaluation-data.md. Accessed 30 June 2025"},{"key":"18_CR4","unstructured":"Github repository for the statistics of muse. https:\/\/github.com\/ChenchengLiang\/DragonLi\/blob\/rank\/Appendix\/Statistics-of-MUSes.md. Accessed 30 June 2025"},{"key":"18_CR5","unstructured":"Github repository for the workflow. https:\/\/github.com\/ChenchengLiang\/DragonLi\/blob\/rank\/Appendix\/Workflow.md. Accessed 30 June 2025"},{"key":"18_CR6","unstructured":"The satisfiability modulo theories library (SMT-LIB). https:\/\/smtlib.cs.uiowa.edu\/benchmarks.shtml. Accessed 16 May 2025"},{"key":"18_CR7","unstructured":"Zaligvinder: A string solving benchmark framework. https:\/\/zaligvinder.github.io. Accessed 16 May 2025"},{"key":"18_CR8","unstructured":"DragonLi github repository branch:rank (2025). https:\/\/github.com\/ChenchengLiang\/boosting-string-equation-solving-by-GNNs\/tree\/rank. Accessed 16 May 2025"},{"key":"18_CR9","unstructured":"wordeq_solver (2025). https:\/\/github.com\/tage64\/wordeq _solver. Accessed 16 May 2025"},{"key":"18_CR10","unstructured":"Abdelaziz, I., et al.: Learning to guide a saturation-based theorem prover (2021). https:\/\/arxiv.org\/abs\/2106.03906"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-031-78709-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2025","unstructured":"Abdulla, P.A., Atig, M.F., Cailler, J., Liang, C., R\u00fcmmer, P.: Guiding word equation solving using graph neural networks. In: Akshay, S., Niemetz, A., Sankaranarayanan, S. (eds.) Automated Technology for Verification and Analysis, pp. 279\u2013301. Springer, Cham (2025)"},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-031-50524-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2024","unstructured":"Abdulla, P.A., Liang, C., R\u00fcmmer, P.: Boosting constrained Horn solving by unsat core learning. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 280\u2013302. Springer, Cham (2024)"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Agarap, A.F.: Deep Learning using Rectified Linear Units (ReLU) arXiv:1803.08375 (2018). https:\/\/doi.org\/10.48550\/arXiv.1803.08375","DOI":"10.48550\/arXiv.1803.08375"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 415\u2013442. Springer, Cham (2022)"},{"key":"18_CR15","unstructured":"Battaglia, P.W., et al.: Relational inductive biases, deep learning, and graph networks. CoRR abs\/1806.01261 (2018). http:\/\/arxiv.org\/abs\/1806.01261"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-030-79876-5_30","volume-title":"Automated Deduction \u2013 CADE 28","author":"F B\u00e1rtek","year":"2021","unstructured":"B\u00e1rtek, F., Suda, M.: Neural precedence recommender. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 525\u2013542. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_30"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek, F., Suda, M.: How much should this symbol weigh? A GNN-advised clause selection. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a094, pp. 96\u2013111. EasyChair (2023). https:\/\/doi.org\/10.29007\/5f4r, \/publications\/paper\/2BSs","DOI":"10.29007\/5f4r"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Chen, T., Hague, M., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL), 49:1\u201349:30 (2019). https:\/\/doi.org\/10.1145\/3290362","DOI":"10.1145\/3290362"},{"key":"18_CR19","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-031-57246-3_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YF Chen","year":"2024","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-noodler: an automata-based string solver. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 24\u201333. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_2"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-030-30806-3_8","volume-title":"Reachability Problems","author":"JD Day","year":"2019","unstructured":"Day, J.D., Ehlers, T., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: On solving word equations using SAT. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 93\u2013106. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_8"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Day, J.D., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: Rule-based word equation solving. In: Proceedings of the 8th International Conference on Formal Methods in Software Engineering, FormaliSE 2020, pp. 87\u201397. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372020.3391556","DOI":"10.1145\/3372020.3391556"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-540-24597-1_14","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"V Diekert","year":"2003","unstructured":"Diekert, V., Lohrey, M.: Word equations over graph products. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 156\u2013167. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-24597-1_14"},{"key":"18_CR23","unstructured":"Gilmer, J., Schoenholz, S.S., Riley, P.F., Vinyals, O., Dahl, G.E.: Neural message passing for quantum chemistry. CoRR abs\/1704.01212 (2017). http:\/\/arxiv.org\/abs\/1704.01212"},{"key":"18_CR24","unstructured":"Goodfellow, I.J., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016). http:\/\/www.deeplearningbook.org"},{"issue":"1","key":"18_CR25","doi-asserted-by":"publisher","first-page":"14","DOI":"10.2307\/2268661","volume":"16","author":"A Horn","year":"1951","unstructured":"Horn, A.: On sentences which are true of direct unions of algebras. J. Symb. Log. 16(1), 14\u201321 (1951). https:\/\/doi.org\/10.2307\/2268661","journal-title":"J. Symb. Log."},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"H\u016fla, J., Moj\u017e\u00ed\u0161ek, D., Janota, M.: Graph neural networks for scheduling of SMT solvers. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 447\u2013451 (2021). https:\/\/doi.org\/10.1109\/ICTAI52525.2021.00072","DOI":"10.1109\/ICTAI52525.2021.00072"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/978-3-030-51054-1_29","volume-title":"Automated Reasoning","author":"J Jakub\u016fv","year":"2020","unstructured":"Jakub\u016fv, J., Chvalovsk\u00fd, K., Ol\u0161\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: symbol-independent inference guiding\u00a0machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 448\u2013463. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29"},{"key":"18_CR28","unstructured":"Je\u017c, A.: Recompression: a simple and powerful technique for word equations (2014). https:\/\/arxiv.org\/abs\/1203.3705"},{"key":"18_CR29","unstructured":"Kipf, T.N., Welling, M.: Semi-supervised classification with graph convolutional networks. In: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, 24\u201326 April 2017, Conference Track Proceedings. OpenReview.net (2017). https:\/\/openreview.net\/forum?id=SJU4ayYgl"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Kumar, A., Manolios, P.: Mathematical programming modulo strings. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, 19\u201322 October 2021, pp. 261\u2013270. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/ISBN.978-3-85448-046-4_36","DOI":"10.34727\/2021\/ISBN.978-3-85448-046-4_36"},{"issue":"141\u2013146","key":"18_CR31","first-page":"82","volume":"36","author":"FW Levi","year":"1944","unstructured":"Levi, F.W.: On semigroups. Bull. Calcutta Math. Soc. 36(141\u2013146), 82 (1944)","journal-title":"Bull. Calcutta Math. Soc."},{"key":"18_CR32","unstructured":"Liang, C., R\u00fcmmer, P., Brockschmidt, M.: Exploring representation of horn clauses using GNNs. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, Israel, 11\u201312 August 2022. CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3201\/paper7.pdf"},{"key":"18_CR33","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. Sb. (N.S.) 103(145)(2(6)), 147\u2013236 (1977)"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.A.: Grasp: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 506\u2013521 (1999). https:\/\/api.semanticscholar.org\/CorpusID:13039801","DOI":"10.1109\/12.769433"},{"key":"18_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Nielsen, J.: Die Isomorphismen der allgemeinen, unendlichen Gruppe mit zwei Erzeugenden. Mathematische Annalen 78, 385\u2013397 (1917). https:\/\/api.semanticscholar.org\/CorpusID:119726936","DOI":"10.1007\/BF01457113"},{"key":"18_CR37","unstructured":"Pin, J.E., Perrin, D.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier (2004). https:\/\/hal.science\/hal-00112831"},{"key":"18_CR38","doi-asserted-by":"publisher","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: 40th Annual Symposium on Foundations of Computer Science (Cat. No. 99CB37039), pp. 495\u2013500 (1999). https:\/\/doi.org\/10.1109\/SFFCS.1999.814622","DOI":"10.1109\/SFFCS.1999.814622"},{"key":"18_CR39","unstructured":"Power, J.F.: Thue\u2019s 1914 paper: a translation. CoRR abs\/1308.5858 (2013). http:\/\/arxiv.org\/abs\/1308.5858"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Selsam, D., Bj\u00f8rner, N.: Neurocore: guiding high-performance SAT solvers with unsat-core predictions. CoRR abs\/1903.04671 (2019)","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"18_CR41","unstructured":"Selsam, D., Lamm, M., B\u00fcnz, B., Liang, P., de\u00a0Moura, L., Dill, D.L.: Learning a SAT solver from single-bit supervision. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May 2019. OpenReview.net (2019). https:\/\/openreview.net\/forum?id=HJMC_iA5tm"},{"key":"18_CR42","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol.\u00a031. Curran Associates, Inc. (2018)"},{"key":"18_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-53291-8_9","volume-title":"Computer Aided Verification","author":"X Si","year":"2020","unstructured":"Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2Inv: a deep learning framework for program verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 151\u2013164. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_9"},{"key":"18_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-79876-5_31","volume-title":"Automated Deduction \u2013 CADE 28","author":"M Suda","year":"2021","unstructured":"Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 543\u2013561. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31"},{"key":"18_CR45","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS 2017, pp. 2783\u20132793. Curran Associates Inc., Red Hook (2017)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:04:24Z","timestamp":1757887464000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}