论文标题
具有长度约束，计数器系统和前脉动算术的二次单词方程式（具有分裂性）
Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
论文作者
论文摘要
单词方程是解决弦的约束解决的理论基础中的关键要素。单词方程式在字符串变量和常数上关联了两个单词。它的解决方案相当于函数映射变量到等同于方程的左侧和右侧的恒定字符串。尽管求解单词方程的问题是可以决定的，但解决具有长度约束的单词方程的问题的可决定性（即，与单词方程式中的单词长度相关的约束）仍然是一个长期的开放问题。我们专注于二次词方程的子类，即每个变量最多发生两次。我们首先表明二次单词方程的解决方案的长度抽象通常不可定义。然后，我们描述一类具有前堡过渡关系的反系统，该系统捕获具有常规约束的二次单词方程的长度抽象。我们提供了对计数器系统的简单循环的效果的编码，这些循环在伯堡算术的存在理论中具有分解性（PAD）的效果。由于PAD是可决定的（NP-HARD，并且在NEXP中），因此我们获得了具有长度约束的二次单词方程式的决策过程，该方程的长度约束，相关的计数器系统是平坦的（即，所有节点最多属于一个循环）。特别是，当最近提出的单词方程式的NP完整片段称为常规单词方程时，我们显示了一个可确定性结果（实际上，也是带有垫Oracle的NP算法）。在存在常规约束的情况下，我们扩展了这种可决定性结果（实际上，Pspace与Pad Oracle的复杂性上限）。
Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function mapping variables to constant strings that equate the left and right hand sides of the equation. While the problem of solving word equations is decidable, the decidability of the problem of solving a word equation with a length constraint (i.e., a constraint relating the lengths of words in the word equation) has remained a long-standing open problem. We focus on the subclass of quadratic word equations, i.e., in which each variable occurs at most twice. We first show that the length abstractions of solutions to quadratic word equations are in general not Presburger-definable. We then describe a class of counter systems with Presburger transition relations which capture the length abstraction of a quadratic word equation with regular constraints. We provide an encoding of the effect of a simple loop of the counter systems in the existential theory of Presburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hard and is in NEXP), we obtain a decision procedure for quadratic words equations with length constraints for which the associated counter system is flat (i.e., all nodes belong to at most one cycle). In particular, we show a decidability result (in fact, also an NP algorithm with a PAD oracle) for a recently proposed NP-complete fragment of word equations called regular-oriented word equations, when augmented with length constraints. We extend this decidability result (in fact, with a complexity upper bound of PSPACE with a PAD oracle) in the presence of regular constraints.
