{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T07:31:55Z","timestamp":1723015915369},"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":[[2019,8]]},"abstract":"<jats:p>The conflict-driven clause learning (CDCL) paradigm has revolutionized\nSAT solving over the last two decades. Extending this approach to\npseudo-Boolean (PB) solvers doing 0-1 linear programming holds the\npromise of further exponential improvements in theory, but\nintriguingly such gains have not materialized in practice. Also\nintriguingly, most PB extensions of CDCL use not the division rule in\ncutting planes as defined in [Cook et al., '87] but instead the\nso-called saturation rule. To the best of our knowledge, there has\nbeen no study comparing the strengths of division and saturation in\nthe context of conflict-driven PB learning, when all linear\ncombinations of inequalities are required to cancel variables.\nWe show that PB solvers with division instead of saturation can be\nexponentially stronger. In the other direction, we prove that\nsimulating a single saturation step can require an exponential number\nof divisions. We also perform some experiments to see whether these\nphenomena can be observed in actual solvers. Our conclusion is that a\ncareful combination of division and saturation seems to be crucial to\nharness more of the power of cutting planes.<\/jats:p>","DOI":"10.24963\/ijcai.2019\/237","type":"proceedings-article","created":{"date-parts":[[2019,7,28]],"date-time":"2019-07-28T03:46:05Z","timestamp":1564285565000},"page":"1711-1718","source":"Crossref","is-referenced-by-count":2,"title":["On Division Versus Saturation in Pseudo-Boolean Solving"],"prefix":"10.24963","author":[{"given":"Stephan","family":"Gocht","sequence":"first","affiliation":[{"name":"KTH Royal Institute of Technology"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[{"name":"University of Copenhagen"},{"name":"KTH Royal Institute of Technology"}]},{"given":"Amir","family":"Yehudayoff","sequence":"additional","affiliation":[{"name":"Technion - Israel Institute of Technology"}]}],"member":"10584","event":{"number":"28","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"acronym":"IJCAI-2019","name":"Twenty-Eighth International Joint Conference on Artificial Intelligence {IJCAI-19}","start":{"date-parts":[[2019,8,10]]},"theme":"Artificial Intelligence","location":"Macao, China","end":{"date-parts":[[2019,8,16]]}},"container-title":["Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2019,7,28]],"date-time":"2019-07-28T03:47:46Z","timestamp":1564285666000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2019\/237"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2019,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2019\/237","relation":{},"subject":[],"published":{"date-parts":[[2019,8]]}}}