<紀要論文>
定理証明系PCMGTPのFPGA上の実装について

作成者
本文言語
出版者
発行日
収録物名
開始ページ
終了ページ
出版タイプ
アクセス権
JaLC DOI
関連情報
概要 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.続きを見る

本文ファイル

p013 pdf 818 KB 106  

詳細

PISSN
EISSN
NCID
レコードID
査読有無
主題
登録日 2015.06.04
更新日 2020.11.02

この資料を見た人はこんな資料も見ています