Solving satisfiability problems using reconfigurable computing

摘要

This paper reports on an innovative approach for solvingnsatisfiability problems for propositional formulas in conjunctive normalnform (SAT) by creating a logic circuit that is specialized to solve eachnproblem instance on field programmable gate arrays (FPGAs). Thisnapproach has become feasible due to recent advances in reconfigurablencomputing and has opened up an exciting new research field in algorithmndesign. SAT is an important subclass of constraint satisfactionnproblems, which can formalize a wide range of application problems. Wenhave developed a series of algorithms that are suitable for a logicncircuit implementation, including an algorithm whose performance isnequivalent to the Davis-Putnam procedure with powerful dynamic variablenordering. Simulation results show that this method can solve a hardnrandom 3-SAT problem with 400 variables within 1.6 min at a clock ratenof 10 MHz. Faster speeds can be obtained by increasing the clock rate.nFurthermore, we have actually implemented a 128-variable 256-clausenproblem instance on FPGAs