A Satisfiability Solver Using Reconfigurable Hardware and Virtual Logic


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)

You are not logged in 
©2002-2017 U.C. Regents