Using configurable computing to accelerate Boolean satisfiability

The issues of software compute time and complexity are very important in cu rrent computer-aided design (CAD) tools. As field-programmable gate array ( FPGA) speeds and densities increase, the opportunity for effective hardware accelerators built from FPGA technology has opened up. This paper describe s and evaluates a formula-specific method for implementing Boolean satisfia bility solver circuits in configurable hardware. That is, using a template generator, we create circuits specific to the problem instance to be solved . This approach yields impressive runtime speedups of up to several hundred times compared to the software approaches. The high performance comes from realizing fine-grained parallelism inherent in the clause evaluation and i mplication and from direct mapping of Boolean relations into logic gates. O ur implementation uses a commercially available hardware system for proof o f concept. This system yields more than 100 times run-time speedup on many problems, even though the clock rate of the hardware is 100 times slow er t han that of the workstation running the software solver. While the time to compile the solver circuit to configurable hardware can be quite long on cu rrent platforms (20-40 min per chip), this paper discusses new approaches t o overcome this compilation overhead. More broadly, we view this work as a case study in the burgeoning domain of high performance configurable comput ing. Our approach realizes large amount of fine-grained parallelism, and ha s broad applications in the very large scale integration CAD area.