In this paper, we will propose a new solution method for SAT (Satisfiability Problems) using FPGA (Field-Programmable Gate Arrays) and logic synthesis system. This method is distinctive in that a logic circuit specialized to solve each problem instance is configured on FPGA. This approach has become possible due to the progress in reconfigurable computing technology in recent years and opens a new possibility in design principle of algorithms: SAT is a kind of constraint satisfaction problem and is a general framework which can represent many application problems. In this paper, we will propose various algorithms which are suitable for implementation on hardware. Among these algorithms, the one which has the highest performance has a performance equal to the Davis-Putman algorithm which introduced the heuristic with dynamic ordering of variables. From the evaluation results using simulation, we show that by the method proposed herein, the solution of a 3-SAT problem instance with 400 variables generated in a very hard random can be obtained in 1.6 minutes when the circuit is operated at a machine cycle of 10 MHz. Moreover, a very hard problem instance with 128 variables and 256 clauses was packaged on FPGAs and its operation was confirmed.
|Number of pages||12|
|Journal||Electronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi)|
|Publication status||Published - Mar 2003|
All Science Journal Classification (ASJC) codes
- Physics and Astronomy(all)
- Computer Networks and Communications
- Electrical and Electronic Engineering