可满足性问题SAT求解器广泛应用于硬件与软件验证、信息安全和计算生物学等领域。当前SAT求解器优化主要通过缩小公式的求解空间和化简整个求解公式。缩小求解空间存在空间缩小速度慢和并行粒度不充分的问题；化简公式在求解小规模问题时结合已有并行策略的表现较差。基于当前最快串行SAT求解器kissat研发了kissat++，具体为提出了基于观察列表动态分块技术实现单元传播过程的细粒度并行算法，引入引导路径完成搜索空间划分过程的粗粒度并行优化。为进一步提升空间划分效率，在构建引导路径时考虑决策层等因素尽早选出关键变量，缩小每个进程上的搜索空间。天河超算上的实验结果表明，相比原始kissat,kissat++获得了2倍以上的加速，同时在SAT基准集上的限定时间内多求出49个实例，能在2023年竞赛并行赛道提交的16个求解器中排名第9。

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.