@inproceedings{f5b7dfdb59b54b3693c7cd421f32649a,
title = "Accelerating Boolean satisfiability with configurable hardware",
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.",
author = "Peixin Zhong and Martonosi, {Margaret Rose} and P. Ashar and Sharad Malik",
note = "Publisher Copyright: {\textcopyright} 1998 IEEE.; 1998 IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998 ; Conference date: 15-04-1998 Through 17-04-1998",
year = "1998",
doi = "10.1109/FPGA.1998.707896",
language = "English (US)",
series = "Proceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "1--10",
editor = "Pocek, {Kenneth L.} and Arnold, {Jeffrey M.}",
booktitle = "Proceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998",
address = "United States",
}