计算机工程与科学2026，Vol.48Issue(5)：793-802,10.DOI:10.3969/j.issn.1007-130X.2026.05.004
可满足性问题并行求解优化
Parallel optimization for satisfiability problem solving
摘要
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 for-mula.However,reducing the solution space faces challenges such as slow space reduction and insuffi-cient 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 al-gorithm 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 con-structing 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.关键词
可满足性问题/天河超算/单元传播/搜索空间划分/VSIDS/kissat求解器Key words
SAT/Tianhe supercomputer/unit propagation/search space partitioning/variable state independent decaying sum(VSIDS)/kissat solver分类
信息技术与安全科学引用本文复制引用
李骥,周磊,龚春叶,马迪,沈玉林,张翔..可满足性问题并行求解优化[J].计算机工程与科学,2026,48(5):793-802,10.基金项目
国家自然科学基金(62032023,42104078,61902411) （62032023,42104078,61902411）
