Divide and conquer: Towards faster pseudo-boolean solving

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationProceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
EditorsJerome Lang
Number of pages9
PublisherInternational Joint Conferences on Artificial Intelligence
Publication date2018
Pages1291-1299
ISBN (Electronic)9780999241127
DOIs
Publication statusPublished - 2018
Externally publishedYes
Event27th International Joint Conference on Artificial Intelligence, IJCAI 2018 - Stockholm, Sweden
Duration: 13 Jul 201819 Jul 2018

Conference

Conference27th International Joint Conference on Artificial Intelligence, IJCAI 2018
LandSweden
ByStockholm
Periode13/07/201819/07/2018
SponsorInternational Joint Conferences on Artifical Intelligence (IJCAI)
SeriesIJCAI International Joint Conference on Artificial Intelligence
Volume2018-July
ISSN1045-0823

ID: 251867419