{"id":{"repo_id":"rowan","oai_identifier":"oai:rdw.rowan.edu:etd-1238"},"canonical_url":"https://search.dev.ndltd.org/etd/rowan/oai:rdw.rowan.edu:etd-1238","repository":{"repo_id":"rowan","name":"Rowan University","base_url":"https://rdw.rowan.edu/do/oai/"},"display":{"title":"Hybrid solvers for the Boolean Satisfiability problem: an exploration","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Nelson, Nicole"],"institution":null,"degree_name":"M.S. Computer Science","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Lobo, Andrea"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2012,"date_issued":"2012-12-12T08:00:00Z","date_published":"2012-12-12T08:00:00Z","updated_at":"2026-07-24T04:13:03Z","subjects":["NP-complete problems","Computer Sciences"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://rdw.rowan.edu/etd/239","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Lobo, Andrea"]},{"key":"dc:creator","label":"Author","values":["Nelson, Nicole"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.available","label":"Dc Date Available","values":["2020-03-03T19:58:51Z"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S. Computer Science"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["NP-complete problems","Computer Sciences"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://rdw.rowan.edu/etd/239"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Hybrid solvers for the Boolean Satisfiability problem: an exploration"]}]}],"canonical_facts":{"dc:contributor":["Lobo, Andrea"],"dc:creator":["Nelson, Nicole"],"dc:date.available":["2020-03-03T19:58:51Z"],"dc:description.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."],"dc:identifier":["https://rdw.rowan.edu/etd/239"],"dc:subject":["NP-complete problems","Computer Sciences"],"dc:title":["Hybrid solvers for the Boolean Satisfiability problem: an exploration"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S. Computer Science"]},"updated_at":"2026-07-24T04:13:03Z"}