Solving Satisfiability Problems Using Reconfigurable Computing
Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada, and Akira Nagoya
IEEE Transactions On Very Large Scale Integration (VLSI), (to
appear)
This paper reports on an innovative approach for solving
satisfiability problems for propositional formulas in conjunctive
normal form (SAT) by creating a logic circuit that is specialized to
solve each problem instance on Field Programmable Gate Arrays (FPGAs).
This approach has become feasible due to recent advances in
Reconfigurable Computing and has opened up an exciting new research
field in algorithm design. SAT is an important subclass of constraint
satisfaction problems, which can formalize a wide range of application
problems.
We have developed a series of algorithms that are suitable for a logic
circuit implementation, including an algorithm whose performance is
equivalent to the Davis-Putnam procedure with powerful dynamic
variable ordering. Simulation results show that this method can solve
a hard random 3-SAT problem with 400 variables within 1.6 minutes at a
clock rate of 10MHz. Faster speeds can be obtained by increasing the
clock rate. Furthermore, we have actually implemented a 128-variable,
256-clause problem instance on FPGAs.