Acceleration of satisfiability algorithms by reconfigurable hardware

Abstract

We present different architectures to solve Boolean satisfiability problems in instance-specific hardware. A simulation of these architectures shows that for examples from the DIMACS benchmark suite, high raw speed-ups over software can be achieved. We present a design tool flow and prototype implementation of an instance-specific satisfiability solver and discuss experimental results. We measure the overall speed-up of the instance-specific architecture that takes the hardware compilation time into account. The results prove that many of the DIMACS examples can be accelerated with current FPGA technology.