Open AccessAccelerating an FPGA‐Based SAT Solver by Software and Hardware Co‐design
Author(s) -
Ma Kefan,
Xiao Liquan,
Zhang Jianmin,
Li Tiejun
Publication year - 2019
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.2019.06.015
Subject(s) - computer science , field programmable gate array , solver , co design , software , fpga prototype , computer architecture , parallel computing , embedded system , computer hardware , programming language
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.