الفهرس Only 14 pages are availabe for public view
 |  | from | 112 |  |  |
| | | from | 112 | | |
Abstract
Reconfigurable computing provides the ability to perform computations in hardware using customized logic functional units to improve performance while retaining much of the flexibility of an equivalent software solution. Several approaches have been proposed to
accelerate NP-complete Boolean Satisfiability problem (SAT) using reconfigurable computing.
SAT is a central problem in artificial intelligence, mathematical logic, and computing theory with wide range of practical applications in Electronic Design Automation.
In this thesis, we present the state-of-the-art in reconfigurable hardware SAT solvers.
We propose 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 current
assigned variable’s value satisfy, unsatisfy,or does not affect 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 application-specific SAT solvers. Also, we
present a new approach for implementing conflict analysis based on a conflicting variables accumulator and priority encoder to determine the backtrack level. Using these two new
ideas, we implement an FPGA-based SAT solver performing depth-first search with nonchronological conflict directed backtracking. We compared our SAT solver with other SAT solvers through instances from DIMACS benchmarks suite. The simplicity of our architecture enables achieving higher clock rates and fewer resources utilization.