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.