Impact of the LZW-based common subexpression elimination algorithm on SAT-solving efficiency

dc.contributor.committeeChairZhang, Yuanlin
dc.contributor.committeeMemberGelfond, Michael
dc.contributor.committeeMemberWatson, Richard
dc.creatorJn Charles, Jeriah
dc.date.available2012-06-29T15:05:57Z
dc.date.issued2012-05
dc.degree.departmentComputer Science
dc.description.abstractThe Satisfiability (SAT) problem is the problem of finding an assignment that satisfies a given propositional formula. SAT is effective in solving many important problems in areas such as automated reasoning, computer-aided design, and planning in Artificial Intelligence. The need to solve these problems in a reduced amount of time has geared considerable research in improving the performance of SAT solvers resulting in many solver algorithms being created or modified. This research investigates how the removal of common subexpressions in a formula via the Lempel–Ziv-Welch (LZW)-based approach can affect the efficiency of SAT solving. By substituting common subexpressions for new variables in the original formula, we compare the results of passing the original formula and the new equivalent formula through a SAT solver. In this LZW-based approach, we modify the Lempel–Ziv-Welch data compression algorithm to find and substitute the common subexpressions in the formula.
dc.format.mimetypeapplication/pdf
dc.identifier.urihttp://hdl.handle.net/2346/45350
dc.language.isoeng
dc.rights.availabilityUnrestricted.
dc.subjectData compression (Computer science)
dc.subjectComputer science
dc.subjectAlgorithms
dc.subjectLempel–Ziv–Welch
dc.subjectLaszlo (Computer program language)
dc.titleImpact of the LZW-based common subexpression elimination algorithm on SAT-solving efficiency
dc.typeThesis
thesis.degree.departmentComputer Science
thesis.degree.disciplineComputer Science
thesis.degree.grantorTexas Tech University
thesis.degree.levelMasters
thesis.degree.nameMaster of Science

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
JN-CHARLES-THESIS.pdf
Size:
522.46 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.13 KB
Format:
Plain Text
Description: