| Paper Abstract and Keywords |
| Presentation |
2005-01-25 15:50
Solving SAT problem by PCMGTP on FPGA
Shohei Kinoshita, Junichi Matsuda, Hiroshi Fujita, Miyuki Koshimura, Ryuzo Hasegawa (Kyushu Univ) |
| Abstract |
(in Japanese) |
(See Japanese page) |
| (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) |
| (in English) |
SAT solvers / FPGA / Reconfigurable logic / Theorem proving / Model generation / / / |
| Reference Info. |
IEICE Tech. Rep., vol. 104, pp. 57-62, Jan. 2005. |
| Paper # |
|
| Date of Issue |
2005-01-18 (VLD, CPSY) |
| ISSN |
Print edition: ISSN 0913-5685 |
| Download PDF |
|
| Conference Information |
| Committee |
CPSY VLD IPSJ-SLDM |
| Conference Date |
2005-01-25 - 2005-01-26 |
| Place (in Japanese) |
(See Japanese page) |
| Place (in English) |
|
| Topics (in Japanese) |
(See Japanese page) |
| Topics (in English) |
FPGA and its Application, etc |
| Paper Information |
| Registration To |
IPSJ-SLDM |
| Conference Code |
2005-01-CPSY-VLD-IPSJ-SLDM |
| Language |
Japanese |
| Title (in Japanese) |
(See Japanese page) |
| Sub Title (in Japanese) |
(See Japanese page) |
| Title (in English) |
Solving SAT problem 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 |
| Keyword(6) |
|
| Keyword(7) |
|
| Keyword(8) |
|
| 1st Author's Name |
Shohei Kinoshita |
| 1st Author's Affiliation |
Kyushu University (Kyushu Univ) |
| 2nd Author's Name |
Junichi Matsuda |
| 2nd Author's Affiliation |
Kyushu University (Kyushu Univ) |
| 3rd Author's Name |
Hiroshi Fujita |
| 3rd Author's Affiliation |
Kyushu University (Kyushu Univ) |
| 4th Author's Name |
Miyuki Koshimura |
| 4th Author's Affiliation |
Kyushu University (Kyushu Univ) |
| 5th Author's Name |
Ryuzo Hasegawa |
| 5th Author's Affiliation |
Kyushu University (Kyushu Univ) |
| 6th Author's Name |
|
| 6th Author's Affiliation |
() |
| 7th Author's Name |
|
| 7th Author's Affiliation |
() |
| 8th Author's Name |
|
| 8th Author's Affiliation |
() |
| 9th Author's Name |
|
| 9th Author's Affiliation |
() |
| 10th Author's Name |
|
| 10th Author's Affiliation |
() |
| 11th Author's Name |
|
| 11th Author's Affiliation |
() |
| 12th Author's Name |
|
| 12th Author's Affiliation |
() |
| 13th Author's Name |
|
| 13th Author's Affiliation |
() |
| 14th Author's Name |
|
| 14th Author's Affiliation |
() |
| 15th Author's Name |
|
| 15th Author's Affiliation |
() |
| 16th Author's Name |
|
| 16th Author's Affiliation |
() |
| 17th Author's Name |
|
| 17th Author's Affiliation |
() |
| 18th Author's Name |
|
| 18th Author's Affiliation |
() |
| 19th Author's Name |
|
| 19th Author's Affiliation |
() |
| 20th Author's Name |
|
| 20th Author's Affiliation |
() |
| Speaker |
Author-1 |
| Date Time |
2005-01-25 15:50:00 |
| Presentation Time |
30 minutes |
| Registration for |
IPSJ-SLDM |
| Paper # |
VLD2004-107, CPSY2004-73 |
| Volume (vol) |
vol.104 |
| Number (no) |
no.589(VLD), no.591(CPSY) |
| Page |
pp.57-62 |
| #Pages |
6 |
| Date of Issue |
2005-01-18 (VLD, CPSY) |