Divide and conquer: Towards faster pseudo-boolean solving
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Divide and conquer : Towards faster pseudo-boolean solving. / Elffers, Jan; Nordström, Jakob.
Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018. ed. / Jerome Lang. International Joint Conferences on Artificial Intelligence, 2018. p. 1291-1299 (IJCAI International Joint Conference on Artificial Intelligence, Vol. 2018-July).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Divide and conquer
T2 - 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
AU - Elffers, Jan
AU - Nordström, Jakob
PY - 2018
Y1 - 2018
N2 - The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability-so-called SAT solvers-and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize-the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modified approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann'05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also improves performance by keeping integer coefficient sizes down, and yields a very competitive solver as shown by the results in the Pseudo-Boolean Competitions 2015 and 2016.
AB - The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability-so-called SAT solvers-and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize-the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modified approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann'05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also improves performance by keeping integer coefficient sizes down, and yields a very competitive solver as shown by the results in the Pseudo-Boolean Competitions 2015 and 2016.
UR - http://www.scopus.com/inward/record.url?scp=85049675778&partnerID=8YFLogxK
U2 - 10.24963/ijcai.2018/180
DO - 10.24963/ijcai.2018/180
M3 - Article in proceedings
AN - SCOPUS:85049675778
T3 - IJCAI International Joint Conference on Artificial Intelligence
SP - 1291
EP - 1299
BT - Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
A2 - Lang, Jerome
PB - International Joint Conferences on Artificial Intelligence
Y2 - 13 July 2018 through 19 July 2018
ER -
ID: 251867419