一句话：将正则语言 Parikh 像推理转化为约束求解问题，提出 PC* 演算与工具 Catra，避免显式构造积自动机并显著加速字符串约束求解。
字符串约束求解器常需计算语言中字符计数的所有可能组合，即 Parikh 像；涉及长度、索引等整数操作时还要处理自动机乘积/交的 Parikh 像，显式计算既慢又耗内存。本文把 Parikh 像推理刻画为约束求解问题，无需显式计算乘积自动机或精确 Parikh 像即可回答查询，并将其实现为演算 PC*，嵌入支持 Presburger 逻辑的定理证明器，形成工具 Catra。实验在 Ostrich+ 对含整数操作的标准字符串约束基准所产生的约束上进行：PC* 大幅优于 Verma 等人的标准提取方法和 Janků 与 Turoňová 的过近似方法，在 60 秒超时下也优于 nuXmv。作为 Ostrich+ 的 Parikh 像后端后，它在 SMT-COMP 2023 QF_SLIA 赛道解决了最多 Unsat 实例。
A common problem in string constraint solvers is computing the Parikh image, a linear arithmetic formula that describes all possible combinations of character counts in strings of a given language. Automata-based string solvers frequently need to compute the Parikh image of products (or intersections) of finite-state automata, in particular when solving string constraints that also include the integer data-type due to operations like string length and indexing. In this context, the computation of Parikh images often turns out to be both prohibitively slow and memory-intensive. This paper contributes a new understanding of how the reasoning about Parikh images can be cast as a constraint solving problem, and questions about Parikh images be answered without explicitly computing the product automaton or the exact Parikh image. The paper shows how this formulation can be efficiently implemented as a calculus, PC*, embedded in an automated theorem prover supporting Presburger logic. The resulting standalone tool Catra is evaluate on constraints produced by the Ostrich+ string solver when solving standard string constraint benchmarks involving integer operations. The experiments show that PC* strictly outperforms the standard approach by Verma et al. to extract Parikh images from finite-state automata, as well as the over-approximating method recently described by Janků and Turoňová by a wide margin, and for realistic timeouts (under 60 s) also the nuXmv model checker. When added as the Parikh image backend of Ostrich+ to the Ostrich string constraint solver’s portfolio, it boosts its results on the quantifier-free strings with linear integer algebra track of SMT-COMP 2023 (QF_SLIA) enough to solve the most Unsat instances in that track of all competitors.
@article{paperbot2529,
title = {A Constraint Solving Approach to Parikh Images of Regular Languages},
author = {Amanda Stjerna and Philipp Rümmer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649855}
}