现有的 SAT 并行求解策略主要分为两类：分治法以及基于组合策略的并行。二者通常都会进一步与子句共享（Clause Sharing）结合。近期研究进一步指出，子句共享本身即可视为一种独立的并行化手段，现代分布式求解器正朝着“纯 CDCL 搜索 + 子句共享”的“流线化”（Streamlining）方向演进，相关内容参见 SAT 2025 的工作[SRB25]。需注意，这类结论通常以核数足够多的分布式规模为前提，详见下文“预处理”一节的讨论。

分治法#

由于 DPLL 和 CDCL 算法的核心思想本质上是对（部分）变量赋值空间进行搜索，因此，我们很自然地会考虑将搜索过程本身并行化。 多年来，大多数并行 SAT 求解器都遵循这一范式[HS18]。

这里的分治，本质上是对搜索空间进行划分，将其分割为多个子问题，然后并行求解。根据划分策略的不同，我们可以将方法主要分为 “静态划分” 与 “动态划分” 两类。

静态划分#

Böhme 与 Speckenmeyer 在 1996 年开发了早期并行 SAT 求解器之一[BS96] 。该求解器通过为每个工作节点分配特定的变量赋值子空间以实现并行化，当检测到某节点的预计工作量低于阈值时会触发负载均衡机制。 在特定公式类型（随机 k-SAT 问题与 Tseitin 图实例[Tse83]）的测试中，此求解器在 256 核规模下实现了接近线性的加速比。

Zhang Hantao 等人开发了另一早期并行求解器 PSATO[ZBH+96]，在 PSATO 中首次提出了引导路径（Guiding path）的概念：该路径沿并行 DPLL 过程的决策树记录决策变量轨迹，并追踪路径中尚未反向探索的节点。 工作节点可独立处理不同的引导路径前缀，这本质上等效于为每个节点分配不同的变量赋值子空间。

Heule 等人在 2011 年提出了 Cube&Conquer 这一术语[HKW+11]，用以描述搜索空间划分的一种极端形式：通过前瞻式求解器（March）生成大量名为 "cube" 的部分赋值，并将其分配给所有可用工作节点。 此方法通过精心设计的划分策略、大规模 cube 生成及随机分配机制，在实践中实现了良好的负载均衡。基于 Cube&Conquer 的并行求解器已成功解决了数学领域长期存在的开放性问题，例如勾股三元数问题[HKM16] 和五阶舒尔数问题[Heu18]。 在共享内存的平台上，基于 Lingeling 的 Cube&Conquer 求解器 Treengeling[Bie12]，[Bie14] 曾多次在国际 SAT 竞赛[BDH+14] 中位列并行求解器性能榜首。

动态划分#

部分研究致力于在 Cube&Conquer 与传统划分方法之间寻求平衡，例如 Audemard 等允许 Cube&Conquer 求解器根据当前子问题的难度，动态划分cube[ALS+16]。 分布式的 Cube&Conquer 求解器包括 Audemard 等提出的 Dolius[AHJ+14] 以及 Heisinger 等 近期推出的 Paracooba[HFB20]。

负载均衡#

并行算法中最重要的部分莫过于负载均衡， 在早期的 PSTAO[ZBH+96] 中，其使用抢占式调度来达到负载均衡的效果。

在现代的 SAT 并行求解中，我们通常采用动态负载均衡策略，例如 Chrabakh 与 Wolski 提出 “当子问题求解时间超过阈值时进行递归分割”[CW03]；Blochinger 等人则通过 随机工作窃取策略（Randomlized Work Stealing）[San94],[BL99] 实现负载均衡[BSK03]。

子句共享#

Sinz 等人提出基于引导路径的求解器 PaSAT[SBK01] 首次将子句共享（Clause Sharing）引入并行 SAT 求解。 其核心思想是：当某个求解器发现冲突子句时，可将其共享给其他求解器以减少冗余计算。 然而，在分治法中，由于存在着假设（assumption）的限制，共享的学习子句要么质量较差，要么数量太少，这两种情况都导致了无法有效的加速求解过程。

缺陷#

基于搜索空间的划分方法的主要缺陷在于，划分所采用的启发式策略对整体性能具有决定性影响，且需针对具体应用场景进行精细调优[HKM16]。 不当的划分选择可能无法均衡的分配计算负载，反而会生成两个与原始问题同等复杂的子问题——这一现象被 Schulz 与 Blochinger 称为“伪分割”[SB10]。 另一种潜在问题是，部分分割后的问题可能变得异常简单，这称为 “倾斜分割”[SB10]。 若此类分割反复发生，将引发“乒乓现象”，导致系统在通信与等待上消耗的时间远超实际求解时间[JLU01]。

基于组合策略的并行#

Balyo 与 Sinz 在书中提到[HS18]，基于搜索空间的划分求解器的性能已趋于被基于组合策略（Portfolio）所超越。

这种基于组合策略的 SAT 求解方法被称为（纯）组合式方法[GS01]：通过并行执行多个具有充分差异性的求解器，使其针对同一问题展开"竞争"。 这种简单并行化策略的乐观解读认为它模拟了虚拟最佳求解器（简称 VBS）[XHH+12]。而悲观（或可能更现实）的解读则认为，纯组合式方法虽对多数问题有效，但效率欠佳，因为无论求解器总数多少，最终仅有一个求解器对解决方案作出贡献。

组合方法的核心在于求解器的多样化配置（diversification）。多样化是指促使组合中各参与者产生不同行为、进而探索搜索空间不同区域的各种机制，此方法中较为典型的求解器为 Hamadi 等人提出的 ManySAT[HJS10] 以及 Balyo 等人提出的 HordeSAT[BSS15]。常见的多样化设置如下：

• 为求解器设置不同随机种子，使求解器在随机决策时选择不同分支路径[BSS15]。
• 设定不同的初始变量相位，引导求解器以不同方式探索搜索空间[HJS10]。
• 采用不同求解器参数，重启间隔[HJS10]、预处理与过程中处理选项[Bie10] 或子句库管理策略[AS17]。
• 使用异构 SAT 求解器，采用完全不同的 SAT 求解算法与实现通常能显著提升组合成员的搜索行为多样性[XHH+12]。

值得注意的是，在组合式的并行方法中，不存在负载均衡的概念，这是因为当一个求解器运行完成后，原问题也随之解决，因此不需要做负载均衡。

子句共享#

正如先前所说，学习子句的共享能够对搜索空间进行剪枝，减少冗余计算，提高求解器性能。 然而区别于分治法中子句共享的困难，在当前的范式中，因为每一个工作节点（求解器）求解的都是原问题，于是不存在子问题的概念，那么子句共享就变得容易做到了。

在通用并行 SAT 求解领域，基于子句共享的组合式求解器在竞赛中往往展现出最优性能[BBI+16],[BHJ17],[FHI+21],[BHI+22],[BHI+23],[HIJ+24],[CFH+25]。 从直观角度分析，每个被共享的子句都具备对搜索空间剪枝的潜力，通过互相交流具有前景的剪枝机会，求解器之间能够有效减少冗余计算并实现显著加速[HJS10],[BSS15]。 可以说子句共享是Portfolio 中除多样性外最为重要的部分。

值得强调的是，Schreiber 与 Sanders[SS24] 近期的研究进一步表明，即便所有求解线程完全一致（连随机种子都相同），仅凭子句共享也能取得可观加速——原因是分布式程序的非确定性会使各线程在不同时刻导入略有差异的子句集合，这本身就足以构成有效的搜索空间剪枝。因此他们主张以“子句共享求解器”（Clause-Sharing Solver）一词来描述现代求解器，以强调子句共享是一种独立的并行化手段，而非组合式或分治式方法的附属。在这一视角下，组合式方法中繁复的多样化配置不再是不可或缺的：SAT 2025 的工作[SRB25] 将多样化精简至仅剩随机种子与变量相位两种轻量手段（其中变量相位影响甚微），仍能保持良好的竞争力。

然而需要指出的是，子句共享机制也会带来计算、同步和通信方面的额外开销。考虑到冲突子句生成数量与求解器数量呈线性关系（不计重复项），并行求解器必须建立子句共享的优先级策略[HJS10],[AHJ+12],[ENS14]。

学习子句质量的评估#

目前最常采用的评估指标包括 子句长度 与 文字块距离（简称 LBD）[AS09]。 基于子句长度的共享优先级策略可追溯至 PaSAT 求解器[SBK01]；在首个基于组合式求解器 ManySAT[HJS10] 中，设定了共享子句长度阈值为 8。与子句长度不同，LBD 是与子句衍生时特定求解器状态相关的动态度量，并可能在后续搜索过程中持续更新。

除上述质量评估指标外，Audemard 等人[AHJ+12] 提出通过子句与求解器当前变量相位的匹配度进行评估，Vallade 等人[VLB+20] 则基于公式的社区结构设计了新型子句度量标准。

由于生成子句的质量分布会随时间推移和输入差异动态变化，采用固定质量阈值[HJS10],[Bie10] 可能导致共享子句数量过多或不足。为此，研究者提出了自适应质量限制机制。例如，Hamadi 等人开发了自适应控制方案[HJS12]，使求解器对之间的子句共享阈值随时间动态调整；而 HordeSat 求解器[BSS15] 则使用了动态 LBD 策略，即初始为每个求解器设置了极为严格的 LBD 阈值，随后在共享的过程中动态调整此阈值。

然而，将 LBD 作为共享子句的选取指标，其有效性近年来正受到越来越多的质疑。与子句长度不同，一个子句的 LBD 与其导出时特定求解器的状态相关，对其他求解线程未必具有可迁移的意义[AS14]；换言之，某一子句所携带的具体 LBD 值在跨求解器共享时可能并不传递有用信息。Iida 等人[ISI24] 转而提出基于公式（静态）图结构的共享子句选取度量，以替代依赖求解器状态的 LBD；Schreiber 与 Sanders[SS24] 也报告称，MallobSat 仅将 LBD 作为子句长度之后的次要排序依据，且各种 LBD 处理方式对性能影响甚微。

Schreiber 等人在 SAT 2025 上给出了更为彻底的结论[SRB25]：将已聚合的待共享子句的 LBD 值在同一子句长度内随机打乱后，求解性能没有可察觉的差异（仅多解出 1 个实例，加速比 1.27%）；进一步地，完全移除子句共享中的 LBD 信息（为每个传入子句赋予等于其长度的最大 LBD 值）同样能保持性能。这些证据共同表明，LBD 对现代子句共享求解器而言并非有用信息。

Portfolio 求解器发展脉络#

Portfolio 求解器的发展可以看作是学习子句共享策略的发展过程。

Hamadi 等人[HJS10] 通过 ManySAT 求解器首次提出并行组合式 SAT 求解方法。ManySAT 确立了两项被后续多数组合式求解器采纳的核心要素：1. 单个求解器的多样化配置；2. 跨求解器的子句共享机制。 尽管 ManySAT 仅针对四核架构进行优化，但它标志着并行 SAT 求解领域的范式转变。自 2010 年起，以 Plingeling[Bie10]、SArTagnan[KK11] 和 PeneLoPe[AHJ+12] 为代表的组合式求解器开始主导各类竞赛[HS18]。 值得关注的极端案例是 ppfolio[Rou12]——该脚本仅通过并行运行往届竞赛优胜求解器实现求解。

多年来，Plingeling 始终被视为性能最优的并行 SAT 求解器[HS18]。该求解器通过配置串行求解器 Lingeling[Bie10] 及后续版本中的局部搜索求解器 YalSAT[Bie14] 实现并行求解，其 Lingeling 实例在重启调度策略、内部处理选项和初始变量相位等方面均采用多样化配置。 新版 Plingeling 支持共享长度不超过 40 且 LBD 值不超过 8 的学习子句[Bie12]。

Audemard 与 Simon 基于串行求解器 Glucose 开发了组合式求解器 Syrup[AS14] ，引入两大关键技术：1. 子句懒交换机制，仅当某个学习子句在本地被两次触发后才考虑共享；2. 子句观察期制度，为每个导入的学习子句仅设置一个观察字，仅当该文字被赋值为假时，该子句才升级为正常处理状态。这些技术显著降低了子句交换量[AS14]，并被后续求解器部分采纳[ALS+16],[EN19]。

Ehlers 等人通过 TopoSAT 求解器[ENS14] 探索了大规模并行 SAT 求解技术，TopoSAT 可协调多个改进版 Glucose 求解器。求解器线程在距离上次共享超过特定时间间隔或内部导出缓冲区满载时，会主动导出子句。 TopoSAT 还可采用惰性子句交换策略，仅当至少四个进程本地求解器判定某子句具有价值时才进行导出[EN19]。子句交换通过点对点消息传递在通信图谱中实现[ENS14]。在导入环节，每个输入子句被赋予等同于其长度的 LBD 值作为保守上界。在 2020 年竞赛中的 TopoSAT 2[FHI+21] 要求每个求解器进程将每批子句发送至所有其他求解器进程，这种设计会导致消息量呈平方级增长。

Balyo 等人通过 HordeSat [BSS15] 提出了子句共享组合式求解器的通用框架。其模块化求解器接口可在不改变内部机制的前提下协调不同 SAT 求解器。 每个进程运行多个求解器线程，跨进程通信由专用线程处理，求解器无需保持同步。HordeSat 通过名为“全收集”（all-gather）的操作周期性地执行全互连子句交换：各进程将其最优本地子句写入固定大小缓冲区，所有缓冲区拼接后统一分发至各进程。初始阶段仅允许 LBD 值不超过 2 的子句参与导出，当进程无法提供预期数量的子句时，此限制将逐步放宽。该系统采用 Bloom 过滤器对已接收子句进行近似去重。 Balyo 等人在 2048 个核心上对 HordeSat 进行评估[BSS15]，在 ISC 应用基准测试中，HordeSat 在 1024 核心上实现中位数加速比 13.8（2048 核心为 13.1）。

受到 HordeSat 的部分启发，Ludovic Le Frioux 等人提出了一个提供了更为模块化的架构 PaInLeSS[LBS+17] ，旨在"无痛"式开发和探索并行 SAT 求解器。PaInLeSS 继承了 HordeSat 的诸多特性，包括子句交换、组合策略与搜索空间划分，同时支持自定义新策略，实验表明，通过 PaInLeSS 实现的求解器与部分最先进的求解器，如 HordeSAT[BSS15] 相比性能有较高的提升。使用 PaInLeSS 框架的并行求解器在近年竞赛中表现卓越[VLO+21],[FHI+21]，在 SAT 2025 年国际竞赛中，基于 PaInLeSS 的并行求解器 PL-PRS-Kissat[CFH+25]（ PL-PRS-BVA-Kissat[SLB+nd] 的改进版本）获得了并行赛道 SAT 实例的第一。

2022 年表现优异的共享内存求解器 Xindi Zhang 等人提出的 ParkissatRS[BHI+22] 同样基于 PaInLeSS 框架构建，但采用 Kissat 求解器变体作为后端，该系统通过随机重排决策变量的分支顺序实现多样化。其后继求解器 PRS[CZQ+23] 进一步强化了多样化机制，并创新性地采用分布式架构，通过单向环形通信实现跨进程子句共享。

Fleury 与 Biere[FB22] 在 2022 年提出的 Gimsatul 展现出与主流组合式求解器截然不同的架构设计。该求解器在不同求解线程间实现物理层面的真实子句共享，而非简单复制，因此选择从头编写而非复用现有求解器。该架构使内存占用量显著降低，并在 16 核范围内实现近似线性的自加速比。

Schreiber 与 Sanders 提出了 MallobSat[Sch24],[SS24]，通过对求解器 HordeSat 进行系统性重构，重点优化其算法构建模块来提升子句共享的性能，实现了对学习子句的精细缓冲与过滤，并有效协调了最先进的求解器后端。

具体而言，HordeSat 中会导致：1. 导出缓冲区未充分利用，且限定容量，导致可能无法保存最近产生的学习子句；2. 单元学习子句重复，且 Bloom 过滤假阳性问题。在 MallobSAT 中，1. 通过二叉树通信来聚合缓冲区，以达到去重与排序的目的；2. 设置全局预算，而不是为导出缓冲区设置容量，预算不足时选择最差的学习子句丢弃。

通过上述改进后的共享策略，在通用的样例上，MallobSAT 显著优于升级版 HordeSat，平均加速比提升两倍。并且，在 2020-2025 年连续多届国际 SAT 竞赛中，MallobSAT 均取得优异排名，并成功解决了多个往届未破解的竞赛难题[FHI+21],[BFH+20],[BHI+22],[BHI+23],[HIJ+24],[CFH+25]。

在 PaInLeSS 的分布式版本 D-PaInLeSS 中[SBS+25]，Mazigh Saoudi 等人加入了 MallobSAT[SS24] 中的子句共享策略，将并行与分布式 SAT 求解器的性能再次进行提高，但可能由于多样化程度不足或子句共享机制未达最优的问题，D-PaInLeSS 在 UNSAT 实例上的表现依然不如 MallobSAT。

最新进展来自 SAT 2025：Schreiber、Rigi-Luperti 与 Biere 对 MallobSat 进行了“流线化”（Streamlining）重构[SRB25]，主张现代分布式求解器盲目沿用了大量面向串行求解的最佳实践，而这些实践在分布式场景下可能收益甚微甚至有害。其核心改动有三：其一，关闭所有线程上冗余执行的预处理与过程中处理，改由单个线程串行执行一遍关键简化技术，并与并行的“纯搜索”任务协同运行；其二，从子句共享中移除 LBD 信息；其三，将多样化精简为随机种子与变量相位两种轻量手段。重构后的求解线程退化为一支“均匀”的 CDCL 搜索阵列，几乎不再具备组合式求解器的特征。在最高 3072 核（64 节点）上的实验表明，该设计在所有规模下均取得了最低的 PAR-2 分数，并在面向应用的基准上表现突出；不过，由于省去了专用的局部搜索线程与针对特定问题的特殊技术（如 Lingeling 的基数约束推理），它在部分由这些技术迅速求解的实例上仍不及混合式配置。

预处理#

在前文提到的 PRS[CZQ+23] 框架中以及 PL-PRS-Kissat[CFH+25] 中都采用了预处理的方式来加速求解。使用的技术包括：1. 等价文字替换（ELS）： 只在子句数量超过 150,000,000 时打开；2. 归结检查（Resolution Check）：对含有 的所有子句做归结；3. Fourier-Motzkin Elimination 处理基数约束；4. 高斯消元处理 XOR 门

而在 PL-PRS-Kissat 中，还通过遗传算法 GASPI[SBD24] 生成了初始解，用于构造一半求解器的初始解，另一半求解器的初始相位。

然而，Schreiber 等人在 SAT 2025 上对分布式求解中的预处理提出了新的审视[SRB25]。他们的运行时间剖析显示：预处理与过程中处理被所有求解线程冗余执行，且本身无法并行化，随着求解核心数增加，其占总工作量的比例显著上升（例如初始快速变量消除的时间占比从单核的 0.3% 升至 768 核的 2.96%），逐渐成为可扩展性瓶颈——在 768 核下直接关闭预/过程中处理，反而取得了 3.7% 的几何平均加速并多解出 12 个实例。此外，各线程之间不一致的预处理级别还会造成“语言障碍”：当某线程已消除某些变量后，其他线程传来的、含有这些变量的子句便无法被导入，实验中约 22% 的线程成功导入的传入子句不足一半。

据此，作者提出一种更可扩展的替代方案：不再让每个线程各自预处理，而是仅用单个线程串行地执行一遍关键简化技术，将预处理后的公式作为一个独立任务，与“纯 CDCL 搜索”任务并行运行，并随着时间推移逐步把计算资源从原始任务转移到预处理任务上。这一思路与早期 Plingeling 的“先预处理、再分叉”（preprocess-then-fork）模式一脉相承，也类似于 PRS / PL-PRS-BVA-KISSAT 中协调式预处理的做法；其区别在于预处理尚未完成时，全部并行资源就已被投入到搜索任务之中。

需要强调的是，上述结论以并行规模足够大为前提，并非在所有核数下都成立。论文的 Figure 2（右）对比了“仅搜索”与默认（带预处理）配置在 1 核与 768 核下的表现：在单核时，带预处理的 Kissat 明显优于“仅搜索”版本；只有当规模提升到 768 核的分布式场景时，“仅搜索”才在整体时间上以微弱优势反超（多解出 12 个实例，几何平均加速 3.7%）。也就是说，两者之间存在一个交叉点——在核心数较少时，预处理与过程中处理依然有效（甚至不可或缺），只有当核数持续增多、使冗余预处理的机会成本超过其收益之后，关闭预处理才会转为更优选择。因此“流线化”设计的收益应结合实际的核数规模来判断，而不宜无条件地关闭预处理。

混合求解#

如前所述，划分与组合策略是 SAT 求解并行化的两大主流研究方向。组合式方案实现简单，其通过多样化原则提升问题求解概率。然而由于工作节点可能搜索重叠区域，其理论加速效果不及分治法[HJN11]。 值得关注的是，尽管分治式方法具备更优的理论加速比，却面临三大挑战：搜索空间划分，工作节点间的负载均衡以及子句共享。 新兴的混合式技术尝试同时运用两种策略，旨在兼收各自优势而规避其缺陷。

混合实现存在两种基础路径：其一是分治式组合法（由 c-sat[OU09] 率先提出），其二是组合式分治法（如 ampharos[ALS+16] 采用的适应性分治策略，允许在搜索空间同一子区域部署多个工作节点）。 此外还存在更复杂的混合方法，包括散射法[HJN06],[HM12] 以及基于转移启发式的策略[ALS+16],[Blo05],[MML10],[SB10]。

基于 GPU 的并行#

基于 CDCL 的 SAT 求解器无法有效地从 CPU 领域迁移到 GPU 领域，其主要困难在于：1. 内存大小不足，GPU 内每个线程可用的内存和缓存远小于 CPU；2. 线程发散问题，当同一“warp”中的线程没有遵循相同的决策路径时，会导致该 warp 中的所有其他线程停滞。为了解决这些问题，研究者提出了多种利用 GPU 加速 SAT 求解的方法：1. 使用 GPU 执行单元传播[DDF+15]；2. 使用 GPU 进行预处理[OW19],[OWB21]；3. 同时使用 GPU 执行 Tabu 搜索算法，而 CPU 执行多线程 CDCL 算法[BDD+12]；4. 将 GPU 视为学习子句的通讯节点，快速计算哪些学习子句需要被共享，并通知对应的工作节点[PSM21]。

然而，目前这些方法都没有被广泛采用。

基于连续搜索的 SAT 求解器#

Anastasios Kyrillidis 等人在 2020 年提出了一种新型 SAT 求解的范式 FourierSAT[KSV+20]，通过傅里叶展开，将 CNF 等约束变化为连续的布尔函数，使用梯度下降的优化方法求解 SAT 问题。 在此方法的改进版本 GradSAT[KVZ21] 基础上，Yunuo Cen 等人又提出了在 GPU 上并行求解器 FastFourierSAT[CZF25]。 通过在 GPU 上计算初等对称多项式，相比之前在 CPU 的性能得到提升显著。与最先进的并行 SAT 求解器在多个基准测试上进行比较，结果表明 FastFourierSAT 在特定类型问题上具有竞争优势。

References#