الفهرس 
AbstractOnly 14 pages are availabe for public view
 |  | from | 103 |  |  |
| | | from | 103 | | |
Abstract
This thesis describes efficient parallel implementations of exploratory algorithms of unit propagation (UP) technique for developing Boolean Satisfiability solving. The recent enhancements in Boolean Satisfiability solving have made satisfiability (SAT) solvers a core engine for many real world applications especially for Automatic Test Pattern Generation (ATPG) for digital circuits. The majority of solving time is spent on iteratively propagating variable assignments that are inferred by decisions, so the Unit Propagation (UP) is the most significant part in the Satisfiability problem. Parallelization of unit propagation in SAT solvers is a compelling way of obtaining an efficient procedure for the propositional satisfiability problem. In addition, it describes an efficient algorithm of SAT solver engine on GPU (SSGPU) which is based on the Davis Putnam Logemann and Loveland (DPLL) SAT solver for developing the minimal correction subsets (MCSes) computation that can be exploited in SAT based ATPG application. Also, it demonstrates a developed technique (𝐹𝑖𝑛𝑑_𝐴𝑙𝑙𝑀𝐶𝑆es) for computing MCSes that can reduce time consumed in detecting faults existed in VLSI digital circuits. The proposed parallel versions of UP technique and SSGPU solver utilize the NVidia Compute Unified Device Architecture (CUDA), one of the most popular platforms for GPU computing. Our thesis presents experimental results for two different UP design approaches, SSGPU solver design and MCSes computation algorithm using a C++ algorithm (SAT encoder) for generating a 3D SAT-based formula of VLSI digital circuits from random, ISCAS’85, ISCAS’89, ITC’99 and Synthetic benchmarks. The outcomes demonstrate the potential for the UP and the proposed SAT engine (SSGPU) approaches, leading to high execution performance using a simple NVIDIA platform. Both UP parallel algorithms have achieved speeds up to 1.88x and 2.13x correspondingly using ISCAS’85 benchmark in comparison to previously published results. Furthermore, using random benchmark, the speeds that have been achieved by both proposed UP algorithms are up to 2.74x and 1.9x respectively compared to their counterpart. For the proposed scheme of SSGPU solver, it has achieved speed up to 200x in comparison to the conventional parallel DPLL SAT solver results. The proposed 𝐹𝑖𝑛𝑑_𝐴𝑙𝑙𝑀𝐶Ses algorithm of computing 𝑀𝐶𝑆𝑒𝑠 in the use of our developed parallel solver achieves speedup to 1.35x in comparison to the conventional parallel solver.