Word Equations in Nondeterministic Linear Space
Word Equations in Nondeterministic Linear Space
复制标题
非确定性线性空间中的词方程
DOI：
10.4230/lipics.icalp.2017.95
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Artur Jeż
中科院分区：
文献类型：
--
作者：
Artur Jeż
词方程的可满足性是形式语言和代数交叉中的一个重要问题：给定两个由字母和变量组成的序列，我们要决定是否存在变量的替换，从而将该方程变成真正的字符串相等。该问题的计算复杂度仍然未知，最佳下限和上限分别为 NP 和 PSPACE。最近，重新压缩的新技术被应用于这个问题，简化了已知的证明并将空间复杂度降低到（不确定的）O(n log n)。在本文中，我们证明词方程的可满足性是在非确定性线性空间中，因此可满足词方程的语言是上下文相关的。我们使用已知的基于再压缩的算法，并另外对字母采用霍夫曼编码。然而，证明使用了对方程片段如何相互依赖的分析，以及算法的非确定性选择的新策略，该策略使用了几种新的想法来限制字母占用的空间。
Satisfiability of word equations is an important problem in the intersection of formal languages and algebra: Given two sequences consisting of letters and variables we are to decide whether there is a substitution for the variables that turns this equation into true equality of strings. The computational complexity of this problem remains unknown, with the best lower and upper bounds being, respectively, NP and PSPACE. Recently, the novel technique of recompression was applied to this problem, simplifying the known proofs and lowering the space complexity to (nondeterministic) O(n log n). In this paper we show that satisfiability of word equations is in nondeterministic linear space, thus the language of satisfiable word equations is context-sensitive. We use the known recompression-based algorithm and additionally employ Huffman coding for letters. The proof, however, uses analysis of how the fragments of the equation depend on each other as well as a new strategy for nondeterministic choices of the algorithm, which uses several new ideas to limit the space occupied by the letters.