一句话：提出基于自动机 Parikh 像归约的位置字符串约束判定过程，避免词方程编码并提升求解效率。
本文针对字符串约束求解中常见的位置约束（如字符串不等、¬prefixof、¬suffixof、str.at 及其否定）提出统一的判定过程。方法不将约束编码为词方程，而是归约为：在特定结构的多项式大小有限自动机的 Parikh 像所导出整数约束下，检查位置冲突。该归约将问题转化为计数，证明位置约束求解为 NP 完全，部分情形属于 PTIME，较此前指数空间词方程/长度约束方法或不完备方法更高效。作者还扩展框架以 NEXPTIME 求解一大类 ¬contains，长期开放的可判定性问题取得进展。在 Z3-NOODLER 中的实现显著提升了位置约束求解性能。
We introduce a novel decision procedure for solving the class of position string constraints , which includes string disequalities, ¬prefixof, ¬sujfixof, str.at , and ¬str.at. These constraints are generated frequently in almost any application of string constraint solving. Our procedure avoids expensive encoding of the constraints to word equations and, instead, reduces the problem to checking conflicts on positions satisfying an integer constraint obtained from the Parikh image of a polynomial-sized finite automaton with a special structure. By the reduction to counting, solving position constraints becomes NP-complete and for some cases even falls into PT IME . This is much cheaper than the previously used techniques, which either used reductions generating word equations and length constraints (for which modern string solvers use exponential-space algorithms) or incomplete techniques. Our method is relevant especially for automata-based string solvers, which have recently achieved the best results in terms of practical efficiency, generality, and completeness guarantees. This work allows them to excel also on position constraints, which used to be their weakness. Besides the efficiency gains, we show that our framework may be extended to solve a large fragment of ¬contains (in NE XP T IME ), for which decidability has been long open, and gives a hope to solve the general problem. Our implementation of the technique within the Z3-N OODLER solver significantly improves its performance on position constraints.
@article{paperbot3077,
title = {A Uniform Framework for Handling Position Constraints in String Solving},
author = {Yu-Fang Chen and Vojtěch Havlena and Michal Hečko and Lukáš Holík and Ondřej Lengál},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729273}
}