Cache Conscious Data Structures for Boolean Satisfiability Solvers
Citations
Altmetric
Author
CHU, GG; HARWOOD, A; STUCKEY, PDate
2010Source Title
Journal of Satisfiability, Boolean Modeling and ComputationPublisher
IOS PressAffiliation
Computer Science And Software EngineeringMetadata
Show full item recordDocument Type
Journal ArticleCitations
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-120Access Status
Access this item via the Open Access locationDescription
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 classifiedExport 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