Several Issues on the Boolean Satisfiability (SAT) Problem

Simple item page
dc.contributor.advisorQu, Gangen_US
dc.contributor.authorPari, Pushkin Rajen_US
dc.contributor.departmentElectrical Engineeringen_US
dc.date.accessioned2004-06-04T05:38:24Z
dc.date.available2004-06-04T05:38:24Z
dc.date.issued2004-04-30en_US
dc.description.abstractBoolean Satisfiability (SAT) is often used as the model for a significant and increasing number of applications in Electronics Design Automation (EDA) and many other fields of computer science and engineering. Although the SAT problem belongs to the class NP-complete - problems that do not have a polynomial run time algorithm but answers for which can be checked for correctness, by an algorithm with run time is polynomial in the size of the input - typical SAT instances are easy to solve. Both theoretical and empirical studies have been conducted on various SAT models to investigate when SAT instances become hard to solve. For more than a decade, crossover point has been the only parameter considered for hardness. Existing results state that for random SAT, the problems becomes relatively harder when the clause to variable ratio is 4.3. This thesis work is motivated by the observation that not all benchmarks at the crossover point are hard. We conjecture that the structure of the solution space is also related to the hardness. We provide an empirical framework for the validation of this conjecture. Firstly, we show by experiments that (1) the crossover point is not the only metric to characterize hardness and (2) existing benchmarks are inefficient in providing solution space information We present a novel approach to generate the SAT instances with known solution space structure. Another related issue on how to obtain the solution space information is also discussed, where we propose two probabilistic techniques for quick estimation of the solution space with high accuracy.en_US
dc.format.extent1211060 bytes
dc.format.mimetypeapplication/pdf
dc.identifier.urihttp://hdl.handle.net/1903/1427
dc.language.isoen_US
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.subject.pqcontrolledEngineering, Electronics and Electricalen_US
dc.subject.pquncontrolledRandomen_US
dc.subject.pquncontrolledBooleanen_US
dc.subject.pquncontrolledSatisfiabilityen_US
dc.subject.pquncontrolledSATen_US
dc.subject.pquncontrolledConstrainten_US
dc.subject.pquncontrolledNPen_US
dc.titleSeveral Issues on the Boolean Satisfiability (SAT) Problemen_US
dc.typeThesisen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
umi-umd-1470.pdf
Size:
1.15 MB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Electrical & Computer Engineering Theses and Dissertations