{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T05:20:56Z","timestamp":1751779256531},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Effectively parallelizing SAT solving is an open and<\/jats:p><jats:p>important issue.  The current state-of-the-art is<\/jats:p><jats:p>based on parallel portfolios. This technique relies<\/jats:p><jats:p>on running multiple solvers on the same instance in<\/jats:p><jats:p>parallel.  As soon one instance finishes the entire<\/jats:p><jats:p>run stops.  Several succesful systems even use plain<\/jats:p><jats:p>parallel portfolio (PPP), where the individual solvers<\/jats:p><jats:p>do not exchange any information.  This paper contains<\/jats:p><jats:p>a thorough experimental evaluation which shows that PPP<\/jats:p><jats:p>can improve wall-clock running time because memory access<\/jats:p><jats:p>is still local, respectively the memory system can hide<\/jats:p><jats:p>the latency of memory access.  In particular, there does<\/jats:p><jats:p>not seem as much cache congestion as one might imagine.<\/jats:p><jats:p>We also present some limits on the scalibility of PPP.<\/jats:p><jats:p>Thus this paper gives one argument why PPP solvers are a<\/jats:p><jats:p>good fit for todays multi-core architectures.<\/jats:p>","DOI":"10.29007\/73n4","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:53Z","timestamp":1516730573000},"page":"28-14","source":"Crossref","is-referenced-by-count":5,"title":["Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures"],"prefix":"10.29007","volume":"29","author":[{"given":"Martin","family":"Aigner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Kirsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"POS-13. Pragmatics of SAT 2013"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:54Z","timestamp":1516730574000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/nHs"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/73n4","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}