Skip to content
University of Maryland LibrariesDigital Repository at the University of Maryland
    • Login
    View Item 
    •   DRUM
    • Theses and Dissertations from UMD
    • UMD Theses and Dissertations
    • View Item
    •   DRUM
    • Theses and Dissertations from UMD
    • UMD Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Several Issues on the Boolean Satisfiability (SAT) Problem

    Thumbnail
    View/Open
    umi-umd-1470.pdf (1.154Mb)
    No. of downloads: 750

    Date
    2004-04-30
    Author
    Pari, Pushkin Raj
    Advisor
    Qu, Gang
    Metadata
    Show full item record
    Abstract
    Boolean 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.
    URI
    http://hdl.handle.net/1903/1427
    Collections
    • Electrical & Computer Engineering Theses and Dissertations
    • UMD Theses and Dissertations

    DRUM is brought to you by the University of Maryland Libraries
    University of Maryland, College Park, MD 20742-7011 (301)314-1328.
    Please send us your comments.
    Web Accessibility
     

     

    Browse

    All of DRUMCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister
    Pages
    About DRUMAbout Download Statistics

    DRUM is brought to you by the University of Maryland Libraries
    University of Maryland, College Park, MD 20742-7011 (301)314-1328.
    Please send us your comments.
    Web Accessibility