TY - GEN

T1 - Solving satisfiability problems using field programmable gate arrays

T2 - 2nd International Conference on Principles and Practice of Constraint Programming, CP 1996

AU - Yokoo, Makoto

AU - Suyama, Takayuki

AU - Sawada, Hiroshi

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

PY - 1996

Y1 - 1996

N2 - This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints 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. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.

AB - This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints 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. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.

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

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

U2 - 10.1007/3-540-61551-2_96

DO - 10.1007/3-540-61551-2_96

M3 - Conference contribution

AN - SCOPUS:84957874566

SN - 3540615512

SN - 9783540615514

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

SP - 491

EP - 509

BT - Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings

A2 - Freuder, Eugene C.

PB - Springer Verlag

Y2 - 19 August 1996 through 22 August 1996

ER -