Implementing a model-generation theorem prover on an FPGA

Hiroshi Fujita, Atsushi Kawano, Ryuzo Hasegawa

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)13-18
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Volume9
Issue number1
Publication statusPublished - Mar 1 2004

Fingerprint

Field programmable gate arrays (FPGA)
Networks (circuits)
Acoustic waves
Hardware

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 journalArticle

@article{ac2012d8d76646429f702d808122931a,
title = "Implementing a model-generation theorem prover on an FPGA",
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.",
author = "Hiroshi Fujita and Atsushi Kawano and Ryuzo Hasegawa",
year = "2004",
month = "3",
day = "1",
language = "English",
volume = "9",
pages = "13--18",
journal = "Research Reports on Information Science and Electrical Engineering of Kyushu University",
issn = "1342-3819",
publisher = "Kyushu University, Faculty of Science",
number = "1",

}

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 -