An FPGA Solver for WSAT Algorithms

Kenji KANAZAWA  Tsutomu MARUYAMA 

Publication
D - Abstracts of IEICE TRANSACTIONS on Information and Systems (Japanese Edition)  Vol.J89-D  No.6  pp.1173-1181
Publication Date: 2006/06/01
Online ISSN: 1881-0225
Print ISSN: 1880-4535
Type of Manuscript: Special Section PAPER (Special Issue Reconfigurable Systems)
Category: 
Keyword: 
SAT,  WSAT,  FPGA, 

Full Text(in Japanese): PDF(404.6KB)

Summary: 
WSAT and its variants are one of the best performing stochastic local search algorithms for the satisfiability (SAT) problem. In this paper, we propose a new FPGA solver for WSAT algorithms. The features of our solver are (1) high parallelism by small size units to evaluate clauses in each instance of the SAT problem, (2) multi-thread execution to achieve high performance, and (3) fast data-downloading for each instance. We implemented the solver for problems up to 256 variables and 1024 clauses on XC2V6000, and it used 45% of slices and five block RAMs. Our implementation shows higher performance over previous SAT solvers on FPGAs.