TY - GEN

T1 - Solving satisfiability problems on FPGAs

AU - Suyama, Takayuki

AU - Yokoo, Makoto

AU - Sawada, Hiroshi

N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

PY - 1996

Y1 - 1996

N2 - This paper presents a report on a new approach for solving satisfiability problems (SAT), i.e., creating a specialized logic circuit to solve each problem instance on Field Programmable Gate Arrays (FP-GAs). Recently, due to advances in FPGA technologies, users can now create their own reconfigurable logic circuits. Furthermore, by using current automatic logic synthesis technologies, users are able to design logic circuits automatically using a high level hardware description language (HDL). The combination of these two technologies have enabled users to rapidly create logic circuits specialized for solving individual problem instances. Satisfiability problems (SAT) were chosen because they make up an important subclass of NP-hard problems. We have developed a new algorithm called parallel-checking, which is suitable for this approach. In the algorithm, all variable values are assigned simultaneously, and all constraints are checked concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs.

AB - This paper presents a report on a new approach for solving satisfiability problems (SAT), i.e., creating a specialized logic circuit to solve each problem instance on Field Programmable Gate Arrays (FP-GAs). Recently, due to advances in FPGA technologies, users can now create their own reconfigurable logic circuits. Furthermore, by using current automatic logic synthesis technologies, users are able to design logic circuits automatically using a high level hardware description language (HDL). The combination of these two technologies have enabled users to rapidly create logic circuits specialized for solving individual problem instances. Satisfiability problems (SAT) were chosen because they make up an important subclass of NP-hard problems. We have developed a new algorithm called parallel-checking, which is suitable for this approach. In the algorithm, all variable values are assigned simultaneously, and all constraints are checked concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs.

UR - http://www.scopus.com/inward/record.url?scp=84955583758&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84955583758&partnerID=8YFLogxK

U2 - 10.1007/3-540-61730-2_14

DO - 10.1007/3-540-61730-2_14

M3 - Conference contribution

AN - SCOPUS:84955583758

SN - 9783540617303

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 136

EP - 145

BT - Field-Programmable Logic

A2 - Hartenstein, Reiner W.

A2 - Glesner, Manfred

PB - Springer Verlag

T2 - 6th International Workshop on Field-Programmable Logic and Applications, FPL 1996

Y2 - 23 September 1996 through 25 September 1996

ER -