الفهرس 
IntroductionOnly 14 pages are availabe for public view
 |  | from | 104 |  |  |
| | | from | 104 | | |
Abstract
This thesis describes the design and implementation of an efficient exploratory algorithm with preprocessing for the Boolean satisfiability (SAT) problem executed on heterogeneous systems. The algorithm is the Ant Colony Optimization (ACO) which is based on the incomplete approaches for solving SAT problems implemented entirely on Graphics Processing Unit (GPU) using NVIDIA Compute Unified Device Architecture (CUDA).
The SAT formulas derived from digital hardware circuits are simplified using a proposed highly optimized parallel SAT preprocessor implemented on both multicore CPU and the many-core GPU providing different techniques for simplifications.
The thesis provides experimental results for the parallel execution of the Ant Colony SAT solver on GPU for various random SAT instances with and without preprocessor. Also we present benchmarks of executing the heterogeneous SAT preprocessor on both CPU and GPU for a plenty of industrial applications such as fault diagnosis, automatic test program generation, and formal verification.