Solving boolean satisfiability with dynamic hardware configurations

Peixin Zhong, Margaret Rose Martonosi, Pranav Ashar, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Scopus citations

Abstract

Boolean satisfiability (SAT) is a core computer science problem with many important commercial applications. An NP-complete problem, many different approaches for accelerating SAT either in hardware or software have been proposed. In particular, our prior work studied mechanisms for accelerating SAT using configurable hardware to implement formula-specific solver circuits. In spite of this progress, SAT solver runtimes still show room for further improvement. In this paper, we discuss further improvements to configurable-hardware-based SAT solvers. We discuss how dynamic techniques can be used to add the new solver circuitry to the hardware during run-time. By examining the basic solver structure, we explore how it can be best designed to support such dynamic reconfiguration techniques. These approaches lead to several hundred times speedups for many problems. Overall, this work offers a concrete example of how aggressively employing on-the-fly reconfigurability can enable runtime learning processes in hardware. As such, this work opens new opportunities for high performance computing using dynamically reconfigurable hardware.

Original languageEnglish (US)
Title of host publicationField-Programmable Logic and Applications
Subtitle of host publicationFrom FPGAs to Computing Paradigm - 8th International Workshop, FPL 1998, Proceedings
PublisherSpringer Verlag
Pages326-335
Number of pages10
ISBN (Print)3540649484, 9783540649489
StatePublished - Jan 1 1998
Event8th International Workshop on Field-Programmable Logic and Applications, FPL 1998 - Tallinn, Estonia
Duration: Aug 31 1998Sep 3 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1482
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Workshop on Field-Programmable Logic and Applications, FPL 1998
CountryEstonia
CityTallinn
Period8/31/989/3/98

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solving boolean satisfiability with dynamic hardware configurations'. Together they form a unique fingerprint.

  • Cite this

    Zhong, P., Martonosi, M. R., Ashar, P., & Malik, S. (1998). Solving boolean satisfiability with dynamic hardware configurations. In Field-Programmable Logic and Applications: From FPGAs to Computing Paradigm - 8th International Workshop, FPL 1998, Proceedings (pp. 326-335). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1482). Springer Verlag.