| Presentation | 2005-01-25 Solving SAT problems by PCMGTP on FPGA Shohei KINOSHITA, Junichi MATSUDA, Hiroshi FUJITA, Miyuki KOSHIMURA, Ryuzo HASEGAWA, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, a new design of the SAT solver PCMGTP implemented on an FPGA chip is described. Although the previous implementation of PCMGTP achieved considerable speedup in solving SAT benchmark problems compared to the software counterpart of MGTP, it failed to compete with the state-of-the-art SAT solvers in speed and was unable to deal with large problems due to the limited capacity of FPGA. We tried to improve our design by removing some redundancy in the data representation and the redundant states in the deduction engine. Also, we developed a new circuit called BCBE for performing logical implication, and modified the tournament circuit so as to deal with very large candidates and to shorten the critical path. As the result, the new implementation achieved speedup by factor of five as well as an order of magnitude space reduction compared to the previous one. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | SAT solvers / FPGA / Reconfigurable logic / Theorem proving / Model generation |
| Paper # | VLD2004-107,CPSY2004-73 |
| Date of Issue |
| Conference Information | |
| Committee | CPSY |
|---|---|
| Conference Date | 2005/1/18(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Computer Systems (CPSY) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Solving SAT problems by PCMGTP on FPGA |
| Sub Title (in English) | |
| Keyword(1) | SAT solvers |
| Keyword(2) | FPGA |
| Keyword(3) | Reconfigurable logic |
| Keyword(4) | Theorem proving |
| Keyword(5) | Model generation |
| 1st Author's Name | Shohei KINOSHITA |
| 1st Author's Affiliation | Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University() |
| 2nd Author's Name | Junichi MATSUDA |
| 2nd Author's Affiliation | Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 3rd Author's Name | Hiroshi FUJITA |
| 3rd Author's Affiliation | Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 4th Author's Name | Miyuki KOSHIMURA |
| 4th Author's Affiliation | Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 5th Author's Name | Ryuzo HASEGAWA |
| 5th Author's Affiliation | Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| Date | 2005-01-25 |
| Paper # | VLD2004-107,CPSY2004-73 |
| Volume (vol) | vol.104 |
| Number (no) | 591 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |