Masters Theses

Keywords and Phrases

Asynchronous Parallel Computation; Boolean Satisfiability; Hyper-heuristics; Program Understanding

Abstract

"Modern society gives rise to complex problems which sometimes lend themselves to being transformed into Boolean satisfiability (SAT) decision problems; this thesis presents an example from the program understanding domain. Current conflict-driven clause learning (CDCL) SAT solvers employ all-purpose heuristics for making decisions when finding truth assignments for arbitrary logical expressions called SAT instances. The instances derived from a particular problem class exhibit a unique underlying structure which impacts a solver's effectiveness. Thus, tailoring the solver heuristics to a particular problem class can significantly enhance the solver's performance; however, manual specialization is very labor intensive. Automated development may apply hyper-heuristics to search program space by utilizing problem-derived building blocks. This thesis demonstrates the potential for genetic programming (GP) powered hyper-heuristic driven automated design of algorithms to create tailored CDCL solvers, in this case through custom variable scoring and learnt clause scoring heuristics, with significantly better performance on targeted classes of SAT problem instances. As the run-time of GP is often dominated by fitness evaluation, evaluating multiple offspring in parallel typically reduces the time incurred by fitness evaluation proportional to the number of parallel processing units. The naive synchronous approach requires an entire generation to be evaluated before progressing to the next generation; as such, heterogeneity in the evaluation times will degrade the performance gain, as parallel processing units will have to idle until the longest evaluation has completed. This thesis shows empirical evidence justifying the employment of an asynchronous parallel model for GP powered hyper-heuristics applied to SAT solver space, rather than the generational synchronous alternative, for gaining speed-ups in evolution time. Additionally, this thesis explores the use of a multi-objective GP to reveal the trade-off surface between multiple CDCL attributes"--Abstract, page iii.

Advisor(s)

Tauritz, Daniel R.

Committee Member(s)

McMillin, Bruce M.
Mulder, Samuel A.

Department(s)

Computer Science

Degree Name

M.S. in Computer Science

Sponsor(s)

Sandia Laboratories

Comments

Funding provided by Sandia National Laboratories through their Critical Skills Master's Program. Sandia National Laboratories is a multi-program laboratory managed and operated by Sandia Corporation, a wholly owned subsidiary of Lockheed Martin Corporation, for the United States Department of Energy's National Nuclear Security Administration under contract DE-AC04-94AL85000.

Publisher

Missouri University of Science and Technology

Publication Date

Summer 2016

Pagination

ix, 64 pages

Note about bibliography

Includes bibliographical references (pages 59-63).

Rights

© 2016 Alex Raymond Bertels, All rights reserved.

Document Type

Thesis - Open Access

File Type

text

Language

English

Subject Headings

Parallel processing (Electronic computers)Evolutionary computationExpert systems (Computer science)

Thesis Number

T 10949

Electronic OCLC #

958293369

Download

Share

 
COinS