The Satisfiability of Word Equations: Decidable and Undecidable Theories
The Satisfiability of Word Equations: Decidable and Undecidable Theories
复制标题
DOI：
10.1007/978-3-030-00250-3_2
复制
发表时间：
2018-09
期刊：
影响因子：
--
通讯作者：
Joel D. Day;Vijay Ganesh;Paul He;F. Manea;Dirk Nowotka
中科院分区：
文献类型：
--
作者：
Joel D. Day;Vijay Ganesh;Paul He;F. Manea;Dirk Nowotka
单词方程的研究是数学和理论计算机科学中的一个中心课题。最近，在用于安全分析的字符串SMT解算器的上下文中，给定的词等式是否具有用各种约束/扩展扩充的解的问题已经变得至关重要。我们考虑了这个问题在几个自然变量中的可判定性，从而阐明了一阶词方程理论及其推广的许多片段的可判定性和不可判定性之间的界限。特别是，我们证明了当扩展到单词上的几个自然谓词时，存在片段变得不可判定。另一方面，正分段是可判定的，并且在方程式中最多出现一个终端符号的情况下，即使添加了长度约束，也是如此。此外，如果允许求反，则可以仅使用包含单个端子符号和长度约束的方程来模拟具有长度约束的任意方程。最后，我们证明了在非确定多项式时间内，判定一类带有许多谓词的受限方程是否存在解是可能的，从而导致一般情况下的不可判定。
The study of word equations is a central topic in mathematics and theoretical computer science. Recently, the question of whether a given word equation, augmented with various constraints/extensions, has a solution has gained critical importance in the context of string SMT solvers for security analysis. We consider the decidability of this question in several natural variants and thus shed light on the boundary between decidability and undecidability for many fragments of the first order theory of word equations and their extensions. In particular, we show that when extended with several natural predicates on words, the existential fragment becomes undecidable. On the other hand, the positivefragment is decidable, and in the case that at most one terminal symbol appears in the equations, remains so even when length constraints are added. Moreover, if negation is allowed, it is possible to model arbitrary equations with length constraints using only equations containing a single terminal symbol and length constraints. Finally, we show that deciding whether solutions exist for a restricted class of equations, augmented with many of the predicates leading to undecidability in the general case, is possible in non-deterministic polynomial time.