### Solving Satisfiability Problems on FPGAs using Experimental
Unit Propagation

Takayuki Suyama, Makoto Yokoo, Akira Nagoya

Fifth International
Conference on Principles and Practice of Constraint Programming (CP-99),
1999.

This paper presents new results on an innovative approach for solving
satisfiability problems (SAT), that is, 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.
We have developed an algorithm that is suitable for a logic circuit
implementation. This algorithm is basically equivalent to the
Davis-Putnam procedure with Experimental Unit Propagation. The
algorithm requires fewer hardware resources than previous
approaches.
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.