Show simple item record

dc.contributor.authorCHU, GG
dc.contributor.authorHARWOOD, A
dc.contributor.authorSTUCKEY, P
dc.date.available2014-05-21T19:46:23Z
dc.date.issued2010
dc.identifier.citationCHU, 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. https://doi.org/10.3233/sat190064.
dc.identifier.issn1574-0617
dc.identifier.urihttp://hdl.handle.net/11343/26737
dc.descriptionC1 - Journal Articles Refereed
dc.description.abstractCurrent 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.
dc.formatapplication/pdf
dc.publisherIOS Press
dc.subjectComputer Software not elsewhere classified; Computer Software and Services not elsewhere classified
dc.titleCache Conscious Data Structures for Boolean Satisfiability Solvers
dc.typeJournal Article
dc.identifier.doi10.3233/sat190064
melbourne.peerreviewPeer Reviewed
melbourne.affiliationThe University of Melbourne
melbourne.affiliation.departmentComputer Science And Software Engineering
melbourne.source.titleJournal of Satisfiability, Boolean Modeling and Computation
melbourne.source.volume6
melbourne.source.issue1-3
melbourne.source.pages99-120
melbourne.publicationid131756
melbourne.elementsid314221
melbourne.openaccess.urlhttps://content.iospress.com/download/journal-on-satisfiability-boolean-modeling-and-computation/sat190064?id=journal-on-satisfiability-boolean-modeling-and-computation%2Fsat190064
melbourne.contributor.authorHarwood, Aaron
melbourne.contributor.authorStuckey, Peter
melbourne.contributor.authorCHU, GEOFFREY
dc.identifier.eissn1574-0617
melbourne.accessrightsAccess this item via the Open Access location


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record