Nicole Nelson

Date Approved

12-12-2012

Embargo Period

3-3-2020

Document Type

Thesis

Degree Name

M.S. Computer Science

Department

Computer Science

College

College of Science & Mathematics

Advisor

Lobo, Andrea

Subject(s)

NP-complete problems

Disciplines

Computer Sciences

Abstract

The Boolean Satisfiability problem (SAT) is one of the most extensively researched NP-complete problems in Computer Science. This thesis focuses on the design of feasible solvers for this problem. A SAT problem instance is a formula in propositional logic. A SAT solver attempts to find a solution for the formula. Our research focuses on a newer solver paradigm, hybrid solvers, where two solvers are combined in order to gain the benefits from both solvers in the search for a solution. Our hybrid solver, AmbSAT, combines two well-known solvers: the systematic Davis-Putnam-Logemann-Loveland solver (DPLL) and the stochastic WalkSAT solver. AmbSAT's design is original and differs from the hybrid solver designs in the research literature. AmbSAT utilizes a DPLL algorithm to lead the search and WalkSAT at appropriate points to aid in the search process. Central to AmbSAT's design is the notion of ambivalence. Essentially, ambivalence attempts to formally identify the points in time when the DPLL solver might be well served by further guidance from WalkSAT. In this thesis, we present three different ambivalence notions and analyze their performance against a pure DPLL solver. Our results are promising, and indicate that AmbSAT performs better than a pure DPLL solver on a diverse collection of SAT problem instances.

Download

Share

COinS