论文标题
具有常规限制的协同作用中的单词方程式（技术报告）
Word Equations in Synergy with Regular Constraints (Technical Report)
论文作者
论文摘要
吃意大利面时，应该将酱汁和面条混合在一起，而不是分开吃。我们认为，在字符串求解中，与大多数当前字符串求解器中的单独使用相比，单词方程式和常规约束更好地混合在一起。我们提出了一种快速算法，该算法是针对无链约束的片段完成的，其中单词方程式和常规约束紧密整合并交换信息，有效地彼此产生的案例并限制了可能的组合爆炸。该算法基于基于新颖的语言对单词方程式具有常规约束的满意度的表征。我们在实验上表明，我们的原型实现与最佳的弦求解器具有竞争力，甚至优越，因为它是困难示例中最快的，并且超时数量最少。
When eating spaghetti, one should have the sauce and noodles mixed instead of eating them separately. We argue that also in string solving, word equations and regular constraints are better mixed together than approached separately as in most current string solvers. We propose a fast algorithm, complete for the fragment of chain-free constraints, in which word equations and regular constraints are tightly integrated and exchange information, efficiently pruning the cases generated by each other and limiting possible combinatorial explosion. The algorithm is based on a novel language-based characterisation of satisfiability of word equations with regular constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior in that it is the fastest on difficult examples and has the least number of timeouts.
