Solving Equations on Words with Morphisms and Antimorphisms

  • Alexandre Blondin Massé
  • Sébastien Gaboury
  • Sylvain Hallé
  • Michaël Larouche
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8370)


Word equations are combinatorial equalities between strings of symbols, variables and functions, which can be used to model problems in a wide range of domains. While some complexity results for the solving of specific classes of equations are known, currently there does not exist any equation solver publicly available. Recently, we have proposed the implementation of such a solver based on Boolean satisfiability that leverages existing SAT solvers for this purpose. In this paper, we propose a new representation of equations on words having fixed length, by using an enriched graph data structure. We discuss the implementation as well as experimental results obtained on a sample of equations.


Word Length String Constraint Boundary Word Alphabet Size Reversal Operator 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abdulrab, H.: Implementation of Makanin’s algorithm. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 61–84. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  2. 2.
    Blondin Massé, A., Garon, A., Labbé, S.: Generation of double square tiles. Theoretical Computer Science (2012) (to appear)Google Scholar
  3. 3.
    Brlek, S.: Interactions between digital geometry and combinatorics on words. In: Ambroz, P., Holub, S., Masáková, Z. (eds.) WORDS. EPTCS, vol. 63, pp. 1–12 (2011)Google Scholar
  4. 4.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Fraenkel, A.S., Simpson, J.: How many squares can a string contain? Journal of Combinatorial Theory, Series A 82(1), 112 – 120 (1998),
  6. 6.
    Fu, X., Li, C.-C.: A string constraint solver for detecting web application vulnerability. In: SEKE, pp. 535–542. Knowledge Systems Institute Graduate School (2010)Google Scholar
  7. 7.
    Gusfield, D.: Algorithms on strings, trees, and sequences: computer science and computational biology. Cambridge Univ. Press (January 2007),
  8. 8.
    Kiezun, A., Ganesh, V., Artzi, S., Guo, P., Hooimeijer, P., Ernst, M.: HAMPI: A solver for word equations over strings, regular expressions and context-free grammars. ACM Trans. on Software Engineering and Methodology 21(4) (2012) (to appear)Google Scholar
  9. 9.
    Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hampi: a solver for string constraints. In: Rothermel, G., Dillon, L.K. (eds.) ISSTA, pp. 105–116. ACM (2009)Google Scholar
  10. 10.
    Larouche, M., Blondin Mass, A., Gaboury, S., Hall, S.: Solving equations on words through Boolean satisfiability. In: Maldonado, J.C., Shin, S.Y. (eds.) SAC, pp. 104–106. ACM (2013)Google Scholar
  11. 11.
    Lothaire, M.: Algebraic Combinatorics on Words. Cambridge University Press (2002)Google Scholar
  12. 12.
    Lothaire, M.: Applied Combinatorics on Words (Encyclopedia of Mathematics and its Applications). Cambridge University Press, New York (2005)CrossRefGoogle Scholar
  13. 13.
    Makanin, G.: The problem of solvability of equations in a free semigroup. Mathematics of the USSR-Sbornik 32(2), 129 (1977)CrossRefzbMATHGoogle Scholar
  14. 14.
    Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: FOCS, pp. 495–500. IEEE Computer Society (1999)Google Scholar
  15. 15.
    Yu, F., Bultan, T., Ibarra, O.H.: Relational string verification using multi-track automata. Int. J. Found. Comput. Sci. 22(8), 1909–1924 (2011)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Alexandre Blondin Massé
    • 1
  • Sébastien Gaboury
    • 1
  • Sylvain Hallé
    • 1
  • Michaël Larouche
    • 1
  1. 1.Laboratoire d’informatique formelleUniversité du Québec à ChicoutimiChicoutimiCanada

Personalised recommendations