{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:50:36Z","timestamp":1762102236761},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"abstract":"<jats:p>The last 20 years have seen dramatic improvements in the performance\n\nof algorithms for Boolean satisfiability---so-called SAT solvers---and\n\ntoday conflict-driven clause learning (CDCL) solvers are routinely\n\nused in a wide range of application areas.  One serious short-coming\n\nof CDCL, however, is that the underlying method of reasoning is quite\n\nweak.  A tantalizing solution is to instead use stronger\n\npseudo-Boolean (PB) reasoning, but so far the promise of exponential\n\ngains in performance has failed to materialize---the increased\n\ntheoretical strength seems hard to harness algorithmically, and in\n\nmany applications CDCL-based methods are still superior.  We propose a\n\nmodified approach to pseudo-Boolean solving based on division instead\n\nof the saturation rule used in [Chai and Kuehlmann '05] and other PB\n\nsolvers.  In addition to resulting in a stronger conflict analysis,\n\nthis also improves performance by keeping integer coefficient sizes\n\ndown, and yields a very competitive solver as shown by the results in\n\nthe Pseudo-Boolean Competitions 2015 and 2016.<\/jats:p>","DOI":"10.24963\/ijcai.2018\/180","type":"proceedings-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T05:49:10Z","timestamp":1530769750000},"page":"1291-1299","source":"Crossref","is-referenced-by-count":27,"title":["Divide and Conquer: Towards Faster Pseudo-Boolean Solving"],"prefix":"10.24963","author":[{"given":"Jan","family":"Elffers","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology"}]}],"member":"10584","event":{"number":"27","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"acronym":"IJCAI-2018","name":"Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}","start":{"date-parts":[[2018,7,13]]},"theme":"Artificial Intelligence","location":"Stockholm, Sweden","end":{"date-parts":[[2018,7,19]]}},"container-title":["Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T05:50:34Z","timestamp":1530769834000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2018\/180"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2018\/180","relation":{},"subject":[],"published":{"date-parts":[[2018,7]]}}}