SpringerLink
Log in

Word Equations in the Context of String Solving

  • Conference paper
  • First Online:
Developments in Language Theory (DLT 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13257))

Included in the following conference series:

  • 465 Accesses

Abstract

String solvers are tools for automatically reasoning about words over some finite alphabet. They are commonly used to perform analyses of string manipulating programs. A fundamental problem which string solvers need to address is solving word equations, usually in combination with additional constraints involving e.g. string lengths or regular languages. In this article, a survey of results on the topic of word equations is presented with an emphasis on recent results which are relevant to the theoretical foundations of string solvers.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Since it is easy to simulate the intersection of regular languages via conjunctions of regular constraints, the satisfiability problem for formulas containing regular constraints is automatically PSPACE-hard. Therefore, we can convert between any reasonable choices for specifying regular languages without affecting the computational complexity.

  2. 2.

    These two viewpoints are not mutually exclusive as a word equation can be thought of as a compact representation of a solution.

  3. 3.

    Paths in which both vertices and edges may be repeated.

  4. 4.

    Non-erasing solutions are solutions for which h(x) is not the empty word for any variable x. The general case can be reduced to the non-erasing case by simply guessing in advance which variables should be mapped to the empty word and removing them from the word equation(s).

  5. 5.

    Where the length of the solution is measured in terms of the word obtained by applying it to one side of the equation.

  6. 6.

    A word is primitive if it cannot be written as the repetition of a strictly shorter word.

References

  1. OWASP top ten web application security risks. https://owasp.org/www-project-top-ten/. Accessed 15 Mar 2022

  2. SMT-LIB standard for unicode strings. https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml. Accessed 15 Mar 2022

  3. Abdulla, P.A., et al.: Norn: an SMT solver for string constraints. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462–469. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_29

    Chapter  Google Scholar 

  4. Abdulla, P.A., et al.: Efficient handling of string-number conversion. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 943–957 (2020)

    Google Scholar 

  5. Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150–166. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_10

    Chapter  Google Scholar 

  6. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proceedings of the 36th ACM Symposium on Theory of Computing (STOC), STOC 2004, pp. 202–211 (2004)

    Google Scholar 

  7. Amadini, R.: A survey on string constraint solving. ACM Comput. Surv. (CSUR) 55(1), 1–38 (2021)

    Article  Google Scholar 

  8. Angluin, D.: Finding patterns common to a set of strings. In: Proceedings of the Eleventh Annual ACM Symposium on Theory of Computing, pp. 130–141 (1979)

    Google Scholar 

  9. Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds) TACAS 2022. LNCS, vol. 13243, pp. 415–442. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_24

  10. Barceló, P., Muñoz, P.: Graph logics with rational relations: the role of word combinatorics. ACM Trans. Comput. Logic (TOCL) 18(2), 1–41 (2017)

    Article  MathSciNet  Google Scholar 

  11. Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England, vol. 13, p. 14 (2010)

    Google Scholar 

  12. Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307–321. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_27

    Chapter  MATH  Google Scholar 

  13. Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45–51. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_6

    Chapter  Google Scholar 

  14. Büchi, J.R., Senger, S.: Definability in the existential theory of concatenation and undecidable extensions of this theory. In: Mac Lane, S., Siefkes, D. (eds.) The Collected Works of J. Richard Büchi, pp. 671–683. Springer, New York (1990). https://doi.org/10.1007/978-1-4613-8928-6_37

    Chapter  Google Scholar 

  15. Bultan, T., Yu, F., Alkhalaf, M., Aydin, A.: String Analysis for Software Verification and Security, vol. 10. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68670-7

    Book  Google Scholar 

  16. Charatonik, W., Pacholski, L.: Word equations with two variables. In: Abdulrab, H., Pécuchet, J.-P. (eds.) IWWERT 1991. LNCS, vol. 677, pp. 43–56. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56730-5_30

    Chapter  MATH  Google Scholar 

  17. Chen, T., Hague, M., Lin, A.W., Rümmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3(POPL), 1–30 (2019)

    Google Scholar 

  18. Ciobanu, L., Diekert, V., Elder, M.: Solution sets for equations over free groups are EDT0L languages. Internat. J. Algebra Comput. 26(05), 843–886 (2016)

    Article  MathSciNet  Google Scholar 

  19. Ciobanu, L., Elder, M.: Solutions sets to systems of equations in hyperbolic groups are EDT0L in PSPACE. ar**v preprint ar**v:1902.07349 (2019)

  20. Czeizler, E.: The non-parametrizability of the word equation xyz = zvx: a short proof. Theoret. Comput. Sci. 345(2–3), 296–303 (2005)

    Article  MathSciNet  Google Scholar 

  21. Czeizler, E., Holub, Š, Karhumäki, J., Laine, M.: Intricacies of simple word equations: an example. Int. J. Found. Comput. Sci. 18(06), 1167–1175 (2007)

    Article  MathSciNet  Google Scholar 

  22. Da̧browski, R., Plandowski, W.: Solving two-variable word equations. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 408–419. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27836-8_36

    Chapter  Google Scholar 

  23. Dahmani, F., Guirardel, V.: Foliations for solving equations in groups: free, virtually free, and hyperbolic groups. J. Topol. 3(2), 343–404 (2010)

    Article  MathSciNet  Google Scholar 

  24. Day, J.D., et al.: On solving word equations using SAT. In: Filiot, E., Jungers, R., Potapov, I. (eds.) RP 2019. LNCS, vol. 11674, pp. 93–106. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30806-3_8

    Chapter  Google Scholar 

  25. Day, J.D., Ganesh, V., Grewal, N., Manea, F.: Formal languages via theories over strings: What’s decidable? Unpublished manuscript

    Google Scholar 

  26. Day, J.D., Ganesh, V., He, P., Manea, F., Nowotka, D.: The satisfiability of word equations: decidable and undecidable theories. In: Potapov, I., Reynier, P.-A. (eds.) RP 2018. LNCS, vol. 11123, pp. 15–29. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00250-3_2

    Chapter  Google Scholar 

  27. Day, J.D., Kröger, A., Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: BASC: benchmark analysis for string constraints. Unpublished manuscript

    Google Scholar 

  28. 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, pp. 87–97 (2020)

    Google Scholar 

  29. Day, J.D., Manea, F.: On the structure of solution-sets to regular word equations. In: Theory of Computing Systems, pp. 1–78 (2021)

    Google Scholar 

  30. Day, J.D., Manea, F., Nowotka, D.: The hardness of solving simple word equations. In: 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  31. Day, J.D., Manea, F., Nowotka, D.: Upper bounds on the length of minimal solutions to certain quadratic word equations. In: 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)

    Google Scholar 

  32. Diekert, V.: More than 1700 years of word equations. In: Maletti, A. (ed.) CAI 2015. LNCS, vol. 9270, pp. 22–28. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23021-4_2

    Chapter  Google Scholar 

  33. Diekert, V., Gutierrez, C., Hagenah, C.: The existential theory of equations with rational constraints in free groups is PSPACE-complete. Inf. Comput. 202(2), 105–140 (2005)

    Article  MathSciNet  Google Scholar 

  34. Diekert, V., Jeż, A., Plandowski, W.: Finding all solutions of equations in free groups and monoids with involution. Inf. Comput. 251, 263–286 (2016)

    Article  MathSciNet  Google Scholar 

  35. Diekert, V., Muscholl, A.: Solvability of equations in free partially commutative groups is decidable. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 543–554. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-48224-5_45

    Chapter  Google Scholar 

  36. Durnev, V.G.: Undecidability of the positive \(\forall \exists ^3\)-theory of a free semigroup. Sib. Math. J. 36(5), 917–929 (1995)

    Article  MathSciNet  Google Scholar 

  37. Freydenberger, D.D.: A logic for document spanners. Theory Comput. Syst. 63(7), 1679–1754 (2019)

    Article  MathSciNet  Google Scholar 

  38. Freydenberger, D.D., Peterfreund, L.: The theory of concatenation over finite models. In: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021)

    Google Scholar 

  39. Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209–226. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39611-3_21

    Chapter  Google Scholar 

  40. Hague, M.: Strings at MOSCA. ACM SIGLOG News 6(4), 4–22 (2019)

    Article  Google Scholar 

  41. Halfon, S., Schnoebelen, P., Zetzsche, G.: Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 1–12. IEEE (2017)

    Google Scholar 

  42. Harju, T., Nowotka, D.: On the independence of equations in three variables. Theoret. Comput. Sci. 307(1), 139–172 (2003)

    Article  MathSciNet  Google Scholar 

  43. Harju, T., Nowotka, D.: On the equation \(x^k = z_1^{k_1}z_2^{k_2} \cdots z_n^{k_n}\) in a free semigroup. Theoret. Comput. Sci. 330(1), 117–121 (2005)

    Article  MathSciNet  Google Scholar 

  44. Hmelevskii, J.I.: Equations in free semigroups, volume 107 of Am. Math. Soc. Transl. Proc. Steklov and Insti. Mat (1976)

    Google Scholar 

  45. Holik, L., Janku, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the ACM on Programming Languages, vol. 2, pp. 1–32. ACM Digital Library (2018)

    Google Scholar 

  46. Holub, Š, Kortelainen, J.: On systems of word equations with simple loop sets. Theoret. Comput. Sci. 380(3), 363–372 (2007)

    Article  MathSciNet  Google Scholar 

  47. Holub, Š., Starosta, Š.: Formalization of basic combinatorics on words. In: 12th International Conference on Interactive Theorem Proving (ITP 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021)

    Google Scholar 

  48. Holub, Š, Žemlička, J.: Algebraic properties of word equations. J. Algebra 434, 283–301 (2015)

    Article  MathSciNet  Google Scholar 

  49. Ilie, L., Plandowski, W.: Two-variable word equations. RAIRO-Theoret. Inform. Appl. 34(6), 467–501 (2000)

    Article  MathSciNet  Google Scholar 

  50. Jain, S., Ong, Y.S., Stephan, F.: Regular patterns, regular languages and context-free languages. Inf. Process. Lett. 110(24), 1114–1119 (2010)

    Article  MathSciNet  Google Scholar 

  51. Jeż, A.: One-variable word equations in linear time. Algorithmica 74(1), 1–48 (2016)

    Article  MathSciNet  Google Scholar 

  52. Jeż, A.: Recompression: a simple and powerful technique for word equations. J. ACM (JACM) 63(1), 1–51 (2016)

    Article  MathSciNet  Google Scholar 

  53. Jeż, A.: Word equations in non-deterministic linear space. J. Comput. Syst. Sci. 123, 122–142 (2022)

    Article  MathSciNet  Google Scholar 

  54. Kan, S., Lin, A.W., Rümmer, P., Schrader, M.: CertiStr: a certified string solver. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 210–224 (2022)

    Google Scholar 

  55. Karhumäki, J., Mignosi, F., Plandowski, W.: The expressibility of languages and relations by word equations. J. ACM (JACM) 47(3), 483–505 (2000)

    Article  MathSciNet  Google Scholar 

  56. Karhumäki, J., Saarela, A.: On maximal chains of systems of word equations. Proc. Steklov Inst. Math. 274(1), 116–123 (2011)

    Article  MathSciNet  Google Scholar 

  57. Kiezun, A., Ganesh, V., Artzi, S., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol. (TOSEM) 21(4), 1–28 (2013)

    Article  Google Scholar 

  58. Kulczynski, M., Manea, F., Nowotka, D., Poulsen, D.B.: ZaligVinder: a generic test framework for string solvers. J. Softw. Evol. Process, e2400 (2021)

    Google Scholar 

  59. Laine, M., Plandowski, W.: Word equations with one unknown. Int. J. Found. Comput. Sci. 22(02), 345–375 (2011)

    Article  MathSciNet  Google Scholar 

  60. Lin, A.W., Barceló, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 123–136 (2016)

    Google Scholar 

  61. Lothaire, M.: Algebraic Combinatorics on Words, vol. 90. Cambridge University Press, Cambridge (2002)

    Google Scholar 

  62. Majumdar, R., Lin, A.W.: Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility. Log. Meth. Comput. Sci. 17 (2021)

    Google Scholar 

  63. Makanin, G.S.: Decidability of the universal and positive theories of a free group. Math. USSR-Izvestiya 25(1), 75 (1985)

    Article  Google Scholar 

  64. Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147–236 (1977)

    MathSciNet  MATH  Google Scholar 

  65. Makanin, G.S.: Equations in a free group. Math. USSR-Izvestiya 21(3), 483 (1983)

    Article  Google Scholar 

  66. Manea, F., Nowotka, D., Schmid, M.L.: On the complexity of solving restricted word equations. Int. J. Found. Comput. Sci. 29(05), 893–909 (2018)

    Article  MathSciNet  Google Scholar 

  67. Maňuch, J.: Characterization of a word by its subwords. In: Developments in Language Theory: Foundations, Applications, and Perspectives, pp. 210–219. World Scientific (2000)

    Google Scholar 

  68. Mora, F., Berzish, M., Kulczynski, M., Nowotka, D., Ganesh, V.: Z3str4: a multi-armed string solver. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 389–406. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_21

    Chapter  Google Scholar 

  69. Nepeivoda, A.: Program specialization as a tool for solving word equations. In: Electronic Proceedings in Theoretical Computer Science, EPTCS, pp. 42–72 (2021)

    Google Scholar 

  70. Nowotka, D., Saarela, A.: One-variable word equations and three-variable constant-free word equations. Int. J. Found. Comput. Sci. 29(05), 935–950 (2018)

    Article  MathSciNet  Google Scholar 

  71. Nowotka, D., Saarela, A.: An optimal bound on the solution sets of one-variable word equations and its consequences. SIAM J. Comput. 51(1), 1–18 (2022)

    Article  MathSciNet  Google Scholar 

  72. Petre, E.: An elementary proof for the non-parametrizability of the equation xyz=zvx. In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 807–817. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28629-5_63

    Chapter  MATH  Google Scholar 

  73. Plandowski, W.: Satisfiability of word equations with constants is in NEXPTIME. In: Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, pp. 721–725 (1999)

    Google Scholar 

  74. Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM (JACM) 51(3), 483–496 (2004)

    Article  MathSciNet  Google Scholar 

  75. Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing, pp. 467–476 (2006)

    Google Scholar 

  76. Plandowski, W., Rytter, W.: Application of Lempel-Ziv encodings to the solution of word equations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 731–742. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055097

    Chapter  Google Scholar 

  77. Quine, W.V.: Concatenation as a basis for arithmetic. J. Symbolic Logic 11(4), 105–114 (1946)

    Article  MathSciNet  Google Scholar 

  78. Razborov, A.A.: On systems of equations in free groups. In: Combinatorial and Geometric Group Theory, pp. 269–283 (1993)

    Google Scholar 

  79. Robson, J.M., Diekert, V.: On quadratic word equations. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 217–226. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49116-3_20

    Chapter  Google Scholar 

  80. Saarela, A.: Word equations with kth powers of variables. J. Comb. Theory Ser. A. 165, 15–31 (2019)

    Article  Google Scholar 

  81. Saarela, A.: Hardness results for constant-free pattern languages and word equations. In: 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2020)

    Google Scholar 

  82. Schulz, K.U.: Makanin’s algorithm for word equations-two improvements and a generalization. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 85–150. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55124-7_4

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Loughborough University, Loughborough, UK

    Joel D. Day

Authors
  1. Joel D. Day
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joel D. Day .

Editor information

Editors and Affiliations

  1. University of Stuttgart, Stuttgart, Baden-Württemberg, Germany

    Volker Diekert

  2. Ural Federal University, Ekaterinburg, Russia

    Mikhail Volkov

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Day, J.D. (2022). Word Equations in the Context of String Solving. In: Diekert, V., Volkov, M. (eds) Developments in Language Theory. DLT 2022. Lecture Notes in Computer Science, vol 13257. Springer, Cham. https://doi.org/10.1007/978-3-031-05578-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-05578-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-05577-5

  • Online ISBN: 978-3-031-05578-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation