الفهرس 
CoverOnly 14 pages are availabe for public view
 |  | from | 131 |  |  |
| | | from | 131 | | |
Abstract
The Boolean Satisfiability problem (SAT) is a central problem in artificial intelligence,
mathematical logic, and computing theory with wide range of practical applications in
Electronic Design Automation. Several approaches have been proposed to accelerate the
NP-complete SAT using reconfigurable computing. Much of the performance improvement
achieved by state-of-the-art software SAT solvers is related to the implementation of
conflict analysis, which enables the solver to perform non-chronological backtracking and
conflict driven learning. Such advanced techniques have been ignored by the majority of
hardware SAT solvers or are executed on some coupled software running on an attached
host processor.
In this thesis, we propose a new conflict directed search algorithm, best suited for a
reconfigurable hardware implementation. The algorithm performs conflict analysis and
hence nonchronological backtracking. The algorithm enables learning without explicit new
clauses addition avoiding consumption of new hardware resources.
We present a pipelined SAT solver in which the execution of the proposed algorithm is
divided into five stages with all stages executed in hardware without any communication
with a host processor. The pipelined architecture provides significant speedup while retaining
the same clock frequency of an equivalent non-pipelined implementation. Performance
is improved by increasing the throughput of assigning SAT variables while evaluating and
checking the validity of the formula with each new variable assignment. All possible data
and control hazards are handled.
For different SAT problem instances, SAT instance’s specific data is stored only in
memory modules. A memory module stores the instance’s clauses and another memory
module stores the effect of the assignment of each of the instance’s variables on the clauses.
No instance-specific circuit is employed. Mapping different SAT problem instances into
the proposed reconfigurable SAT solver requires only reloading those memory modules
eliminating compilation, synthesis, and place-and-route overhead. This enables achieving
real speedup compared to current state-of-the-art software SAT solvers.
Finally, we presented a new approach for certifying the solver’s output. Based on the
latest explored search space and the last encountered conflict clauses, the solver produces a
refutation proof assuring that no non-redundant search space has been erroneously pruned
iii
and that no hardware malfunction has occurred.
We compared our SAT solver with other hardware SAT solvers through instances from
DIMACS benchmarks suite. The simplicity of our architecture enables achieving higher
clock rates and fewer resources utilization