关键词: 现场可编程门逻辑, 可满足性, 求解器

Abstract:

As the first proved NPcomplete problem，Boolean satisfiability problem (SAT) is a key problem in computer theory and applications, and has crucial significance in both theoretical research and practical applications. A variety of SAT solvers have emerged in recent years. However, the operation efficiency of SAT solvers is always a key factor affecting its applications, so taking advantage of the hardware's high performance and parallelism to accelerate the SAT solving process becomes a hot research topic in the area of verification. We summarize the methods for accelerating SAT solving solution, which use the parallelism and flexibility of FPGA, and analyze the acceleration policies of applicationspecified solver emphatically. Through indepth analysis of these methods, we point out their advantages and disadvantages, and provide ideas for future research.

Key words: FPGA;SAT;solver