SAT Solving with GPU Accelerated Inprocessing

研究问题及研究意义

研究问题：布尔可满足性(SAT)问题的GPU求解

SAT问题：判断是否存在一组布尔变量的赋值，使得给定的布尔公式为真。

研究意义：逻辑学、图论、计算机科学、计算机工程和运筹学等领域中的许多问题都可以转化为SAT问题进行求解。

内处理(Inprocessing)

目的：减少学习子句的数量

内处理：在搜索过程中，删除冗余的子句

• 变量消除(VE)

• 自归纳(SUB)

• 阻塞子句消除(BCE)

• 急切冗余消除(ERE)：作者提出的

并行内处理

问题：无法同时对所有变量进行内处理

• 变量之间存在依赖（子句）

  同一个子句中的变量可能同时尝试更改这个子句

方法：最少约束变量选择(LCVE)算法

• 选择出现次数低于某个阈值的变量
• 每当选中变量进行处理时，冻结与该变量具有依赖关系的其他变量

三阶段变量消去

问题：在之前的实现中，添加子句使用了两个原子指令：添加新子句；添加新文字。

方法：类似于GC的思想，将添加子句分为三个阶段。

• 确定子句大小
• 确定子句地址
• 存储新子句

使用阶段间同步代替原子指令。

实验结果

论文贡献与个人评价

论文贡献：

• 针对GPU的垃圾回收机制
• 并行内处理过程
• 使用CUDA实现了ParaFROST求解器（第一个GPU CDCL求解器）

个人评价：

• 垃圾回收过程是基于数据的并行
• 并行内处理，总体上是基于任务的并行
• 实际效果不好的原因（猜测）：没有对冲突分析过程进行并行化

总结

SAT问题是数学中的一个基础问题，而逻辑学、图论、计算机科学和运筹学等领域中的众多问题都可以转化为SAT问题。提高SAT求解器的性能，也就相当于提高了一大类问题的求解效率。在本论文中，作者希望通过GPU实现一个性能更高的SAT求解器，但GPU有限的存储空间成为了实现过程中的第一个阻碍。所以作者提出了一种并行回收垃圾存储空间的算法，相较于线性的垃圾回收算法具有极大的性能提升。作者还设计了一种在内处理过程中消除变量依赖的任务分配算法，使得内处理过程具有了一定的并行性。结合三阶段变量消去优化，并行内处理部分有平均1.8倍的性能提升。但是，可能由于该论文没有对CDCL SAT求解器的关键部分——冲突分析过程进行优化，导致GPU求解器对比CPU版本的整体提升并不大。