Open AccessAn Parallel FPGA SAT Solver Based on Multi‐Thread and Pipeline
Author(s) -
Tiejun LI,
Kefan MA,
Jianmin ZHANG
Publication year - 2021
Publication title -
chinese journal of electronics
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.267
H-Index - 25
eISSN - 2075-5597
pISSN - 1022-4653
DOI - 10.1049/cje.2021.08.001
Subject(s) - computer science , solver , boolean satisfiability problem , thread (computing) , parallel computing , speedup , field programmable gate array , pipeline (software) , satisfiability , algorithm , computer hardware , programming language , operating system
The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application. A parallel multi‐thread SAT solver named pprobSAT+ 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 pprobSAT+ have achieved substantial improvement while a solution is found.