Exploits in Concurrency for Boolean Satisfiability

dc.contributor.authorSohanghpurwala, Ali Asgar Ali Akbaren
dc.contributor.committeechairAthanas, Peter M.en
dc.contributor.committeememberPatterson, Cameron D.en
dc.contributor.committeememberJones, Mark T.en
dc.contributor.committeememberHuang, Berten
dc.contributor.committeememberHsiao, Michael S.en
dc.contributor.departmentElectrical and Computer Engineeringen
dc.date.accessioned2018-12-15T09:00:21Zen
dc.date.available2018-12-15T09:00:21Zen
dc.date.issued2018-12-14en
dc.description.abstractBoolean Satisfiability (SAT) is a problem that holds great theoretical significance along with effective formulations that benefit many real-world applications. While the general problem is NP-complete, advanced solver algorithms and heuristics allow for fast solutions to many large industrial problems. In addition to SAT, many applications rely on generalizations of Satisfiability such as MaxSAT, and Satisfiability Modulo Theories (SMT). Much of the advancement in SAT solver performance has been in the realm of improved sequential solvers with advanced conflict resolution, learning mechanisms, and sophisticated heuristics. There have been some successful demonstrations of massively parallel and hardware-accelerated solvers for SAT, but these have failed to find their way into mainstream usage. This document first presents previous work in Hardware Acceleration of Satisfiability followed by an analysis of why these attempts failed to gain widespread acceptance. It then demonstrates an alternative, hardware-centric approach, based on distributed Stochastic Local Search (SLS) that is better suited to efficient hardware implementation. Then a parallel SLS/CDCL hybrid approach is proposed that is suitable for distributed search with minimal communication overhead while maintaining completeness. Finally the efficacy and flexibility of distributed local search is considered with an adaptation to Weighted Partial MaxSAT (WPMS) and a focused case study on converted Probabilistic Inference instances.en
dc.description.abstractgeneralThe Boolean Satisfiability (SAT) problem is an important decision problem that asks whether there exists a solution that satisfies all given constraints over a set of variables that can assume values of either 0 or 1. May real-world decision problems can be translated into SAT, and there exist efficient sequential solvers that can quickly resolve many such instances. Less progress has been made in efficiently scaling SAT solvers to modern multi-core systems and massively parallel hardware accelerators such as GPUs and Field Programmable Gate Arrays (FPGAs). This thesis explore different approaches to solving SAT based decision and optimization problems with the goal of increasing concurrency.en
dc.description.degreePh. D.en
dc.format.mediumETDen
dc.identifier.othervt_gsexam:16971en
dc.identifier.urihttp://hdl.handle.net/10919/86417en
dc.publisherVirginia Techen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectSatisfiabilityen
dc.subjectField programmable gate arraysen
dc.subjectSLSen
dc.subjectMaxSATen
dc.subjectParallel Local Searchen
dc.subjectSATen
dc.titleExploits in Concurrency for Boolean Satisfiabilityen
dc.typeDissertationen
thesis.degree.disciplineComputer Engineeringen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Sohanghpurwala_AA_D_2018.pdf
Size:
745.55 KB
Format:
Adobe Portable Document Format