Accelerating boolean satisfiability through application specific processing

Ying Zhao, Sharad Malik, Matthew Moskewicz, Conor Madigan

Research output: Contribution to journalArticle

12 Scopus citations

Abstract

This paper presents our work in developing an application specific multiprocessor system for SAT, utilizing the most recent results such as the development of highly efficient sequential SAT algorithms, the emergence of commercial configurable processor cores and the rapid progress in IC manufacturing techniques. Based on an analysis of the basic SAT search algorithm, we propose a new parallel SAT algorithm that utilizes fine grain parallelism. This is then used to design a multiprocessor architecture in which each processing node consists of a processor and a communication assist node that deals with message processing. Each processor is an application specific processor built from a commercial configurable processor core. All the system configurations are determined based on the characteristics of SAT algorithms, and are supported by simulation results. While this hardware accelerator system does not change the inherent intractability of the SAT problems, it achieves a 30-60x speedup over and above the fastest known SAT solver - Chaff. We believe that this system can be used to expand the practical applicability of SAT in all its application areas.

Original languageEnglish (US)
Pages (from-to)244-249
Number of pages6
JournalProceedings of the International Symposium on System Synthesis
DOIs
StatePublished - Jan 1 2001

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture

Keywords

  • Application specific
  • Boolean satisfiability
  • Configurable processor core
  • Multiprocessor

Fingerprint Dive into the research topics of 'Accelerating boolean satisfiability through application specific processing'. Together they form a unique fingerprint.

  • Cite this