Solving Satisfiability Problems using Field Programmable Gate Arrays: First Results
Makoto Yokoo, Takayuki Suyama, Hiroshi Sawada
Second International
Conference on Principles and Practice of Constraint Programming (CP-96),
1996.
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.