Parallel optimization for satisfiability problem solving.

Saved in:

Bibliographic Details
Title:	Parallel optimization for satisfiability problem solving.
Authors:	LI, Ji¹, ZHOU, Lei², GONG, Chunye^3,4, MA, Di³, SHEN, Yulin⁵, ZHANG, Xiang³ zhangxiang08@nudt.edu.cn
Source:	Computer Engineering & Science / Jisuanji Gongcheng yu Kexue. May2026, Vol. 48 Issue 5, p793-802. 10p.
Subjects:	Satisfiability (Computer science), Parallel programming, Constraint satisfaction, Software verification, Verification of computer systems
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 2x 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. [ABSTRACT FROM AUTHOR]
	Copyright of Computer Engineering & Science / Jisuanji Gongcheng yu Kexue is the property of Computer Engineering & Science and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
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 2x 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. [ABSTRACT FROM AUTHOR]
ISSN:	1007130X
DOI:	10.3969/j.issn.1007-130X.2026.05.004