具有子词序和换能器的上下文无关字符串约束的可满足性

我们研究字符串约束的可满足性，其中可以对变量施加上下文无关的成员约束。此外，变量可能被约束为通过混洗变量及其换导得到的单词的子词。已知即使没有有理换导，可满足性问题也是不可判定的。如果没有换导，并且变量之间的子词关系没有循环依赖，则已知该问题是NExptime完全的。我们证明，即使添加了有理换导，该片段中的可满足性问题仍然是可判定的。对于上下文无关成员，它是2NExptime完全的；对于仅正则成员，它是NExptime完全的。对于下界，我们证明了一个具有独立兴趣的技术引理：下推自动机（大小为$O(n)$）与$n$个有限状态自动机（每个大小为$O(n)$）的交集中的最短单词的长度可以是$n$的双指数。