带长度约束的二次字方程、计数器系统与带整除的Presburger算术
计算机科学中的逻辑
2023-06-22 v6 形式语言与自动机理论
摘要
字方程是字符串约束求解理论基石中的关键要素。字方程关联了两个关于字符串变量与常量的词。其解等价于一个将变量映射到常数字符串、并使方程左右两边相等的函数。尽管求解字方程的问题是可判定的，但求解带长度约束（即关联字方程中各词长度之约束）的字方程问题的可判定性，长期以来一直是一个悬而未决的开放问题。我们聚焦于二次字方程这一子类，即每个变量至多出现两次。我们首先证明，二次字方程解的“长度抽象”一般而言并非Presburger可定义的。接着我们描述了一类具有Presburger转移关系的计数器系统，其刻画了带正则约束的二次字方程的长度抽象。我们给出了计数器系统简单循环之效应在带整除的Presburger算术存在理论（PAD）中的一种编码。由于PAD是可判定的（NP难且属于NEXP），我们获得了针对二次字方程带长度约束、且其关联计数器系统为平坦（即所有节点至多属于一个环）情形的判定过程。特别地，我们给出了一个针对近来提出的、被称为正则定向字方程的NP完全字方程片段在增补长度约束后的可判定性结果（事实上，还给出了一个带PAD预言机的NP算法）。我们将该可判定性结果（事实上，复杂度上界为带PAD预言机的PSPACE）推广到了存在正则约束的情形。
引用
@article{arxiv.2007.15478,
title = {Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility},
author = {Anthony W. Lin and Rupak Majumdar},
journal= {arXiv preprint arXiv:2007.15478},
year = {2023}
}
备注
arXiv admin note: substantial text overlap with arXiv:1805.06701