47 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
EditorsKenneth L. Pocek, Jeffrey M. Arnold
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1-10
Number of pages10
ISBN (Electronic)0818689005, 9780818689000
DOIs
StatePublished - 1998
Event1998 IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998 - Napa Valley, United States
Duration: Apr 15 1998Apr 17 1998

Publication series

NameProceedings - IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
Volume1998-April

Other

Other1998 IEEE Symposium on FPGAs for Custom Computing Machines, FCCM 1998
Country/TerritoryUnited States
CityNapa Valley
Period4/15/984/17/98

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Software

Fingerprint

Dive into the research topics of 'Accelerating Boolean satisfiability with configurable hardware'. Together they form a unique fingerprint.

Cite this