Sciweavers

CCECE
2006
IEEE

FPGA-Based SAT Solver

13 years 9 months ago
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 ...
Mona Safar, M. Watheq El-Kharashi, Ashraf Salem
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where CCECE
Authors Mona Safar, M. Watheq El-Kharashi, Ashraf Salem
Comments (0)