Boolean Satisfiability. Creating Solvers Optimized for Specific Problem Instances.

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

The Boolean satisfiability problem is well-known in computer science. Given a Boolean formula, the goal is to find an assignment to the variables so that the formula evaluates to true or 1, or to prove that such an assignment does not exist. It has many applications, including theorem proving, automatic test pattern generation, and formal verification. Boolean satisfiability (SAT) is a classic NP-complete problem with a broad range of applications. There are many projects that use reconfigurable computing to solve it. This chapter presents a review of the subject with emphasis on a particular approach that employs a backtrack search algorithm and generates solver hardware according to the problem instance. This approach uses the reconfigurability and fine-grained parallelism provided by field-programmable gate arrays (FPGAs). This chapter introduces the SAT formulation and applications. It describes the algorithms to solve the SAT problem and describes in detail two SAT solvers that use reconfigurable computing. Many projects have designed Boolean satisfiability solvers with reconfigurable computing. These projects demonstrate the performance potential of these solvers through fine-grained custom hardware and massively parallel processing. Significant progress has been made in software algorithms as well, and recently, reconfigurable computing solutions have not kept up in incorporating these innovations. This is partly because the tools for reconfigurable computing are not yet mature.

Original languageEnglish (US)
Title of host publicationReconfigurable Computing
PublisherElsevier Inc.
Pages613-636
Number of pages24
ISBN (Print)9780123705228
DOIs
StatePublished - Dec 1 2008

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Boolean Satisfiability. Creating Solvers Optimized for Specific Problem Instances.'. Together they form a unique fingerprint.

  • Cite this