Title :
Accelerating Boolean satisfiability with configurable hardware
Author :
Zhong, Peixin ; Martonosi, Margaret ; Ashar, Pranav ; Malik, Sharad
Author_Institution :
Dept. of Electr. Eng., Princeton Univ., NJ, USA
Abstract :
This paper describes and evaluates methods for implementing formula-specific Boolean satisfiability (SAT) solver circuits in configurable hardware. Starting from a general template design, our approach automatically generates VHDL for a circuit that is specific to the particular Boolean formula being solved. Such an approach tightly customizes the circuit to a particular problem instance. Thus, it represents an ideal use for dynamically-reconfigurable hardware, since it would be impractical to fabricate an ASIC for each Boolean formula being solved. Our approach also takes advantage of direct gate mappings and large degrees of fine-grained parallelism in the algorithm´s Boolean logic evaluations. We compile our designs to two hardware targets: an IKOS logic emulation system, and Digital SRC´s Pamette configurable computing board. Performance evaluations on the DIMACS SAT benchmark suite indicate that our approach offers speedups from 17X to more than a thousand times. Overall, this SAT solver demonstrates promising performance speedups on an important and complex problem with extensive applications in the CAD and AI communities
Keywords :
Boolean functions; computability; field programmable gate arrays; hardware description languages; performance evaluation; ASIC; Boolean logic evaluations; Boolean satisfiability; DIMACS SAT benchmark suite; Digital SRC´s Pamette configurable computing board; IKOS logic emulation system; VHDL; configurable hardware; direct gate mappings; dynamically-reconfigurable hardware; general template design; performance evaluations; Acceleration; Application software; Application specific integrated circuits; Artificial intelligence; Boolean functions; Computer applications; Field programmable gate arrays; Hardware; Logic design; National electric code;
Conference_Titel :
FPGAs for Custom Computing Machines, 1998. Proceedings. IEEE Symposium on
Conference_Location :
Napa Valley, CA
Print_ISBN :
0-8186-8900-5
DOI :
10.1109/FPGA.1998.707896