一句话：通过计数器系统与带整除 Presburger 算术，给出 flat 二次词方程长度约束的可判定性与复杂度上界。
词方程求解是可判定的，但加入长度约束后的可判定性长期未决。本文聚焦每个变量至多出现两次的二次词方程。作者先证明二次词方程解的长度抽象一般不是 Presburger 可定义的；随后定义一类带 Presburger 迁移关系的计数器系统，用以刻画带正则约束的二次词方程的长度抽象。关键步骤是把计数器系统中简单循环的效果编码进带整除的 Presburger 算术（PAD）的存在理论。由于 PAD 可判定（NP-hard 且属于 NEXP），得到当关联计数器系统为 flat（每个节点至多属于一个循环）时带长度约束二次词方程的可判定性。对最近提出的 NP-完全片段 regular-oriented word equations，加入长度约束后也可判定，并给出带 PAD 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{LinM18,
title = {Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility},
author = {Anthony W. Lin and Rupak Majumdar},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:4)2021}
}