Please use this identifier to cite or link to this item:
Title: Distributed SAT solving engine
Keywords: Boolean Satisfiability Problem, Distributed Systems, Constraint Programming, Combinatorial Optimization
Issue Date: 15-Aug-2011
Citation: MAI DANG QUANG HUNG (2011-08-15). Distributed SAT solving engine. ScholarBank@NUS Repository.
Abstract: The boolean satisfiability problem (SAT) is one of the typical NP-complete problems that have found considerable industrial applications in the past decades. Significant theoretical and practical efforts has been devoted to the research in this particular problem. Recently, with the major architectural shift from increasing processor power to increasing number of processors, and the development of cloud computing, there is an emerging need to paral- lelize these solvers to run on a loose distributed system where minimal synchronization and communication overhead is desirable. It is an important challenge to improve performance when the number of processors increase. Moreover, the parallel solver should be able to scale accordingly when the number of processors is significant. In this report, we first present multiple aspects of the algorithm implemented in modern state-of-the-art solvers and advances in parallel SAT solving. Based on the analysis of cur- rent research, we then propose optimizations on splitting strategies aimed for the distributed environment. A protocol of sharing relevant information between processes was also designed and implemented using the hybrid of Message Passing Interface (MPI) and POSIX threads. Moreover, two different approaches on load balancing on long-running jobs are proposed and implemented. Experimental data show that we can achieve good speedup and scalabil- ity by combining the new communication protocol combined with improved strategies and heuristics.
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
MaiDQH.pdf631.53 kBAdobe PDF



Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.