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

Simple item page
dc.contributor.committeeChairZhang, Yuanlin
dc.contributor.committeeMemberGelfond, Michael
dc.contributor.committeeMemberWatson, Richard
dc.creatorJn Charles, Jeriah
dc.date.accessioned2016-11-14T23:32:42Z
dc.date.available2012-06-29T15:05:57Z
dc.date.available2016-11-14T23:32:42Z
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.subjectAlgorithm
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

Files

Collections

Texas Tech University