FPGA-Based SAT Solver

Several approaches have been proposed to accelerate the NP-complete Boolean Satisfiability problem (SAT) using reconfigurable computing. We present an FPGA based clause evaluator, where each clause is modeled as a shift register that is either right shifted, left shifted, or standstill according to whether the current assigned variable value satisfy, unsatisfy, or does not effect the clause, respectively. For a given problem instance, the effect of the value of each of its variables on its SAT formula is loaded in the FPGA on-chip memory. This results in less configuration effort and fewer hardware resources than other available SAT solvers. Also, we present a new approach for implementing conflict analysis based on a conflicting variables accumulator and priority encoder to determine backtrack level. Using these two new ideas, we implement an FPGA based SAT solver performing depth-first search with nonchronological conflict directed backtracking. We compare our SAT solver with other ...

• Type: Conference
• Year: 2006
• Where: CCECE
• Authors: Mona Safar, M. Watheq El-Kharashi, Ashraf Salem
• Keywords: Available Sat Solvers, CCECE 2006, Electrical And Computer Engineering, FPGA Based Clause, Sat Solver