• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

J4 ›› 2016, Vol. 38 ›› Issue (04): 634-639.

• 论文 • Previous Articles     Next Articles

State of the art and future research of
a SAT problem solver on FPGA  

MA Kefan,XIAO Liquan,ZHANG Jianmin,LI Tiejun   

  1. (College of Computer,National University of Defense Technology,Changsha 410073,China)
  • Received:2015-08-26 Revised:2015-10-24 Online:2016-04-25 Published:2016-04-25

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