A preprocessing method for the SAT solver PCMGTP on FPGA

Junichi Matsuda, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa

Research output: Contribution to journalArticlepeer-review


This paper describes a preprocessing method for the SAT solver PCMGTP implemented on an FPGA chip. In PCMGTP, each problem is transformed into an HDL code so as to solve the problem directly on an FPGA. It is time consuming to compile an HDL code to a hardware circuit for the FPGA, while its deduction is at speed. Preprocessing SAT problems can sometimes reduce their search space and size considerably. Applying the preprocessing method to SAT problems not only decreases runtime for solving them, but also reduces their circuit size and compilation time. Experimental results show significant performance in solving some benchmark SAT problems.

Original languageEnglish
Pages (from-to)109-114
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number2
Publication statusPublished - Sept 2006

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • Electrical and Electronic Engineering


Dive into the research topics of 'A preprocessing method for the SAT solver PCMGTP on FPGA'. Together they form a unique fingerprint.

Cite this