Abstract
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 reconfigured 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.
| Original language | English |
|---|---|
| Pages (from-to) | 13-18 |
| Number of pages | 6 |
| Journal | Research Reports on Information Science and Electrical Engineering of Kyushu University |
| Volume | 9 |
| Issue number | 1 |
| Publication status | Published - Mar 1 2004 |
Fingerprint
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering
Cite this
Implementing a model-generation theorem prover on an FPGA. / Fujita, Hiroshi; Kawano, Atsushi; Hasegawa, Ryuzo.
In: Research Reports on Information Science and Electrical Engineering of Kyushu University, Vol. 9, No. 1, 01.03.2004, p. 13-18.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Implementing a model-generation theorem prover on an FPGA
AU - Fujita, Hiroshi
AU - Kawano, Atsushi
AU - Hasegawa, Ryuzo
PY - 2004/3/1
Y1 - 2004/3/1
N2 - 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 reconfigured 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.
AB - 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 reconfigured 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.
UR - http://www.scopus.com/inward/record.url?scp=3543137203&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=3543137203&partnerID=8YFLogxK
M3 - Article
AN - SCOPUS:3543137203
VL - 9
SP - 13
EP - 18
JO - Research Reports on Information Science and Electrical Engineering of Kyushu University
JF - Research Reports on Information Science and Electrical Engineering of Kyushu University
SN - 1342-3819
IS - 1
ER -