University Library
  • Login
A gateway to Melbourne's research publications
Minerva Access is the University's Institutional Repository. It aims to collect, preserve, and showcase the intellectual output of staff and students of the University of Melbourne for a global audience.
View Item 
  • Minerva Access
  • Engineering
  • Computing and Information Systems
  • Computing and Information Systems - Research Publications
  • View Item
  • Minerva Access
  • Engineering
  • Computing and Information Systems
  • Computing and Information Systems - Research Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

    Cache Conscious Data Structures for Boolean Satisfiability Solvers

    Thumbnail
    Citations
    Altmetric
    Author
    CHU, GG; HARWOOD, A; STUCKEY, P
    Date
    2010
    Source Title
    Journal of Satisfiability, Boolean Modeling and Computation
    Publisher
    IOS Press
    University of Melbourne Author/s
    Harwood, Aaron; Stuckey, Peter; CHU, GEOFFREY
    Affiliation
    Computer Science And Software Engineering
    Metadata
    Show full item record
    Document Type
    Journal Article
    Citations
    CHU, G. G., HARWOOD, A. & STUCKEY, P. (2010). Cache Conscious Data Structures for Boolean Satisfiability Solvers. Journal of Satisfiability, Boolean Modeling and Computation, 6 (1-3), pp.99-120
    Access Status
    Access this item via the Open Access location
    URI
    http://hdl.handle.net/11343/26737
    Open Access URL
    https://content.iospress.com/download/journal-on-satisfiability-boolean-modeling-and-computation/sat190064?id=journal-on-satisfiability-boolean-modeling-and-computation%2Fsat190064
    Description

    C1 - Journal Articles Refereed

    Abstract
    Current SAT solvers are well engineered and highly efficient, and significant research effort has been put into creating data structures that can produce maximal efficiency for the core propagation engine within SAT solvers. However, there is still substantial room for improvement. As the disparity between CPU speeds and cache sizes have increased, cache conscious data structures and algorithms have become very important. They are even more important in the context of parallel SAT solving, as issues like cache contention and main memory contention can dramatically slow down a parallel SAT solver. We present a series of data structure and algorithmic modifications that are able to increase the core propagation speed of MiniSat 2.0 by an average of 80% on a set of medium sized industrial instances, and increase the speed of a parallelized version of MiniSat running with 8 threads by 140% on those same instances.
    Keywords
    Computer Software not elsewhere classified; Computer Software and Services not elsewhere classified

    Export Reference in RIS Format     

    Endnote

    • Click on "Export Reference in RIS Format" and choose "open with... Endnote".

    Refworks

    • Click on "Export Reference in RIS Format". Login to Refworks, go to References => Import References


    Collections
    • Minerva Elements Records [45770]
    • Computing and Information Systems - Research Publications [1456]
    Minerva AccessDepositing Your Work (for University of Melbourne Staff and Students)NewsFAQs

    BrowseCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects
    My AccountLoginRegister
    StatisticsMost Popular ItemsStatistics by CountryMost Popular Authors