FPGA-Based Hardware Acceleration for Boolean Satisfiability Academic Article

abstract

• We present an FPGA-based hardware solution to the Boolean satisfiability (SAT) problem, with the main goals of scalability and speedup. In our approach the traversal of the implication graph as well as conflict clause generation are performed in hardware, in parallel. The experimental results and their analysis, along with the performance models are discussed. We show that an order of magnitude improvement in runtime can be obtained over MiniSAT (the best-in-class software based approach) by using a Virtex-4 (XC4VFX140) FPGA device. The resulting system can handle instances with as many as 10K variables and 280K clauses.

authors

• Khatri, Sunil

published proceedings

• ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS

altmetric score

• 3

author list (cited authors)

• Gulati, K., Paul, S., Khatri, S. P., Patil, S., & Jas, A.

citation count

• 17

complete list of authors

• Gulati, Kanupriya||Paul, Suganth||Khatri, Sunil P||Patil, Srinivas||Jas, Abhijit

publication date

• March 2009

publisher

• Association for Computing Machinery (ACM)  Publisher

published in

• ACM Transactions on Design Automation of Electronic Systems  Journal

keywords

• Algorithms
• Boolean Constant Propagation (bcp)
• Boolean Satisfiabilty (sat)
• Conflict Induced Clauses
• Design
• Fpga
• Non-chronological Backtrack
• Performance

Digital Object Identifier (DOI)

• 10.1145/1497561.1497576

start page

• 33

end page

• 11

volume

• 14

issue

• 2

URL

• http%3A%2F%2Fdx.doi.org%2F10.1145%2F1497561.1497576