الفهرس 
Boolean SatisfiabilityOnly 14 pages are availabe for public view
 |  | from | 130 |  |  |
| | | from | 130 | | |
Abstract
econfigurable 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 comput-
ing. 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 confiict 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
confiict directed bad-tracking. 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.