Accelerating Boolean satisfiability with configurable hardware
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 186-195
- https://doi.org/10.1109/fpga.1998.707896
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 communitiesKeywords
This publication has 11 references indexed in Scilit:
- Virtual wires: overcoming pin limitations in FPGA-based logic emulatorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Using reconfigurable computing techniques to accelerate problems in the CAD domainPublished by Association for Computing Machinery (ACM) ,1998
- Satisfiability on reconfigurable hardwarePublished by Springer Nature ,1997
- Architectural and physical design challenges for one-million gate FPGAs and beyondPublished by Association for Computing Machinery (ACM) ,1997
- Solving graph problems with dynamic computation structuresPublished by SPIE-Intl Soc Optical Eng ,1996
- Programmable active memories: reconfigurable systems come of ageIEEE Transactions on Very Large Scale Integration (VLSI) Systems, 1996
- A transitive closure algorithm for test generationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1993
- Test pattern generation using Boolean satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992
- An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic CircuitsIEEE Transactions on Computers, 1981
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960