首页|Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
  • 维普
The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application.Field-programmable gate array (FPGA) has been addressed frequently to accelerate the SAT solving process in the last few years owing to its parallelism and flexibility.We have proposed a novel SAT solver based on an improved local search algorithm on the reconfigurable hardware platform.The new software preprocessing procedure and hardware architecture are involved to solve large-scale SAT problems instances.As compared with the past solvers,the proposed solver has the following advantages: the preprocessing technology can strongly improve the efficiency of solver;the strategy of strengthening the variable selection can avoid the same variable flipped continuously and repeatedly.It reduces the possibility of search falling into local minima.The experimental results indicate that the solver can solve problems of up to 32K variables/128K clauses without off-chip memory banks,and has better performance than previous works.

FPGASATPreprocessingEnhanced constraintIncomplete algorithmCo-design

MA Kefan、XIAO Liquan、ZHANG Jianmin、LI Tiejun

展开 >

College of Computer, National University of Defense Technology, Changsha 410073, China

This work is supported by the National Major Scientific Research ProgramNational Natural Science Foundation of ChinaNational Natural Science Foundation of China

2016YFB02002036110308361133007

2019

10.1049/cje.2019.06.015

中国电子杂志(英文版)

中国电子杂志(英文版)

CSTPCDCSCDSCIEI
ISSN：1022-4653
年,卷(期)：2019.28(5)
  • 1
  • 26