Implementing a model-generation theorem prover on an FPGA

Hiroshi Fujita, Atsushi Kawano, Ryuzo Hasegawa

研究成果: Contribution to journalArticle査読


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.

ジャーナルResearch Reports on Information Science and Electrical Engineering of Kyushu University
出版ステータス出版済み - 3 1 2004

All Science Journal Classification (ASJC) codes

  • コンピュータ サイエンス(全般)
  • 電子工学および電気工学


「Implementing a model-generation theorem prover on an FPGA」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。