Accelerating boolean satisfiability through application specific processing

Ying Zhao, Sharad Malik, Matthew Moskewicz, Conor Madigan

Research output: Contribution to journalArticlepeer-review

17 Scopus citations


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
StatePublished - 2001

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture


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


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

Cite this