SAT-Accel: A Modern SAT Solver on a FPGA
Michael Lo, Mau-Chung Frank Chang, Jason Cong
Abstract
Boolean satisfiability (SAT) solving is the first known NP-complete problem and is widely used in many application domains. Over the years, there have been so many consistent improvements in this area such that larger instances can be solved relatively quickly. Although these improvements have found their way onto CPU implementations, there has been limited progress adopting this on hardware accelerators mainly because it is difficult to implement the dynamic data structures needed to support a modern SAT solving algorithm.
Topics & Concepts
Computer scienceField-programmable gate arrayParallel computingProgramming languageComputer architectureEmbedded systemFormal Methods in VerificationLogic, programming, and type systemsModel-Driven Software Engineering Techniques