Abstract
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.
Degree
thesis:*- Name thesis:degree_name
- Ph. D.
- Level thesis:degree_level
- doctoral
- Discipline thesis:degree_discipline
- Computer Engineering
- Department dc:contributor.department
- Electrical and Computer Engineering
- Grantor dc:publisher
- Virginia Tech
- Year dc:date.issued
- 2018
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Sohanghpurwala, Ali Asgar Ali Akbar
- Chair dc:contributor.committeechair
-
- Athanas, Peter M.
- Committee members dc:contributor.committeemember
-
- Patterson, Cameron D.
- Jones, Mark T.
- Huang, Bert
- Hsiao, Michael S.
Subjects
dc:subject × 6Rights
dc:rights- Statement dc:rights
-
- In Copyright
- Licence dc:rights.uri
Identifiers
dc:identifier.*- Dc Identifier Other
- vt_gsexam:16971
- OAI identifier oai:identifier
- oai:vtechworks.lib.vt.edu:10919/86417