Abstract
This paper presents new parallel strategies for preprocessing and solving the issue of Boolean Satisfaction (SAT) on Heterogeneous systems of multicore and many-core CPU and Graphics Processing Unit (GPU) using Open Multi-Processor (OpenMP) and NVIDIA - CUDA. We propose exceptionally proficient and parallel techniques for SAT simplifications using the variable elimination method based on the Davis-Putnam-Logemann-Loveland (DPLL) slitting rule algorithm performed with a shared-memory model on a multicore CPU platform, where the clause elimination subsumption and the pure-literal removal techniques are completely performed on the CUDA framework. We demonstrate how efficient an evolutionary SAT solver is by using the suggested heterogeneous pre-processing, leading to important acceleration improvements in the solution's quality enhancement. The penalization of the transformative SAT solver is executed with Ant Colony Optimization (ACO) scheme utilizing CUDA. (Compute Unified Device Architecture) We perform thorough benchmarks to test the performance of our preprocessor and solver implementations against various random SAT formulas. The promoted H-SAT pre-processor scheme has gotten a speed-up of a factor 15x over the sequential implementation with statistical reductions on the original CNF which becomes up to 49% and 43% in case of literals and clauses numbers exclusively, where the H-SAT gain strength the solvability of the ACO solver by 100% in some cases.