{"id":{"repo_id":"nus","oai_identifier":"oai:scholarbank.nus.edu.sg:10635/30691"},"canonical_url":"https://search.dev.ndltd.org/etd/nus/oai:scholarbank.nus.edu.sg:10635/30691","repository":{"repo_id":"nus","name":"National University of Singapore","base_url":"https://scholarbank.nus.edu.sg/oai/request"},"display":{"title":"Distributed SAT solving engine","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.","abstract_html":"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.","abstract_has_math":false,"creators":["MAI DANG QUANG HUNG"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-08-15","date_published":"2011-08-15","updated_at":"2026-07-24T03:33:34Z","subjects":["Boolean Satisfiability Problem, Distributed Systems, Constraint Programming, Combinatorial Optimization"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["MAI DANG QUANG HUNG"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2011-08-15"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://scholarbank.nus.edu.sg/handle/10635/30691"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Boolean Satisfiability Problem, Distributed Systems, Constraint Programming, Combinatorial Optimization"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://scholarbank.nus.edu.sg/bitstreams/e49e89d1-3f3e-44f8-b78d-8dea225692c6/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["e5e39dc5ad1f9b818e23a65498707a27","2173d36c5e5be97830495e3c5a953c53"]},{"key":"dc:title","label":"Title","values":["Distributed SAT solving engine"]}]}],"canonical_facts":{"dc:creator":["MAI DANG QUANG HUNG"],"dc:date.issued":["2011-08-15"],"dc:description.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."],"dc:format.checksum.md5":["e5e39dc5ad1f9b818e23a65498707a27","2173d36c5e5be97830495e3c5a953c53"],"dc:identifier.uri":["https://scholarbank.nus.edu.sg/bitstreams/e49e89d1-3f3e-44f8-b78d-8dea225692c6/download"],"dc:relation.isreferencedby":["https://scholarbank.nus.edu.sg/handle/10635/30691"],"dc:subject":["Boolean Satisfiability Problem, Distributed Systems, Constraint Programming, Combinatorial Optimization"],"dc:title":["Distributed SAT solving engine"],"dc:type":["Thesis"]},"updated_at":"2026-07-24T03:33:34Z"}