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.
|Number of pages||6|
|Journal||Research Reports on Information Science and Electrical Engineering of Kyushu University|
|Publication status||Published - Sep 1 2006|
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Electrical and Electronic Engineering