并行 SAT 的简单综述

现有的 SAT 并行求解策略主要分为两类：分治法以及基于组合策略的并行。

分治法

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

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

静态划分

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

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

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

动态划分

部分研究致力于在 Cube&Conquer 与传统划分方法之间寻求平衡，例如 Audemard 等允许 Cube&Conquer 求解器根据当前子问题的难度，动态划分cube(Audemard et al. 2016)。 分布式的 Cube&Conquer 求解器包括 Audemard 等提出的 Dolius(Audemard et al. 2014) 以及 Heisinger 等 近期推出的 Paracooba(Heisinger, Fleury, and Biere 2020)。

负载均衡

并行算法中最重要的部分莫过于负载均衡， 在早期的 PSTAO(Zhang et al. 1996) 中，其使用抢占式调度来达到负载均衡的效果。

在现代的 SAT 并行求解中，我们通常采用动态负载均衡策略，例如 Chrabakh 与 Wolski 提出 “当子问题求解时间超过阈值时进行递归分割”(Chrabakh and Wolski 2003)；Blochinger 等人则通过 随机工作窃取策略（Randomlized Work Stealing）(Sanders 1994),(Blumofe and Leiserson 1999) 实现负载均衡(Blochinger, Sinz, and Küchlin 2003)。

子句共享

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

缺陷

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

基于组合策略的并行

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

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

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

• 为求解器设置不同随机种子，使求解器在随机决策时选择不同分支路径(Balyo, Sanders, and Sinz 2015)。
• 设定不同的初始变量相位，引导求解器以不同方式探索搜索空间(Hamadi, Jabbour, and Sais 2010)。
• 采用不同求解器参数，重启间隔(Hamadi, Jabbour, and Sais 2010)、预处理与过程中处理选项(Biere 2010) 或子句库管理策略(Audemard and Simon 2017)。
• 使用异构 SAT 求解器，采用完全不同的 SAT 求解算法与实现通常能显著提升组合成员的搜索行为多样性(Xu et al. 2012)。

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

子句共享

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

在通用并行 SAT 求解领域，基于子句共享的组合式求解器在竞赛中往往展现出最优性能(Balyo et al. 2016),(Tomás Balyo, Heule, and Jarvisalo 2017),(Froleyks et al. 2021),(Tomás Balyo et al. 2022),(Tomas Balyo et al. 2023),(M. J. Heule et al. 2024),(Codel et al. 2025)。 从直观角度分析，每个被共享的子句都具备对搜索空间剪枝的潜力，通过互相交流具有前景的剪枝机会，求解器之间能够有效减少冗余计算并实现显著加速(Hamadi, Jabbour, and Sais 2010),(Tomáš Balyo, Sanders, and Sinz 2015)。 可以说子句共享是Portfolio 中除多样性外最为重要的部分。

然而需要指出的是，子句共享机制也会带来计算、同步和通信方面的额外开销。考虑到冲突子句生成数量与求解器数量呈线性关系（不计重复项），并行求解器必须建立子句共享的优先级策略(Hamadi, Jabbour, and Sais 2010),(Audemard et al. 2012),(Ehlers, Nowotka, and Sieweck 2014)。

学习子句质量的评估

目前最常采用的评估指标包括 子句长度 与 文字块距离（简称 LBD）(Audemard and Simon 2009)。 基于子句长度的共享优先级策略可追溯至 PaSAT 求解器(Sinz, Blochinger, and Küchlin 2001)；在首个基于组合式求解器 ManySAT(Hamadi, Jabbour, and Sais 2010) 中，设定了共享子句长度阈值为 8。与子句长度不同，LBD 是与子句衍生时特定求解器状态相关的动态度量，并可能在后续搜索过程中持续更新。

除上述质量评估指标外，Audemard 等人(Audemard et al. 2012) 提出通过子句与求解器当前变量相位的匹配度进行评估，Vallade 等人(Vallade et al. 2020) 则基于公式的社区结构设计了新型子句度量标准。

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

Portfolio 求解器发展脉络

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

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

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

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

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

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

受到 HordeSat 的部分启发，Ludovic Le Frioux 等人提出了一个提供了更为模块化的架构 PaInLeSS(Le Frioux et al. 2017) ，旨在”无痛”式开发和探索并行 SAT 求解器。PaInLeSS 继承了 HordeSat 的诸多特性，包括子句交换、组合策略与搜索空间划分，同时支持自定义新策略，实验表明，通过 PaInLeSS 实现的求解器与部分最先进的求解器，如 HordeSAT(Tomáš Balyo, Sanders, and Sinz 2015) 相比性能有较高的提升。使用 PaInLeSS 框架的并行求解器在近年竞赛中表现卓越(Vallade et al. 2021),(Froleyks et al. 2021)，在 SAT 2025 年国际竞赛中，基于 PaInLeSS 的并行求解器 PL-PRS-Kissat(Codel et al. 2025)（ PL-PRS-BVA-Kissat(Saoudi et al., n.d.) 的改进版本）获得了并行赛道 SAT 实例的第一。

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

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

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

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

通过上述改进后的共享策略，在通用的样例上，MallobSAT 显著优于升级版 HordeSat，平均加速比提升两倍。并且，在 2020-2025 年连续多届国际 SAT 竞赛中，MallobSAT 均取得优异排名，并成功解决了多个往届未破解的竞赛难题(Froleyks et al. 2021),(Tomáš Balyo et al. 2020),(Tomás Balyo et al. 2022),(Tomas Balyo et al. 2023),(M. J. Heule et al. 2024),(Codel et al. 2025)。

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

预处理

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

而在 PL-PRS-Kissat 中，还通过遗传算法 GASPI(Saouli, Baarir, and Dutheillet 2024) 生成了初始解，用于构造一半求解器的初始解，另一半求解器的初始相位。

混合求解

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

混合实现存在两种基础路径：其一是分治式组合法（由 c-sat(Ohmura and Ueda 2009) 率先提出），其二是组合式分治法（如 ampharos(Audemard et al. 2016) 采用的适应性分治策略，允许在搜索空间同一子区域部署多个工作节点）。 此外还存在更复杂的混合方法，包括散射法(Hyvärinen, Junttila, and Niemelä 2006),(Hyvärinen and Manthey 2012) 以及基于转移启发式的策略(Audemard et al. 2016),(Blochinger 2005),(Martins, Manquinho, and Lynce 2010),(Schulz and Blochinger 2010)。

基于 GPU 的并行

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

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

基于连续搜索的 SAT 求解器

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

Audemard, Gilles, Benoı̂t Hoessen, Said Jabbour, Jean-Marie Lagniez, and Cédric Piette. 2012. “Revisiting Clause Exchange in Parallel SAT Solving.” In International Conference on Theory and Applications of Satisfiability Testing, 200–213. Springer.

Audemard, Gilles, Benoı̂t Hoessen, Saı̈d Jabbour, and Cédric Piette. 2014. “Dolius: A Distributed Parallel SAT Solving Framework.” In POS@ SAT, 1–11.

Audemard, Gilles, Jean-Marie Lagniez, Nicolas Szczepanski, and Sébastien Tabary. 2016. “An Adaptive Parallel SAT Solver.” In International Conference on Principles and Practice of Constraint Programming, 30–48. Springer.

Audemard, Gilles, and Laurent Simon. 2009. “Predicting Learnt Clauses Quality in Modern SAT Solvers.” In IJCAI, 9:399–404.

———. 2014. “Lazy Clause Exchange Policy for Parallel SAT Solvers.” In International Conference on Theory and Applications of Satisfiability Testing, 197–205. Springer.

———. 2017. “Glucose and Syrup in the SAT’17.” Proceedings of SAT Competition, 16–17.

Balyo, Tomáš, Armin Biere, Markus Iser, and Carsten Sinz. 2016. “SAT Race 2015.” Artificial Intelligence 241: 45–65.

Balyo, Tomáš, Nils Froleyks, MJH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. 2020. “The Results of SAT Competition 2021.” Sat 2020.

Balyo, Tomas, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. 2023. “Proceedings of Sat Competition 2023: Solver, Benchmark and Proof Checker Descriptions.”

Balyo, Tomás, Marijn Heule, and Matti Jarvisalo. 2017. “SAT Competition 2016: Recent Developments.” In Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 31.

Balyo, Tomás, Marijn JH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. 2022. “SAT COMPETITION 2022.”

Balyo, Tomáš, Peter Sanders, and Carsten Sinz. 2015. “Hordesat: A Massively Parallel Portfolio SAT Solver.” In International Conference on Theory and Applications of Satisfiability Testing, 156–72. Springer.

Beckers, Sander, Gorik De Samblanx, Floris De Smedt, Toon Goedemé, Lars Struyf, and Joost Vennekens. 2012. “Parallel Hybrid SAT Solving Using OpenCL.” Proceedings BNAIC 2012, 11–18.

Belov, Anton, Daniel Diepold, Marijn Heule, and Matti Järvisalo. 2014. “The Sat Competition 2014.” In Proc. SAT COMPETITION, 45.

Biere, Armin. 2010. “Lingeling, Plingeling, Picosat and Precosat at Sat Race 2010.”

———. 2012. “Lingeling and Friends Entering the SAT Challenge 2012.” Proceedings of SAT Challenge, 33–34.

———. 2014. “Yet Another Local Search Solver and Lingeling and Friends Entering the SAT Competition 2014.” Sat Competition 2014 (2): 65.

Blochinger, Wolfgang. 2005. “Towards Robustness in Parallel SAT Solving.” In PARCO, 301–8.

Blochinger, Wolfgang, Carsten Sinz, and Wolfgang Küchlin. 2003. “Parallel Propositional Satisfiability Checking with Distributed Dynamic Learning.” Parallel Computing 29 (7): 969–94.

Blumofe, Robert D, and Charles E Leiserson. 1999. “Scheduling Multithreaded Computations by Work Stealing.” Journal of the ACM (JACM) 46 (5): 720–48.

Böhm, Max, and Ewald Speckenmeyer. 1996. “A Fast Parallel SAT-Solver - Efficient Workload Balancing.” Ann. Math. Artif. Intell. 17 (3–4): 381–400. https://doi.org/10.1007/BF02127976.

Cen, Yunuo, Zhiwei Zhang, and Xuanyao Fong. 2025. “Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs.” In Proceedings of the AAAI Conference on Artificial Intelligence, 39:11140–49.

Chen, Zhihan, Xindi Zhang, Yuhang Qian, and Shaowei Cai. 2023. “Prs: A New Parallel/Distributed Framework for Sat.” SAT COMPETITION 2023: 39.

Chrabakh, Wahid, and Rich Wolski. 2003. “GrADSAT: A Parallel SAT Solver for the Grid.” In Proceedings of IEEE SC03. Vol. 53.

Codel, Cayden, Katalin Fazekas, Marijn J. H. Heule, Markus Iser, Cayden Codel, Katalin Fazekas, Marijn J. H. Heule, and Markus Iser. 2025. “Proceedings of SAT Competition 2025 : Solver and Benchmark Descriptions.” TU Wien. https://doi.org/10.34726/10379.

Dal Palù, Alessandro, Agostino Dovier, Andrea Formisano, and Enrico Pontelli. 2015. “Cud@ Sat: Sat Solving on Gpus.” Journal of Experimental & Theoretical Artificial Intelligence 27 (3): 293–316.

Ehlers, Thorsten, and Dirk Nowotka. 2019. “Tuning Parallel Sat Solvers.” Proceedings of Pragmatics of SAT 59: 127–43.

Ehlers, Thorsten, Dirk Nowotka, and Philipp Sieweck. 2014. “Communication in Massively-Parallel SAT Solving.” In 2014 IEEE 26th International Conference on Tools with Artificial Intelligence, 709–16. IEEE.

Fleury, Mathias, and Armin Biere. 2022. “Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing Instead of Copying Clauses.” arXiv Preprint arXiv:2207.13577.

Froleyks, Nils, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. 2021. “SAT Competition 2020.” Artificial Intelligence 301: 103572.

Gomes, Carla P, and Bart Selman. 2001. “Algorithm Portfolios.” Artificial Intelligence 126 (1–2): 43–62.

Hamadi, Youssef, Said Jabbour, and Jabbour Sais. 2012. “Control-Based Clause Sharing in Parallel SAT Solving.” In Autonomous Search, 245–67. Springer.

Hamadi, Youssef, Said Jabbour, and Lakhdar Sais. 2010. “ManySAT: A Parallel SAT Solver.” Journal on Satisfiability, Boolean Modelling and Computation 6 (4): 245–62.

Hamadi, Youssef, and Lakhdar Sais, eds. 2018. Handbook of Parallel Constraint Reasoning. Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-63516-3.

Heisinger, Maximilian, Mathias Fleury, and Armin Biere. 2020. “Distributed Cube and Conquer with Paracooba.” In International Conference on Theory and Applications of Satisfiability Testing, 114–22. Springer.

Heule, Marijn. 2018. “Schur Number Five.” In Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 32.

Heule, Marijn JH, Markus Iser, Matti Järvisalo, and Martin Suda. 2024. “Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions.”

Heule, Marijn JH, Oliver Kullmann, and Victor W Marek. 2016. “Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer.” In International Conference on Theory and Applications of Satisfiability Testing, 228–45. Springer.

Heule, Marijn JH, Oliver Kullmann, Siert Wieringa, and Armin Biere. 2011. “Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads.” In Haifa Verification Conference, 50–65. Springer.

Hyvärinen, Antti EJ, Tommi Junttila, and Ilkka Niemelä. 2006. “A Distribution Method for Solving SAT in Grids.” In International Conference on Theory and Applications of Satisfiability Testing, 430–35. Springer.

———. 2011. “Partitioning Search Spaces of a Randomized Search.” Fundamenta Informaticae 107 (2–3): 289–311.

Hyvärinen, Antti EJ, and Norbert Manthey. 2012. “Designing Scalable Parallel SAT Solvers.” In International Conference on Theory and Applications of Satisfiability Testing, 214–27. Springer.

Jurkowiak, Bernard, Chu Min Li, and Gil Utard. 2001. “Parallelizing Satz Using Dynamic Workload Balancing.” Electronic Notes in Discrete Mathematics 9: 174–89.

Kottler, Stephan, and Michael Kaufmann. 2011. “SArTagnan-a Parallel Portfolio SAT Solver with Lockless Physical Clause Sharing.” Pragmatics of SAT.

Kyrillidis, Anastasios, Anshumali Shrivastava, Moshe Vardi, and Zhiwei Zhang. 2020. “FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints.” In Proceedings of the AAAI Conference on Artificial Intelligence, 34:1552–60.

Kyrillidis, Anastasios, Moshe Vardi, and Zhiwei Zhang. 2021. “On Continuous Local Bdd-Based Search for Hybrid Sat Solving.” In Proceedings of the AAAI Conference on Artificial Intelligence, 35:3841–50.

Le Frioux, Ludovic, Souheib Baarir, Julien Sopena, and Fabrice Kordon. 2017. “PaInleSS: A Framework for Parallel SAT Solving.” In Theory and Applications of Satisfiability Testing – SAT 2017, edited by Serge Gaspers and Toby Walsh, 10491:233–50. Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-66263-3_15.

Martins, Ruben, Vasco Manquinho, and Inês Lynce. 2010. “Improving Search Space Splitting for Parallel SAT Solving.” In 2010 22nd IEEE International Conference on Tools with Artificial Intelligence, 1:336–43. IEEE.

Ohmura, Kei, and Kazunori Ueda. 2009. “C-Sat: A Parallel SAT Solver for Clusters.” In International Conference on Theory and Applications of Satisfiability Testing, 524–37. Springer.

Osama, Muhammad, and Anton Wijs. 2019. “Parallel SAT Simplification on GPU Architectures.” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 21–40. Springer.

Osama, Muhammad, Anton Wijs, and Armin Biere. 2021. “SAT Solving with GPU Accelerated Inprocessing.” In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 133–51. Springer.

Prevot, Nicolas, Mate Soos, and Kuldeep S Meel. 2021. “Leveraging GPUs for Effective Clause Sharing in Parallel SAT Solving.” In International Conference on Theory and Applications of Satisfiability Testing, 471–87. Springer.

Roussel, Olivier. 2012. “Description of Ppfolio (2011).” Proc. SAT Challenge, 46.

Sanders, Peter. 1994. “A Detailed Analysis of Random Polling Dynamic Load Balancing.” In Proceedings of the International Symposium on Parallel Architectures, Algorithms and Networks (ISPAN), 382–89. IEEE.

Saoudi, Mazigh, Souheib Baarir, Julien Sopena, and Thibault Lejemble. 2025. “D-Painless: A Framework for Distributed Portfolio SAT Solving.” In Tools and Algorithms for the Construction and Analysis of Systems, edited by Arie Gurfinkel and Marijn Heule, 15697:45–64. Cham: Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-90653-4_3.

Saoudi, Mazigh, Thibault Lejemble, Souheib Baarir, and Julien Sopena. n.d. “PL-PRS-BVA-KISSAT in SAT Competition 2024.”

Saouli, Sabrine, Souheib Baarir, and Claude Dutheillet. 2024. “Tackling the Polarity Initialization Problem in Sat Solving Using a Genetic Algorithm.” In NASA Formal Methods Symposium, 21–36. Springer.

Schreiber, Dominik. 2024. “MallobSat and MallobSat-ImpCheck in the SAT Competition 2024.” In SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions, 21–22. http://hdl.handle.net/10138/584822.

Schreiber, Dominik, and Peter Sanders. 2024. “MallobSat: Scalable SAT Solving by Clause Sharing.” Journal of Artificial Intelligence Research (JAIR) 80: 1437–95. https://doi.org/10.1613/jair.1.15827.

Schulz, Sven, and Wolfgang Blochinger. 2010. “Cooperate and Compete! A Hybrid Solving Strategy for Task-Parallel SAT Solving on Peer-to-Peer Desktop Grids.” In 2010 International Conference on High Performance Computing & Simulation, 314–23. IEEE.

Sinz, Carsten, Wolfgang Blochinger, and Wolfgang Küchlin. 2001. “PaSAT—Parallel SAT-Checking with Lemma Exchange: Implementation and Applications.” Electronic Notes in Discrete Mathematics 9: 205–16.

Tseitin, G. S. 1983. “On the Complexity of Derivation in Propositional Calculus.” In Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, edited by Jörg H. Siekmann and Graham Wrightson, 466–83. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_28.

Vallade, Vincent, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, and Fabrice Kordon. 2020. “Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving.” In International Conference on Theory and Applications of Satisfiability Testing, 11–27. Springer.

Vallade, Vincent, Ludovic Le Frioux, Razvan Oanea, Souheib Baarir, Julien Sopena, Fabrice Kordon, Saeed Nejati, and Vijay Ganesh. 2021. “New Concurrent and Distributed Painless Solvers: P-Mcomsps, p-Mcomsps-Com, p-Mcomsps-Mpi, and p-Mcomsps-Com-Mpi.” SAT COMPETITION 2021: 40.

Xu, Lin, Frank Hutter, Holger Hoos, and Kevin Leyton-Brown. 2012. “Evaluating Component Solver Contributions to Portfolio-Based Algorithm Selectors.” In International Conference on Theory and Applications of Satisfiability Testing, 228–41. Springer.

Zhang, Hantao, Maria Paola Bonacina, Jieh Hsiang, and others. 1996. “PSATO: A Distributed Propositional Prover and Its Application to Quasigroup Problems.” Journal of Symbolic Computation 21 (4–6): 543–60.