2024¶
IJCAI_2012_Inprocessing
SAT问题是数学中的一个基础问题，而逻辑学、图论、计算机科学和运筹学等领域中的众多问题都可以转化为SAT问题。为了提高SAT求解器的性能，现代求解器往往会使用多种推理规则对子句进行化简。这些操作在求解过程前被称为预处理，在求解过程中被称为内处理。本文的作者认为混合使用多种化简技术可能存在求解过程不完整的问题，缺乏相关的理论支持。于是作者通过分析现有的技术，提取出其中的关键步骤，绘制出化简技术之间的关系图，随后提出了一个内处理规则框架，并且证明只要遵循该框架就可以保证求解过程的完整性。作者还将被广泛认可的求解技术套用到框架中以证明框架的合理性。我认为这个内处理框架能够为未来SAT求解器的设计提供指导性的帮助。
TACAS_2021_GPU Inprocessing
SAT问题是数学中的一个基础问题，而逻辑学、图论、计算机科学和运筹学等领域中的众多问题都可以转化为SAT问题。提高SAT求解器的性能，也就相当于提高了一大类问题的求解效率。在本论文中，作者希望通过GPU实现一个性能更高的SAT求解器，但GPU有限的存储空间成为了实现过程中的第一个阻碍。所以作者提出了一种并行回收垃圾存储空间的算法，相较于线性的垃圾回收算法具有极大的性能提升。作者还设计了一种在内处理过程中消除变量依赖的任务分配算法，使得内处理过程具有了一定的并行性。结合三阶段变量消去优化，并行内处理部分有平均1.8倍的性能提升。但是，可能由于该论文没有对CDCL SAT求解器的关键部分——冲突分析过程进行优化，导致GPU求解器对比CPU版本的整体提升并不大。
Handbook of SAT_3_完备算法
本章主要介绍了三类完备的SAT求解算法，分别是存在量化、逻辑推理和系统搜索。并简单介绍了目前主流求解器使用的搜索与推理结合的算法，介绍了DPLL和DPLL+两个具体算法。
ASPLOS_2021_GAMMA
稀疏矩阵乘法是计算机领域中的基础问题，是许多稀疏算法的核心，如稀疏深度神经网络，稀疏线性和张量代数，图分析等。通过提高运行速度或是降低所需的缓存空间，都可以提高稀疏矩阵乘法在cpu与gpu上的运行效率。该论文从优化访存的角度出发，利用Gustavson算法，使得稀疏矩阵乘法的数据流行平稳化，从而使得内存的访问局部连续化。作者还针对该访存模式设计了片上存储结构和对应的动态调度算法，相较于同类的硬件系统提高了性能并降低了片上储存空间。
PPoPP_2023_FASTBCC
双连通分量（BCC）的求解是图论中的基础问题，可以广泛应用于如平面性检验、中心性计算和网络分析等任务中。Hopcroft-Tarjan算法是串行求解BCC的经典算法，其时间复杂度\(O(n+m)\)与空间复杂度\(O(n)\)都在可接受的范围内，但由于其基于深度优先搜索（DFS）树框架，难以并行化。最初能够并行求解BCC的Tarjan-Vishkin算法可以基于任意生成树（AST）框架，但由于其使用了过多的额外空间\(O(m)\)，没有被广泛采用。后续算法采用广度优先搜索（BFS）树框架对Tarjan-Vishkin算法进行改进，将额外空间降低到\(O(n)\)，但由于BFS的特性，改进后的算法在直径较大的图中性能不佳。在该论文中，作者重新审视Hopcroft-Tarjan串行算法，提取出关键思想，结合了高效的并行单连通分量算法，实现了AST框架下使用\(O(n)\)额外空间的FAST-BCC算法。该算法流程简明，实现高效，在多种负载下均表现出较高的性能。
SPAA_2021_Parallel Shortest Paths
单源最短路（SSSP）问题是图论中的经典问题，对其理论与实现的研究都具有重大意义。目前，大部分并行SSSP算法基于Δ-Stepping，即以Δ为步长进行Dijkstra算法，并在子过程中进行Bellman-Ford算法。然而，超参数Δ的选择与图的结构、权重分布及具体实现相关，而且对性能的影响极大。在本文中，作者提出了惰性批量优先队列（LAB-PQ），并基于现有的并行SSSP算法，构建了新的Stepping算法框架，实现了超参数不敏感的并行SSSP算法。新算法在理论上具有较低复杂度，实现后在多种不同的负载下均表现出较高的性能。
HVC_2015_VSIDS
现代SAT求解器中普遍使用VSIDS方法及其变种作为启发式搜索的方法之一，该论文对这个方法的合理性给出了解释，对SAT问题的启发式搜索策略的选择具有指导性的意义。VSIDS方法是优先选择在最近推断过的子句中，出现次数多的变量，在后续的变量枚举时优先枚举。由于子句代表了变量之间的相关性，作者使用图论中的社区结构和桥接变量进行解释。VSIDS高效的原因主要包括：挑选高中心性的桥接变量、倾向于从较小的社区中选择变量和倾向于从最近的社区中选择变量。作者对VSIDS的有效性分析较为完备，对该论文进一步思考，社区结构性强的SAT问题具有良好的可分性，可以通过这种可分性提高SAT问题的并行性。