الفهرس 
Boolean SatisfiabilityOnly 14 pages are availabe for public view
 |  | from | 116 |  |  |
| | | from | 116 | | |
Abstract
The Boolean satisfiability (SAT) problem is a very popular problem in computer science. The importance of the problem came from the fact that it is the first problem proven to be NP-complete by Cook in 1971. Nevertheless, SAT solvers are successfully used in several practical applications.
With the advances of multicore processors, parallel SAT solvers have witnessed a significant improvement. Thus, in 2008 a specialized track for parallel SAT solvers was added to the SAT competition. However, the need for optimized sequential SAT solvers is still present and adapting it to cope with the parallel nature is necessary.
In this thesis, we propose a new unorthodox cooperative algorithm for solving satisfiable SAT instances in parallel. We propose a simple yet effective approach that is mainly clause oriented. Our proposed clause oriented algorithm takes full advantage of the parallel nature paradigm.
The most important trait of our algorithm is that it adapts to the parallel temper. This adaptation comes from the fact that our approach scales with the formula clauses since the formula is divided to a number of clauses that are processed in parallel. In addition, our algorithm depends only on an independent metric which is the cardinality of the coverage set of the formula clauses that does not require the sharing of clauses between parallel processing units. This feature provides our algorithm with not only scalability but also saving the communication cost and memory consumption which is one of the most important challenges in parallelism. Moreover, our proposed approach provides a natural balanced workload distribution.
Unlike other algorithms, our algorithm does not depend on the Boolean constraint propagation problem which is a P-complete problem that is hard to parallelize. Our algorithm is generic and can be implemented on top of any parallel SAT solver as a base solver. This is due to its simplicity and independence of the original algorithm since it only depends on the formula clauses.
We compared our proposed clause oriented algorithm with parallel and sequential SAT solvers through instances from various benchmarks.