关键词: 布尔可满足, FPGA, 不完全算法, 多线程

Abstract: The Boolean satisfiability (SAT) problem is the key problem in computer theory and application. his paper proposes a parallel SAT solver based on incomplete algorithm on FPGA. The algorithm uses a multi-threaded strategy to reduce the waiting time of related components and improve the efficiency of the solver. In addition, different threads use data storage structures that share addresses and clause information to reduce the resource overhead of on-chip memory. When all data is stored in the FPGA’s on-chip memory, the solver can achieve the best performance. The experimental results show that, compared with the single-threaded solver, the solver proposed in this paper can achieve a speedup of more than 2 times. 

Key words: boolean satisfiability, FPGA, incomplete algorithm, multi-thread