Boolean satisfiability: parallelization and exploration
Date
2015
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
University of Delaware
Abstract
The Boolean Satisfiability Problem (SAT) is a well-known and core problem in computer science. SAT is the problem of determining whether a propositional Boolean formula can be true by assigning truth values to variables. SAT is the first problem proved to be NP-complete, and has been applied in various disciplines, such as artificial intelligence, software/hardware verification, and theorem proving. In the era of parallel computing, it is expected that the extra computational power does not come from higher CPU frequency or deeper ILP, but by having additional processing units being able to run in parallel. In recent years, with the predominance of multi-core processors, parallel SAT solving based on multi-core processors has been an active research area. In this thesis, the SAT solving process is parallelized from a new perspective by using the new abstraction: tao-analysis and amorphous data-parallelism, to exploit the parallelism inside the SAT solving algorithm. This thesis is mainly about parallelizing the SAT solving process, and provides an in-depth exploration of the proposed parallel SAT solving idea. Different branching variable selection heuristics and different learnt clause recording schemes are proposed to serve the parallelization idea better. Experiments show that a maximum speedup of 100X can be reached on selected benchmarks. To further optimize the SAT solving performance, this thesis proposes a hybrid framework; the hybrid framework aims at relaxing certain heuristics. Experiments show that a maximum speedup of 700X can be achieved on selected benchmarks. This thesis also discusses two other SAT related areas; one is about building instance features from a new perspective, and the other applying SAT in a new area — model checking for investment strategies. For instance features, various features are proposed based on the notation of path length in the graph representations of input instances; experiments show that up to 60% performance improvement can be reached on selected instances with the help of the proposed instance features. For SAT in model checking for investment strategies, various models are built and corresponding results are presented; this direction serves as an attempt to explore the possibilities of applying SAT in the finance-related area.