| Presentation | 2004/1/16 Implementing a Model-Generation Theorem Prover on an FPGA Atsushi KAWANO, Hiroshi FUJITA, Ryuzo HASEGAWA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, a design and implementation of theorem prover PCMGTP on an FPGA chip is described. PCMGTP is based on a model-generation method which is sound and complete to decide satisfiability of a set of clauses of propositional logic. Given a set of clauses, the whole circuit is re-configured on an FPGA chip together with a small PCMGTP kernel modules. Since closure computation with definite clauses is most time consuming in PCMGTP, it is essential to exploit as much hardware parallelism as possible in designing the corresponding part. Also some useful circuits are designed to choose suitable clauses for case splitting and to perform backtracking for proof search. Experimental results show significant performance in solving some benchmark SAT problems. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Theorem provers / Model generation / SAT solvers / FPGA / Reconfigurable computing |
| Paper # | VLD2003-134,CPSY2003-43 |
| Date of Issue |
| Conference Information | |
| Committee | VLD |
|---|---|
| Conference Date | 2004/1/16(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 | VLSI Design Technologies (VLD) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Implementing a Model-Generation Theorem Prover on an FPGA |
| Sub Title (in English) | |
| Keyword(1) | Theorem provers |
| Keyword(2) | Model generation |
| Keyword(3) | SAT solvers |
| Keyword(4) | FPGA |
| Keyword(5) | Reconfigurable computing |
| 1st Author's Name | Atsushi KAWANO |
| 1st Author's Affiliation | () |
| 2nd Author's Name | Hiroshi FUJITA |
| 2nd Author's Affiliation | |
| 3rd Author's Name | Ryuzo HASEGAWA |
| 3rd Author's Affiliation | |
| Date | 2004/1/16 |
| Paper # | VLD2003-134,CPSY2003-43 |
| Volume (vol) | vol.103 |
| Number (no) | 579 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |