|
A Satisfiability Solver Using Reconfigurable Hardware and
Virtual Logic
Abstract
We present the architecture of a new SAT solver using reconfigurable logic
and a virtual logic scheme. Our main contributions include new forms of
massive fine-grain parallelism, structured design techniques based on
iterative logic arrays that reduce compilation times from hours to a few
minutes, and a decomposition technique that creates independent subproblems
that may be concurrently solved by unconnected FPGAs. The decomposition
technique is the basis of the virtual logic scheme, as it allows solving
problems that exceed the available hardware capacity. Our architecture is
easily scalable. Our results show several orders of magnitude speed-up
compared with a state-of-the-art software implementation, and also with
respect to prior SAT solvers using reconfigurable hardware.
(joint work with Jose de Sousa)
|
