并行SAT求解器23
截至2023年SAT竞赛中优秀求解器的简图（不完整）。并行以Painless框架为代表，介绍了PRS求解器的改进，分布式以Mallob框架为代表，介绍了改进。
并行算法¶
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算法。新算法在理论上具有较低复杂度，实现后在多种不同的负载下均表现出较高的性能。