Hybrid solvers for the Boolean Satisfiability problem: an exploration

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.

Name thesis:degree_name

M.S. Computer Science

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Year dc:date.available

2012

Author dc:creator

• Nelson, Nicole

Contributors dc:contributor

• Lobo, Andrea

• NP-complete problems
• Computer Sciences

Repository record dc:identifier

https://rdw.rowan.edu/etd/239

OAI identifier oai:identifier

oai:rdw.rowan.edu:etd-1238