🤖 AI

Learning Splitting Heuristics for Parallel String Solvers

本文提出了一种数据驱动的方法，用于自动学习并行字符串求解器的拆分启发式算法，并证明了在 Z3seq 和 Z3str4 中实现这些学习到的启发式算法时，其在求解公式数量和平均求解时间方面均显著优于人工设计的启发式算法。

原作者： Chenhao Gao, Peisen Yao

发布于 2026-06-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Chenhao Gao, Peisen Yao

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在试图解决一个巨大且极其复杂的拼图。这个拼图代表了一个计算机程序的逻辑，特别是处理文本（如密码、用户名或文件路径）的逻辑。你的目标是弄清楚是否有一种方法可以将这些碎片完美地组合在一起（即“可满足”解），或者这个拼图是否已经损坏，无法完成（即“不可满足”解）。

这就是 字符串求解器 (String Solver) 的工作。然而，这些拼图往往如此庞大且复杂，以至于让单个人（或单个计算机核心）逐一尝试解决会耗费太长时间。

问题：选择太多，速度太慢

为了更快地解决这些拼图，计算机使用了一种称为 “分而治之” (Divide and Conquer) 的策略。它们不尝试一次性解决整个拼图，而是将大拼图拆分为两个较小的堆。然后，它们将这些堆发送给不同的工作者（计算机核心）同时进行解决。

关键问题在于：你如何决定在哪里切开这个拼图？

如果你在错误的地方切开，你可能会得到两个依然需要耗费大量时间才能解决的巨大且困难的堆。
如果你在正确的地方切开，你可能会瞬间解决其中一半，或者让剩下的另一半变得非常容易。

目前，计算机使用 人工设计的规则 (Heuristics) 来决定在哪里切开。你可以把这些规则想象成一位从未品尝过你厨房里特定食材的厨师所写的食谱。厨师可能会说：“总是先切红色的碎片”，但有时红色碎片才是最难处理的部分。这些人工规则通常是次优的，并且需要大量的人力去不断调整。

解决方案：Owl（学习型厨师）

本文的作者引入了一个名为 Owl 的新工具。Owl 不再依赖静态的食谱，而是一个 数据驱动的学习器。它观察计算机解决数千个拼图的过程，从错误中学习，并找出针对 每一个特定实例 最好的切割方式。

以下是 Owl 的工作原理，使用一个简单的类比：

1. 旧方法：“味觉测试”（成对分类法）

以往尝试自动化的方法使用的是一种类似于盲测的方法。为了在两个碎片（碎片 A 和碎片 B）之间做出选择，计算机会询问：“如果我选 A，它是否比 B 更好？”它会对每一对可能的组合都进行这样的比较。

缺陷： 这种方法很慢且容易出错。如果计算机在早期犯了一个小错误（认为 A 比 B 好），这个错误就会不断累积，导致最终的选择非常糟糕。这就像是通过仅进行两两比较来对 100 首歌进行排名；一次错误的比较就会毁掉整个列表。

2. Owl 的方法：“时光机”（回归分析）

Owl 采取了一种更聪明的方法。它不再问“A 是否比 B 更好？”，而是问：“如果我选择 A，解决这个拼图需要多长时间？” 以及 “如果我选择 B，需要多长时间？”

类比： 想象你是一名项目经理。与其询问你的团队“任务 A 是否比任务 B 更好？”，不如询问你的 AI 助手：“如果我们做任务 A，项目需要多少小时？如果我们做任务 B，需要多少小时？”
优势： AI 会给出一个具体的数字（例如：“任务 A 需要 2 小时，任务 B 需要 10 小时”）。这保留了完整的图景。你不仅知道 A “更好”，你还知道它“好得多”。这避免了旧方法中出现的连锁错误。

3. 特征：阅读水晶球

为了做出这些预测，Owl 会观察两类线索（特征）：

静态特征： 这些就像是观察拼图盒的封面。它们告诉 Owl 碎片的形状、有多少个红色碎片以及图像的总体复杂度。
动态特征： 这些就像是实时观察拼图的组装过程。Owl 会检查：“这个碎片以前是否引起过冲突？它是否似乎能快速解锁其他碎片？”

通过结合这些线索，Owl 构建了一个模型，用于预测任何潜在切割的“求解时间”。然后，它会选择那个承诺最短时间的切割方案。

结果：更快、更聪明

作者在两个世界顶尖的拼图求解器（Z3seq 和 Z3str4）上测试了 Owl。他们发现：

解决的拼图更多： 在有 Owl 帮助的情况下，计算机在耗尽时间之前解决了显著更多的拼图。例如，在使用 4 个工作者时，Z3seq 比其独立运行时多解决了 46 个拼图。
速度更快： 解决拼图的平均时间降低了约 44% 到 59%。
可扩展性： 随着增加的工作者（计算机核心）数量，Owl 的表现越来越好，这证明了它能够有效地管理团队。

总结

简而言之，本文用一个 智能的学习系统 取代了用于拆分复杂文本问题的“猜测与检查”式人工规则。它不再问“哪一个更好？”，而是问“这需要多久？”，并利用这个精确的答案来做出最佳决策。这把一个缓慢、易错的过程变成了一个快速、高效的过程，使计算机能够更有效地解决复杂的字符串问题。

技术摘要：学习用于并行字符串求解器的分裂启发式算法

问题陈述

字符串约束求解器对于验证涉及字符串操作的程序（如安全策略强制执行和符号执行领域）至关重要。然而，许多实际的字符串约束是不可判定的，且现有的求解器在处理可扩展性和复杂的现实世界实例时往往表现不佳。虽然多核架构提供了利用并行求解的机会，但分而治之策略（特别是立方与征服/cube-and-conquer）的有效性高度依赖于高质量的分裂启发式算法（splitting heuristics）。这些启发式算法决定了应该对哪个原子（约束）进行分支，从而将搜索空间划分为子问题。

目前的分裂启发式算法通常是手动设计的且是静态的。它们往往无法适应特定约束实例的具体结构特征。此外，现有应用于 SAT 领域的自动化方法（如成对分类法）在应用于 SMT 字符串求解时存在显著局限性：

定量信息丢失： 将求解时间简化为二元标签会丢弃细粒度的成本数据。
级联误差： 成对分类中的串行比较会导致误差累积，从而降低预测质量。
可扩展性： 成对方法需要对候选对进行线性（或更糟）的扫描，这在计算上是非常昂贵的。
领域适用性： 先前的自动化方法主要在 SAT 领域得到验证，在 SMT 理论（如字符串）中的适用性尚未得到证实。

方法论

作者引入了 Owl，这是一个数据驱动的框架，用于为并行字符串求解器自动生成分裂启发式算法。其核心创新在于将原子选择问题从一个分类任务重新定义为一个回归任务。

1. 将问题建模为回归

不同于通过比较两个原子来确定哪一个“更好”（分类），Owl 预测的是基于特定原子 $p$ 进行分裂后所产生的子问题所需的连续求解时间（ $Time(\varphi, p)$ ）。

成本定义： 目标变量是根据两个分支（ $\varphi \land p$ 和 $\varphi \land \neg p$ ）的并行执行结果定义的。例如，如果两个分支都满足（satisfiable），则成本是两者求解时间的最小值；如果两个分支都不可满足（unsatisfiable），则成本是两者的最大值。
优势： 这种方法保留了性能指标的连续性，避免了分类带来的离散化误差，并消除了对详尽成对比较的需求，从而降低了推理开销。

2. 特征工程

为了支持回归模型，作者为每个候选原子设计了一套包含 77 个特征 的综合特征集，分为两类：

静态特征（66 个特征）： 在不执行求解器的情况下，从公式结构中提取。包括算子分布（例如 str.increment、re.union 的计数）、子句大小以及图属性（例如变量-子句度数）。
动态特征（11 个特征）： 通过求解器执行过程中的短期**前瞻（lookahead）和回顾（lookback）**启发式算法获取。
- 回顾（Lookback）： 追踪历史求解器状态，例如一个原子出现在冲突子句或学习引理中的次数。
- 前瞻（Lookahead）： 模拟有限的约束传播（通常限制在约 600 个冲突以内），以观察即时后果，例如新增赋值的数量或学习到的子句数量。

3. 模型选择与训练

算法： 系统采用**随机森林回归（Random Forest Regression）**作为核心预测模型。这一选择平衡了预测精度与推理速度，并对噪声标签（求解时间的波动）具有鲁棒性。
训练数据： 通过在多样化的基准公式上运行求解器，对各种原子进行分裂，并记录由此产生的求解时间和特征向量，从而构建数据集。
部署： 训练好的模型被集成到求解器（Z3seq 和 Z3str4）中。在每个决策点，求解器为候选原子构建特征矩阵，通过进程间通信（IPC）将其发送给并行工作进程，并接收预测出的具有最低估计求解时间的原子。

核心贡献

新颖的建模方式： 本文提出将并行字符串求解的分裂启发式算法设计从成对分类问题重新构建为回归问题。
实用的学习框架： 引入了一个利用丰富的 77 个专用实例特征（静态和动态）自动生成启发式算法的框架。
实现与评估： 该方法已在两个最先进的字符串求解器 Z3seq 和 Z3str4 上实现并进行了评估，证明了其相对于手动设计启发式算法的显著性能提升。

实验结果

作者在 1,024 个来自 SMT-LIB 仓库的 QF_SLIA 公式上，使用 4、8、16 和 32 个线程对 Owl 进行了评估。

求解能力： 在 4 个线程下，Z3seq(Owl) 比基准模型多解决了 46 个公式（提升 4.8%），Z3str4(Owl) 多解决了 9 个公式。这些改进在所有线程配置下均得到了保持。
运行时性能：
- Z3seq(Owl) 在 32 线程下实现了平均 1.44× 的加速。
- Z3str4(Owl) 在 32 线程下实现了平均 1.59× 的加速。
预测准确度： 回归模型的表现显著优于默认的前瞻启发式算法和成对分类基准。对于 Z3seq，该模型在近 45% 的情况下正确识别了前 20% 的原子，而基准模型的表现接近随机。
开销： 特征提取和模型推理的计算开销极小，仅占总求解时间的 23.6%，这与默认前瞻启发式算法的开销相当甚至更低。
特征重要性： 分析显示，虽然特定特征的排名在不同求解器之间有所不同（表明需要针对特定求解器进行优化），但关键特征如“赋值数量”、“前瞻得分”以及特定的字符串操作计数始终保持重要性。

意义与主张

本文声称 Owl 通过自动化设计分裂启发式算法，为并行字符串约束求解提供了显著的进步。通过从手动、静态的启发式算法转向数据驱动的回归模型，该方法有效地适应了复杂字符串约束的具体特征。

作者强调，其方法：

优于现有的手工设计启发式算法，在解决实例数量和平均求解时间方面均表现出色。
缓解了 成对分类方法中固有的误差累积和信息丢失问题。
证明了 学习到的启发式算法可以高效地集成到现有的 CDCL( $T$ )-based 求解器（Z3seq 和 Z3str4）中，以释放并行架构的潜力。

研究结论指出，尽管顺序求解器的效率限制了整体加速比，但学习到的启发式算法通过创建平衡的子问题，有效地实现了最大化并行性，从而带来了实质性的实际改进。