{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:01:03Z","timestamp":1784239263537,"version":"3.55.0"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["25-18318S"],"award-info":[{"award-number":["25-18318S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001823","name":"Czech Ministry of Education, Youth and Sports","doi-asserted-by":"crossref","award":["LL1908"],"award-info":[{"award-number":["LL1908"]}],"id":[{"id":"10.13039\/501100001823","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100017520","name":"FIT BUT","doi-asserted-by":"crossref","award":["FIT-S-23-8151"],"award-info":[{"award-number":["FIT-S-23-8151"]}],"id":[{"id":"10.13039\/501100017520","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Brno City Municipality","award":["Brno Ph.D. Talent"],"award-info":[{"award-number":["Brno Ph.D. Talent"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    We introduce a novel decision procedure for solving the class of\n                    <jats:italic toggle=\"yes\">position string constraints<\/jats:italic>\n                    , which includes string disequalities,\n                    <jats:italic toggle=\"yes\">\u00acprefixof, \u00acsujfixof, str.at<\/jats:italic>\n                    , and\n                    <jats:italic toggle=\"yes\">\u00acstr.at.<\/jats:italic>\n                    These constraints are generated frequently in almost any application of string constraint solving. Our procedure avoids expensive encoding of the constraints to word equations and, instead, reduces the problem to checking conflicts on positions satisfying an integer constraint obtained from the Parikh image of a polynomial-sized finite automaton with a special structure. By the reduction to counting, solving position constraints becomes NP-complete and for some cases even falls into PT\n                    <jats:monospace>IME<\/jats:monospace>\n                    . This is much cheaper than the previously used techniques, which either used reductions generating word equations and length constraints (for which modern string solvers use exponential-space algorithms) or incomplete techniques. Our method is relevant especially for automata-based string solvers, which have recently achieved the best results in terms of practical efficiency, generality, and completeness guarantees. This work allows them to excel also on position constraints, which used to be their weakness. Besides the efficiency gains, we show that our framework may be extended to solve a large fragment of\n                    <jats:italic toggle=\"yes\">\u00accontains<\/jats:italic>\n                    (in NE\n                    <jats:monospace>XP<\/jats:monospace>\n                    T\n                    <jats:monospace>IME<\/jats:monospace>\n                    ), for which decidability has been long open, and gives a hope to solve the general problem. Our implementation of the technique within the Z3-N\n                    <jats:monospace>OODLER<\/jats:monospace>\n                    solver significantly improves its performance on position constraints.\n                  <\/jats:p>","DOI":"10.1145\/3729273","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"550-575","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Uniform Framework for Handling Position Constraints in String Solving"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Brno, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2428-8547","authenticated-orcid":false,"given":"Michal","family":"He\u010dko","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Brno, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Brno, Czech Republic"},{"name":"Aalborg University, Aalborg, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Brno, Czech Republic"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2024. SMT-COMP\u203224. https:\/\/smt-comp.github.io\/2024\/"},{"key":"e_1_3_2_3_2","unstructured":"2024. SMT-COMP\u203224 QF Strings https:\/\/smt-comp.github.io\/2024\/results\/qf_strings-single-query\/"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_17"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062384"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926454"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_1"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_13_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2898375.2898393"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Murphy Berzish Joel D. Day Vijay Ganesh Mitja Kulczynski Florin Manea Federico Mora and Dirk Nowotka. 2023. Towards More Efficient Methods for Solving Regular-expression Heavy String Constraints. Theor. Comput. Sei. 943 (2023) 50\u201372. doi:10.1016\/j.tcs.2022.12.009","DOI":"10.1016\/j.tcs.2022.12.009"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158091"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498707"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622872"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_2"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_18"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622872"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Yu-Fang Chen Vojt\u00e9ch Havlena Michal He\u0451ko Luk\u00e2\u00e4 Hol\u00edk and Ondrej Leng\u00e2l. 2025. Artifact: A Uniform Framework for Handling Position Constraints for String Solving. Zenodo. doi:10.5281\/zenodo.15050654","DOI":"10.5281\/zenodo.15050654"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen Vojt\u00e9ch Havlena Michal He\u0451ko Luk\u00e2\u00e4 Hol\u00edk and Ondrej Leng\u00e2l. 2025. A Uniform Framework for Handling Position Constraints in String Solving (Technical Report). arXiv:2504.07033 [cs.LO]https:\/\/arxiv.org\/abs\/2504.07033","DOI":"10.1145\/3729273"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Yu-Fang Chen Vojt\u00e9ch Havlena Ondrej Leng\u00e2l and Andrea Turrini. 2023. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software 201 (2023) 111673. doi:10.1016\/j.jss.2023.111673","DOI":"10.1016\/j.jss.2023.111673"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_7"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00224-023-10154-8"},{"key":"e_1_3_2_33_2","article-title":"The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability","author":"Day Joel D.","year":"2018","unstructured":"Joel D. Day, Vijay Ganesh, Paul He, Florin Manea, and Dirk Nowotka. 2018. The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability. CoRR abs\/1802.00523 (2018). http:\/\/arxiv.org\/abs\/1802.00523","journal-title":"CoRR"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02112533"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603092"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_8"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2024.14"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158092"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"John E. Hopcroft and Jean-Jacques Pansiot. 1979. On the Reachability Problem for 5-Dimensional Vector Addition Systems. Theor. Comput. Sei. 8 (1979) 135\u2013159. doi:10.1016\/0304-3975(79)90041-0","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1#0x005F;10"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45093-9_59"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/2743014"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Ankit Jha Rosemary Monahan and Hao Wu. 2023. Verifying UML Models Annotated with OCL Strings. In Proceedings of the 26th International Conference on Model Driven Engineering Languages and Systems (MODELS). 123\u2013132. doi:10.1145\/3652620.3687822","DOI":"10.1145\/3652620.3687822"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_54"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_19"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/11562948_36"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24246-0_"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(4:4)2021"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2024\/211"},{"issue":"2","key":"e_1_3_2_58_2","first-page":"147","article-title":"The problem of solvability of equations in a free semigroup","volume":"32","author":"Makanin G. S.","year":"1977","unstructured":"G. S. Makanin. 1977. The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 32, 2 (1977), 147\u2013236.(in Russian)..","journal-title":"Matematicheskii Sbornik"},{"issue":"1","key":"e_1_3_2_59_2","first-page":"196","article-title":"Undecidability of the positive V\u2203-theory of a free semigroup","volume":"23","author":"Marchenkov S. S.","year":"1982","unstructured":"S. S. Marchenkov. 1982. Undecidability of the positive V\u2203-theory of a free semigroup. Sibirsk. Mat. Zh. 23, 1 (1982), 196\u2013198, 223.","journal-title":"Sibirsk. Mat. Zh."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259006"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_21"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457113"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_12"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/322276.322287"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFFCS.1999.814622"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Mathias Preiner Hans-J\u00f6rg Schurr Clark Barrett Pascal Fontaine Aina Niemetz and Cesare Tinelli. 2024. SMT-LIB release 2024 (non-incremental benchmarks). doi:10.5281\/zenodo.11061097","DOI":"10.5281\/zenodo.11061097"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_2"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_30"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_24"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59776-8_5"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_3_2_74_2","unstructured":"Wei-Lun Tsai. 2021. PyCT. https:\/\/github.com\/alan23273850\/PyCT"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3040488"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_13"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111009112"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-40x005F;14"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729273","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:08:38Z","timestamp":1784196518000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729273"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":80,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729273"],"URL":"https:\/\/doi.org\/10.1145\/3729273","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}