An Parallel FPGA SAT Solver Based on Multi-Thread and Pipeline  

作　　者：LI Tiejun MA Kefan ZHANG Jianmin 

机构地区：[1]College of Computer,National University of Defense Technology,Changsha 410073,China

出　　处：《Chinese Journal of Electronics》2021年第6期1008-1016,共9页电子学报（英文版）

基　　金：supported by the National Key Research and Development Program of China (No.2018YFB0204301);the National Natural Science Foundation of China (No.62072464, No.U19A2062)。

摘　　要：The Boolean Satisfiability(SAT) problem is the key problem in computer theory and application. A parallel multi-thread SAT solver named pprob SAT+ on a configurable hardware is proposed. In the algorithm,multithreads are executed simultaneously to hide the circuit stagnate. In order to improve the working frequency and throughput of the SAT solver, the deep pipeline strategy is adopted. When all data stored in block random access memory of the field programmable gate array, the solver can achieve maximum performance. If partial data are stored in the external memory, the size of the problem instances the SAT solver can be greatly improved. The experimental results show that the speedup of three-thread SAT solver is approximately 2.4 times with single thread,and shows that the pprob SAT+ have achieved substantial improvement while a solution is found.

关 键 词：FPGA Incomplete algorithm MULTI-THREAD PIPELINE 

分 类 号：TN791[电子电信—电路与系统]