{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T04:14:24Z","timestamp":1725423264062},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Nowadays, powerful parallel SAT solvers are based on an algorithm portfolio. The<\/jats:p><jats:p>alternative approach, (iterative) search space partitioning, cannot keep up, although, ac-<\/jats:p><jats:p>cording to the literature, iterative partitioning systems should scale better than portfolio<\/jats:p><jats:p>solvers. In this paper we identify key problems in current parallel cooperative SAT solving<\/jats:p><jats:p>approaches, most importantly communication, how to partition the search space, and how<\/jats:p><jats:p>to utilize the sequential search engine. First, we improve on each problem separately. In<\/jats:p><jats:p>a further step, we show that combining all the improvements leads to a state-of-the-art<\/jats:p><jats:p>parallel SAT solver, which does not use the portfolio approach, but instead relies on it-<\/jats:p><jats:p>erative partitioning. The experimental evaluation of this system completely changes the<\/jats:p><jats:p>picture about the performance of search space partitioning SAT solvers: on instances of<\/jats:p><jats:p>a combined benchmark of recent SAT competitions, the presented approach can keep up<\/jats:p><jats:p>with the winners of last years SAT competition. The combined improvements improve the<\/jats:p><jats:p>existing cooperative solver splitter by 24%: instead of 561 out of 880 instances, the new<\/jats:p><jats:p>solver Pcasso can solve 696 instances.<\/jats:p>","DOI":"10.29007\/jnvf","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:53Z","timestamp":1516730573000},"page":"41-26","source":"Crossref","is-referenced-by-count":0,"title":["Modern Cooperative Parallel SAT Solving"],"prefix":"10.29007","volume":"29","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]},{"given":"Davide","family":"Lanti","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[]}],"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:55Z","timestamp":1516730575000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/jnvf","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}