sfSAT: An Incremental SAT Solver Based on Prioritizing Small-scale Clauses
Lei Gong, Zijian Wang, Chengxiang Chu, Yuping Yuan, Tengfei Wang, Rui Hu · 2019 IEEE International Conference on Power, Intelligent Computing and Systems (ICPICS) · 2019
The satisfiability(SAT) of the propositional logic formula is the most classic NP-hard problem and the earliest proven NP-complete problem, making an invaluable contribution to both industry and research. Based on the interpretation of MiniSat's CDCL solver and related technologies, this paper implements a solver sfSAT for the priority processing of small-scale clauses in the process of unit propagation. Through experiments, this paper analyzed and compared sfSAT, bfSAT(the author's improved solver) and MiniSat data using the SAT competition 2017 benchmark.