The Community for Technology Leaders
2014 47th Hawaii International Conference on System Sciences (1998)
Kohala Coast, HI
Jan. 6, 1998 to Jan. 9, 1998
ISSN: 1060-3425
ISBN: 0-8186-8251-5
pp: 179
Makoto Yokoo , NTT Communication Science Laboratories
Hiroshi Sawada , NTT Communication Science Laboratories
Takayuki Suyama , NTT Communication Science Laboratories
This paper presents new results on an approach for solving satisfiability problems (SAT), i.e. creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). This approach becomes feasible due to the recent advances in FPGAs and high-level logic synthesis. In this approach, each SAT problem is automatically analyzed and implemented on FPGAs. We have developed an algorithm which is suitable for implementing on a logic circuit. This algorithm is equivalent to the Davis-Putnam procedure with a powerful dynamic variable ordering heuristic. The algorithm does not have a large memory structure like a stack; thus sequential accesses to the memory do not become a bottleneck in algorithm execution. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 20 minutes at a clock rate of 1MHz.
Makoto Yokoo, Hiroshi Sawada, Takayuki Suyama, "Solving Satisfiability Problems Using Logic Synthesis and Reconfigurable Hardware", 2014 47th Hawaii International Conference on System Sciences, vol. 07, no. , pp. 179, 1998, doi:10.1109/HICSS.1998.649212
530 ms
(Ver 3.3 (11022016))