关键词: 可满足性问题, 天河超算, 单元传播, 搜索空间划分, VSIDS, kissat求解器

Abstract: The satisfiability problem (SAT) solver is widely applied in fields such as hardware and software verification, information security, and computational biology. Current optimizations of SAT solvers primarily focus on reducing the solution space of formulas and simplifying the entire solving formula. However, reducing the solution space faces challenges such as slow space reduction and insufficient parallel granularity, while formula simplification exhibits poor performance when combined with existing parallel strategies for solving small-scale problems. This paper introduces kissat++, developed based on kissat, the fastest serial SAT solver to date. Specifically, we propose a fine-grained parallel algorithm for unit propagation using observation list-based dynamic blocking techniques and introduce guided paths to achieve coarse-grained parallel optimization during the search space partitioning process. To further enhance space partitioning efficiency, factors such as decision levels are considered when constructing guided paths to select key variables early, thereby reducing the search space on each process. Experimental results on the Tianhe supercomputer demonstrate that kissat++ achieves more than a 2× speedup compared to the original kissat. Additionally, it solves 49 more instances within the time limit on the SAT benchmark set and ranks ninth among the 16 solvers submitted to the parallel track of the 2023 competition.

Key words: SAT, Tianhe supercomputer, unit propagation, search space partitioning, variable state independent decaying sum(VSIDS), kissat solver