{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T14:52:41Z","timestamp":1725720761284},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Dividing a Boolean formula into smaller independent sub-formulae can be a useful technique for accelerating the solution of Boolean problems, including SAT and #SAT. Nevertheless, and despite promising early results, formula partitioning is hardly used in state-of-the-art solvers. In this paper, we show that this is rooted in a lack of consistency of the usefulness of formula partitioning techniques. In particular, we evaluate two existing and a novel partitioning model, coupled with two existing and two novel partitioning algorithms, on a wide range of benchmark instances. Our results show that there is no one-size-fits-all solution: for different formula types, different partitioning models and algorithms are the most suitable. While these results might seem negative, they help to improve our understanding about formula partitioning; moreover, the findings also give some guidance as to which method to use for what kinds of formulae.<\/jats:p>","DOI":"10.29007\/9skn","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:02:59Z","timestamp":1516730579000},"page":"41-24","source":"Crossref","is-referenced-by-count":1,"title":["Formula partitioning revisited"],"prefix":"10.29007","volume":"27","author":[{"given":"Zoltan","family":"Mann","sequence":"first","affiliation":[]},{"given":"Pal","family":"Papp","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"POS-14. Fifth Pragmatics of SAT workshop"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:03:00Z","timestamp":1516730580000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/SD"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/9skn","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}