解决正则表达式填字游戏的有效方法

《Science of Computer Programming》：Effective methods for solving regex crossword puzzles

　　李荣晨|苏伟豪|黄洪|陈海明|陈子轩

摘要
正则表达式在多种场景中被广泛使用。但目前，正则表达式的建模通常仅基于语言理论层面的定义，许多扩展运算符被忽略。相关工具缺乏对这类扩展运算符的全面建模，限制了它们的应用范围和实用性。为解决这一问题，我们对正则表达式的运算符进行了全面建模，并将该建模方法应用于正则填字游戏求解。首先，为应对正则表达式全面建模的挑战，我们根据其语义提出了一种过近似建模方法，同时采用反例引导的抽象精化策略来强化约束，从而消除错误解，确保建模的可靠性。基于该建模方法，我们提出了Rcps这一用于解决正则填字游戏的新算法，此外还提出了基于通信顺序过程模型的并行版本RcpsP。我们从最受欢迎的正则填字游戏网站收集了803个矩形谜题和95个六边形谜题，并将我们的算法与五种最先进的工具进行了比较。实验结果表明，Rcps能够解决97.76%的矩形谜题和98.95%的六边形谜题，分别比最佳基准方法的成功率高出19.06%和65.27%。通过并行化处理，RcpsP的平均速度比Rcps快1.86倍和1.25倍，且矩形谜题的解决率提升至98.13%。相关代码和数据集可在https://github.com/SuperMaxine/rcps-solver.git获取。

引言
作为字符串处理工具，正则表达式在计算机科学和软件开发的诸多领域都有广泛应用，如软件工程[1]–[4]、网络安全[5]–[7]、自然语言处理[8]–[12]、数据库处理[14]–[16]等。由于正则表达式极为常见，其建模技术也被应用于程序分析[4]–[17]、正则拒绝服务攻击检测[18]、正则表达式的合成与修复[19]–[22]、正则表达式测试[23]以及正则填字游戏求解[24]等诸多场景。然而，目前对于许多扩展运算符仍缺乏全面建模——很多扩展运算符往往被忽略（我们稍后会通过示例说明这一点）。这种缺失会导致这些运算符在各种应用中的使用受限，比如测试用例覆盖不全、无法实现ReDoS检测、表达式合成或修复失败、测试不完整以及无法解决某些谜题。此外，还有研究探讨了涉及回溯和反向引用等复杂结构的正则表达式的难度问题，例如[25]中就有学者证明某种约束求解问题是不可判定的。

目前的正则表达式建模通常仅关注语言理论层面的定义，而忽视了那些结构复杂或语义特殊的部分。例如，用于解析HTML文件中img标签的正则表达式r=定义了一种上下文相关的语言，其中在([''']?)1中匹配到的字符串需要在\1中再次匹配。在这个例子中，后顾断言（用于限定匹配内容的(?<=\s)）、捕获组（即括号中的( )1、( )2，详见第2节）、反向引用（即\1对第一个捕获组的引用）以及非贪婪匹配机制（即*?）往往会被忽略，因为这些扩展运算符难以进行精确建模。

为应对这些挑战，我们对正则表达式的运算符进行了全面建模，并以正则填字游戏作为主要研究案例，因为有效解决这类谜题本身就具有较高难度。正则填字游戏是一种极具挑战性的基准测试，它需要运用回溯、反向引用等高级特性，同时也有已公布的解决方案可用于验证建模的正确性。重要的是，这类谜题与程序分析、测试生成以及安全防护领域中的多正则表达式约束求解任务高度相似。我们将在第7节通过一个实际案例进一步说明这种现实意义。传统填字游戏是全球最受欢迎的游戏之一，作为典型的满足性问题，它也受到了约束编程领域的关注[27]–[28]。作为一种新的填字游戏形式，正则填字游戏在多个程序员社区中广受欢迎[29]–[30]，并且还出现在夺旗竞赛[31]以及MIT的谜题寻宝活动中[32]。

正则填字游戏由空白网格和各种约束条件组成。在基本的正则填字游戏中，我们会得到两个非空的正则表达式列表，分别用于标记m×n大小空白网格的m行和n列。这类游戏的任务是在网格中填入字符，使得每行从左到右构成的字符串能与对应的正则表达式匹配，每列从上到下也是如此。详细内容可见第4.1节。例如，图1a展示了一个2×2的基本谜题，它有唯一的解。基本正则填字游戏还有两种变体：一种是矩形正则填字游戏（R-rcps），每行和每列各包含两个正则表达式，字符串需同时满足这两个正则表达式；另一种是六边形正则填字游戏（H-rcps），它由六边形单元格构成，正则表达式在三个不同方向上存在，图1b展示了一个示例。

尽管正则填字游戏很受欢迎，但如何有效解决它们仍然是一个未解决的问题。目前，用于解决这类谜题的先进技术主要基于不同的方法：字符串约束求解法（如Jeong[24]的方法）、启发式算法（如Trux[33]和Shcherban[34]的方法）、回溯算法（如Abolofia[35]和Schaaf[36]的方法）。然而，根据最受欢迎的正则填字游戏网站的实验结果，现有工具中解决矩形谜题的最佳成功率仅为78.70%，而解决六边形谜题的成功率仅为33.68%（详见第5节的表3），这大大限制了它们的实际应用价值。

另一方面，已有研究得出了关于标准正则表达式的正则填字游戏的复杂性结果[37]–[38]，例如，当所有行和列的正则表达式都相同时，这类受限正则填字游戏的复杂性为NP完全问题。而对于同时包含回溯和反向引用的正则填字游戏，目前尚无复杂性研究结果：具有无限大小网格的谜题因其正则表达式的空性问题不可判定，这一结论源于[25]中的研究，不过对于固定大小的网格，其复杂性仍有待进一步研究。这些结果都体现了解决正则填字游戏的难度。

正因如此，我们决定设计一种全面的正则运算符建模方法，并将其应用于正则填字游戏的求解中。此外，如第5节的表1所示，这类扩展运算符在正则填字游戏中被广泛使用——例如，捕获组、反向引用和回溯结构的出现频率分别为40.15%、22.12%和12.62%。Loring等人[4]也对JavaScript中的类似现象进行了研究。

在本文中，我们首先提出了一种全面建模正则运算符的方法，该方法在某些情况下可能会存在过近似问题（比如反向引用）。我们的模型会将正则表达式r转化为一个一阶逻辑公式φ，该公式可作为满足性模理论求解器的约束条件，确保得到的解s满足s∈L(r)，其中L(r)表示正则表达式r对应的语言。我们还采用了反例引导的抽象精化（CEGAR）[39]策略，通过迭代方式优化模型，消除错误解，确保模型的正确性。

在此基础上，我们提出了Rcps及其并行版本RcpsP，这两种算法都是用于解决正则填字游戏的新方法。具体而言，Rcps首先根据谜题的特点初始化变量矩阵，然后基于我们的建模方法生成约束条件，最后使用SMT求解器来求解这些约束。需要注意的是，对于某些扩展运算符，生成的约束可能存在过近似问题，在这种情况下，我们会通过CEGAR策略消除模型可能产生的错误解。为了解决性能瓶颈并提升实用性，我们提出了基于通信顺序过程模型的并行算法RcpsP[40]。该算法的核心思路是独立处理那些易于生成的字符串约束，而不必处理那些计算量较大的完整约束，从而有效减少CPU资源的浪费。为进一步提升并行效率，RcpsP利用CSP实现高效的进程间通信，减少对共享内存和进程锁的依赖。此外，我们还设计了一种并行链表结构，旨在优化并行读写操作，同时避免竞态条件。

实验结果表明，我们的算法相比现有方法具有显著优势。本文的主要贡献如下：
• 我们提出了一种基于正则运算符的语言或语义特征的建模方法，并通过CEGAR策略确保建模的正确性（第3节）。
• 我们提出了Rcps及其并行版本RcpsP，用于解决矩形和六边形正则填字游戏，该方法会根据坐标为网格单元分配长度有限的变量，利用SMT求解器处理字符串约束，并通过CEGAR策略消除错误解（第4节）。
• 我们从最受欢迎的正则填字游戏网站收集了803个矩形谜题和95个六边形谜题，将我们的算法与五种最先进的工具进行了对比。实验结果显示，Rcps能解决97.76%的矩形谜题和98.95%的六边形谜题，分别比最佳基准方法的成功率高出19.06%和65.27%。通过并行优化，RcpsP的平均速度比Rcps快1.86倍和1.25倍，矩形谜题的解决率提升至98.13%（第5节）。

本文是对会议摘要[41]的扩展，补充了更多内容：包括在第3节添加示例、新的并行算法、新的实验结果、更完整的相关工作综述，以及新的讨论与未来工作部分，探讨了如何将这种建模方法应用于软件测试和网络安全等领域，同时也分析了进一步提升并行算法效率的途径。

章节节选

预备知识
设Σ为一个非空的有限符号字母表，所有由Σ构成的字符串集合记为Σ*。设N={0,1,2,…}，N+=N?{0}。|s|表示字符串s的长度。对于字符串s=s0…sn?1（n∈N），当n≥1时，用s[i: j]（0≤i≤j< n）表示s的子串si…sj，否则表示空字符串ε。

正则运算符的建模
在本节中，我们将介绍如何将正则运算符编码为一阶逻辑约束，这也是我们Rcps算法的基础。具体而言，给定一个正则表达式r和一个固定的目标字符串长度k，我们会引入一系列变量V=〈x0,x1,…,xk?1〉，用来表示每个字符的位置。核心函数Φ(r,p,l)会递归地生成约束条件，确保从位置p开始、长度为l的子串与子正则表达式r相匹配。为了确定每个位置的合法长度……

解决正则填字游戏
在本节中，我们将详细介绍解决正则填字游戏的完整流程，这一流程建立在第3节所建立的约束建模基础之上。总体而言，我们的方法遵循以下步骤：（1）初始化一个带有变量标记的网格GMT，每个单元格都被分配一个唯一的变量；（2）针对谜题中的每个正则表达式，选取对应的变量序列；（3）利用Φ函数生成约束条件，并将所有约束合并为一个整体公式Ψ；（4）使用SMT求解器求解Ψ，进而填充网格中的字符……

实验
在本节中，我们通过大量实验评估了Rcps和RcpsP的性能与效率，测试对象为五种最先进的基准工具，同时涵盖了矩形和六边形两种类型的谜题数据集。实验旨在回答以下问题：（1）与现有工具相比，我们的方法在成功率方面表现如何？（2）算法的运行时间是多少，并行化处理又该如何提升性能？

评估指标包括：……

正则运算符的建模
Peasant[54]提出了一种全局约束模型，利用DFA来描述复杂的序列规则，但他们的模型并未考虑扩展特性。Saxena等人[55]首次提出了通过字符串约束来编码捕获组的方案。Li和Ghosh[56]设计了一种字符串约束求解器，它能支持大多数JavaScript字符串操作，也能部分支持ECMAScript正则表达式，但不支持反向引用和回溯功能。Loring等人[17]则实现了对正则表达式编码的部分支持……

其他实际应用
除了正则填字游戏之外，我们所开发的建模技术还可直接应用于其他实际问题。以下列举了一些应用场景。在软件验证和测试方面，我们对正则运算符的建模以及并行CEGAR策略可用于生成指定长度的测试用例，或逐步生成最短的测试用例，这些方法在功能测试、模糊测试以及网页表单验证中尤为有用。未来的工作方向
在实现过程中，还有几个方面可以进一步优化以提高效率。对于并行链表而言，当为ψ更新新约束条件时，所有进程都会从链表头部开始获取锁，这会导致链表前端处于忙碌状态而尾部却闲置，从而浪费大量CPU资源在遍历链表和获取锁上。因此，应当探索更先进的分配机制，比如多头链表或随机位置锁获取方式。

结论
在本文中，我们提出了一种用于正则表达式运算符的过近似建模方法。基于该模型，我们设计了一种算法，能够利用CEGAR方案有效解决两类正则表达式交叉字谜问题。为克服性能瓶颈，我们对Rcps进行了并行化处理，得到了RcpsP算法。我们还将所提出的算法与五种最先进的工具在803个R-rcps问题和95个H-rcps问题上进行了比较。实验结果表明，得益于完善的建模，Rcps能够解决97.76%的R-rcps问题。

CRediT作者贡献说明
李荣晨：写作——审稿与编辑，写作——初稿撰写，可视化，验证，软件开发，项目管理，方法论，数据整理。苏伟豪：写作——审稿与编辑，写作——初稿撰写，方法论，形式化分析。黄洪：写作——审稿与编辑。陈海明：写作——审稿与编辑，监督，资金筹集。陈子轩：验证，软件开发，方法论，形式化分析，概念设计。

利益冲突声明
作者们声明，他们不存在任何可能影响本文研究结果的已知财务利益或个人关系。