Document Open Access Logo

Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk)

Author Artur Jeż

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.3.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Author Details

Artur Jeż
  • University of Wrocław, Poland

Funding

Work supported under National Science Centre, Poland project number 2017/26/E/ST6/ 00191.

Cite As Get BibTex

Artur Jeż. Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.3

Abstract

In word equation problem we are given an equation u = v, where both u and v are words of letters and variables, and ask for a substitution of variables by words that equalizes the sides of the equation. This problem was first solved by Makanin and a different solution was proposed by Plandowski only 20 years later, his solution works in PSPACE, which is the best computational complexity bound known for this problem; on the other hand, the only known lower-bound is NP-hardness. In both cases the algorithms (and proofs) employed nontrivial facts on word combinatorics.
In the paper I will present an application of a recent technique of recompression, which simplifies the known proofs and (slightly) lowers the complexity to linear nondeterministic space. The technique is based on employing simple compression rules (replacement of two letters ab by a new letter c, replacement of maximal repetitions of a by a new letter), and modifying the equations (replacing a variable X by bX or Xa) so that those operations are sound and complete. In particular, no combinatorial properties of strings are used.
The approach turns out to be quite robust and can be applied to various generalizations and related scenarios (context unification, i.e. equations over terms; equations over traces, i.e. partially ordered words; ...).

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Formalisms
  • Theory of computation → Grammars and context-free languages
  • Theory of computation → Design and analysis of algorithms
  • Theory of computation → Tree languages
Keywords
  • word equation
  • context unification
  • equations in groups
  • compression

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Julius Richard Büchi and Steven Senger. Definability in the existential theory of concatenation and undecidable extensions of this theory. Mathematical Logic Quarterly, 34(4):337-342, 1988. URL: https://doi.org/10.1002/malq.19880340410.
  2. Witold Charatonik and Leszek Pacholski. Word equations with two variables. In IWWERT, pages 43-56, 1991. URL: https://doi.org/10.1007/3-540-56730-5_30.
  3. Laura Ciobanu, Volker Diekert, and Murray Elder. Solution sets for equations over free groups are EDT0L languages. IJAC, 26(5):843-886, 2016. URL: https://doi.org/10.1142/S0218196716500363.
  4. Hubert Comon. Completion of rewrite systems with membership constraints. Part I: Deduction rules. J. Symb. Comput., 25(4):397-419, 1998. URL: https://doi.org/10.1006/jsco.1997.0185.
  5. Hubert Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. Symb. Comput., 25(4):421-453, 1998. URL: https://doi.org/10.1006/jsco.1997.0186.
  6. Carles Creus, Adria Gascón, and Guillem Godoy. One-context unification with STG-compressed terms is in NP. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of LIPIcs, pages 149-164, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.149.
  7. Volker Diekert. Makanin’s Algorithm. In M. Lothaire, editor, Algebraic Combinatorics on Words, chapter 12, pages 342-390. Cambridge University Press, 2002. Google Scholar
  8. Volker Diekert, Claudio Gutiérrez, and Christian Hagenah. The existential theory of equations with rational constraints in free groups is PSPACE-complete. Inf. Comput., 202(2):105-140, 2005. URL: https://doi.org/10.1016/j.ic.2005.04.002.
  9. Volker Diekert, Artur Jeż, and Manfred Kufleitner. Solutions of word equations over partially commutative structures. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, ICALP, volume 55 of LIPIcs, pages 127:1-127:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.127.
  10. Volker Diekert, Artur Jeż, and Wojciech Plandowski. Finding all solutions of equations in free groups and monoids with involution. Inf. Comput., 251:263-286, 2016. URL: https://doi.org/10.1016/j.ic.2016.09.009.
  11. Volker Diekert and Anca Muscholl. Solvability of equations in free partially commutative groups is decidable. International Journal of Algebra and Computation, 16:1047-1070, 2006. Conference version in Proc. ICALP 2001, 543-554, LNCS 2076. URL: https://doi.org/10.1142/S0218196706003372.
  12. Robert Dąbrowski and Wojciech Plandowski. Solving two-variable word equations. In ICALP, pages 408-419, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_36.
  13. Robert Dąbrowski and Wojciech Plandowski. On word equations in one variable. Algorithmica, 60(4):819-828, 2011. URL: https://doi.org/10.1007/s00453-009-9375-3.
  14. William M. Farmer. Simple second-order languages for which unification is undecidable. Theor. Comput. Sci., 87(1):25-41, 1991. URL: https://doi.org/10.1016/S0304-3975(06)80003-4.
  15. Adria Gascón, Guillem Godoy, and Manfred Schmidt-Schauß. Context matching for compressed terms. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 93-102. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.17.
  16. Adria Gascón, Guillem Godoy, and Manfred Schmidt-Schauß. Unification and matching on compressed terms. ACM Trans. Comput. Log., 12(4):26, 2011. URL: https://doi.org/10.1145/1970398.1970402.
  17. Adria Gascón, Guillem Godoy, Manfred Schmidt-Schauß, and Ashish Tiwari. Context unification with one context variable. J. Symb. Comput., 45(2):173-193, 2010. URL: https://doi.org/10.1016/j.jsc.2008.10.005.
  18. Warren D. Goldfarb. The undecidability of the second-order unification problem. Theor. Comput. Sci., 13:225-230, 1981. URL: https://doi.org/10.1016/0304-3975(81)90040-2.
  19. Claudio Gutiérrez. Satisfiability of word equations with constants is in exponential space. In FOCS, pages 112-119, 1998. URL: https://doi.org/10.1109/SFCS.1998.743434.
  20. Lucian Ilie and Wojciech Plandowski. Two-variable word equations. ITA, 34(6):467-501, 2000. URL: https://doi.org/10.1051/ita:2000126.
  21. Joxan Jaffar. Minimal and complete word unification. J. ACM, 37(1):47-85, 1990. Google Scholar
  22. Artur Jeż. Context unification is in PSPACE. In Elias Koutsoupias, Javier Esparza, and Pierre Fraigniaud, editors, ICALP, volume 8573 of LNCS, pages 244-255. Springer, 2014. full version at http://arxiv.org/abs/1310.4367. URL: https://doi.org/10.1007/978-3-662-43951-7_21.
  23. Artur Jeż. One-variable word equations in linear time. Algorithmica, 74:1-48, 2016. URL: https://doi.org/10.1007/s00453-014-9931-3.
  24. Artur Jeż. Recompression: a simple and powerful technique for word equations. J. ACM, 63(1):4:1-4:51, March 2016. URL: https://doi.org/10.1145/2743014.
  25. Olga Kharlampovich and Alexei Myasnikov. Irreducible affine varieties over a free group. ii: Systems in triangular quasi-quadratic form and description of residually free groups. Journal of Algebra, 200:517–-570, 1998. Google Scholar
  26. Olga Kharlampovich and Alexei Myasnikov. Elementary theory of free non-abelian groups. Journal of Algebra, 302:451-552, 2006. Google Scholar
  27. Antoni Kościelski and Leszek Pacholski. Complexity of Makanin’s algorithm. J. ACM, 43(4):670-684, 1996. URL: https://doi.org/10.1145/234533.234543.
  28. Antoni Kościelski and Leszek Pacholski. Makanin’s algorithm is not primitive recursive. Theor. Comput. Sci., 191(1-2):145-156, 1998. URL: https://doi.org/10.1016/S0304-3975(96)00321-0.
  29. Markku Laine and Wojciech Plandowski. Word equations with one unknown. Int. J. Found. Comput. Sci., 22(2):345-375, 2011. URL: https://doi.org/10.1142/S0129054111008088.
  30. Jordi Levy. Linear second-order unification. In Harald Ganzinger, editor, RTA, volume 1103 of LNCS, pages 332-346. Springer, 1996. URL: https://doi.org/10.1007/3-540-61464-8_63.
  31. Jordi Levy, Manfred Schmidt-Schauß, and Mateu Villaret. On the complexity of bounded second-order unification and stratified context unification. Logic Journal of the IGPL, 19(6):763-789, 2011. URL: https://doi.org/10.1093/jigpal/jzq010.
  32. Jordi Levy and Margus Veanes. On the undecidability of second-order unification. Inf. Comput., 159(1-2):125-150, 2000. URL: https://doi.org/10.1006/inco.2000.2877.
  33. Jordi Levy and Mateu Villaret. Linear second-order unification and context unification with tree-regular constraints. In Leo Bachmair, editor, RTA, volume 1833 of LNCS, pages 156-171. Springer, 2000. URL: https://doi.org/10.1007/10721975_11.
  34. Jordi Levy and Mateu Villaret. Currying second-order unification problems. In Sophie Tison, editor, RTA, volume 2378 of LNCS, pages 326-339. Springer, 2002. URL: https://doi.org/10.1007/3-540-45610-4_23.
  35. Markus Lohrey. Algorithmics on SLP-compressed strings: A survey. Groups Complexity Cryptology, 4(2):241-299, 2012. Google Scholar
  36. Gennadií Makanin. The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik, 2(103):147-236, 1977. (in Russian). Google Scholar
  37. Gennadií Makanin. Equations in a free group. Izv. Akad. Nauk SSR, Ser. Math. 46:1199-1273, 1983. English transl. in Math. USSR Izv. 21 (1983). Google Scholar
  38. Gennadií Makanin. Decidability of the universal and positive theories of a free group. Izv. Akad. Nauk SSSR, Ser. Mat. 48:735-749, 1984. In Russian; English translation in: Math. USSR Izvestija, 25, 75-88, 1985. Google Scholar
  39. Yuri Matiyasevich. Some decision problems for traces. In Sergej Adian and Anil Nerode, editors, LFCS, volume 1234 of LNCS, pages 248-257. Springer, 1997. Invited lecture. Google Scholar
  40. Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. On equality up-to constraints over finite trees, context unification, and one-step rewriting. In William McCune, editor, CADE, volume 1249 of LNCS, pages 34-48. Springer, 1997. URL: https://doi.org/10.1007/3-540-63104-6_4.
  41. Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. A uniform approach to underspecification and parallelism. In Philip R. Cohen and Wolfgang Wahlster, editors, ACL, pages 410-417. Morgan Kaufmann Publishers / ACL, 1997. URL: https://doi.org/10.3115/979617.979670.
  42. S. Eyono Obono, Pavel Goralcik, and M. N. Maksimenko. Efficient solving of the word equations in one variable. In MFCS, pages 336-341, 1994. URL: https://doi.org/10.1007/3-540-58338-6_80.
  43. Wojciech Plandowski. Testing equivalence of morphisms on context-free languages. In Jan van Leeuwen, editor, ESA, volume 855 of LNCS, pages 460-470. Springer, 1994. URL: https://doi.org/10.1007/BFb0049431.
  44. Wojciech Plandowski. Satisfiability of word equations with constants is in NEXPTIME. In STOC, pages 721-725. ACM, 1999. URL: https://doi.org/10.1145/301250.301443.
  45. Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. J. ACM, 51(3):483-496, 2004. URL: https://doi.org/10.1145/990308.990312.
  46. Wojciech Plandowski. An efficient algorithm for solving word equations. In Jon M. Kleinberg, editor, STOC, pages 467-476. ACM, 2006. URL: https://doi.org/10.1145/1132516.1132584.
  47. Wojciech Plandowski and Wojciech Rytter. Application of Lempel-Ziv encodings to the solution of word equations. In Kim Guldstrand Larsen, Sven Skyum, and Glynn Winskel, editors, ICALP, volume 1443 of LNCS, pages 731-742. Springer, 1998. URL: https://doi.org/10.1007/BFb0055097.
  48. Alexander A. Razborov. On Systems of Equations in Free Groups. PhD thesis, Steklov Institute of Mathematics, 1987. In Russian. Google Scholar
  49. John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965. Google Scholar
  50. Aleksi Saarela. On the complexity of Hmelevskii’s theorem and satisfiability of three unknown equations. In Volker Diekert and Dirk Nowotka, editors, Developments in Language Theory, volume 5583 of LNCS, pages 443-453. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02737-6_36.
  51. Manfred Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/94, Johann-Wolfgang-Goethe-Universität, 1994. Google Scholar
  52. Manfred Schmidt-Schauß. A decision algorithm for stratified context unification. J. Log. Comput., 12(6):929-953, 2002. URL: https://doi.org/10.1093/logcom/12.6.929.
  53. Manfred Schmidt-Schauß. Decidability of bounded second order unification. Inf. Comput., 188(2):143-178, 2004. URL: https://doi.org/10.1016/j.ic.2003.08.002.
  54. Manfred Schmidt-Schauß and Klaus U. Schulz. On the exponent of periodicity of minimal solutions of context equation. In RTA, volume 1379 of LNCS, pages 61-75. Springer, 1998. URL: https://doi.org/10.1007/BFb0052361.
  55. Manfred Schmidt-Schauß and Klaus U. Schulz. Solvability of context equations with two context variables is decidable. J. Symb. Comput., 33(1):77-122, 2002. URL: https://doi.org/10.1006/jsco.2001.0438.
  56. Klaus U. Schulz. Makanin’s algorithm for word equations - two improvements and a generalization. In Klaus U. Schulz, editor, IWWERT, volume 572 of LNCS, pages 85-150. Springer, 1990. URL: https://doi.org/10.1007/3-540-55124-7_4.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact