Divide and conquer : Towards faster pseudo-boolean solving
(2018) 27th International Joint Conference on Artificial Intelligence, IJCAI 2018 In IJCAI International Joint Conference on Artificial Intelligence 2018-July. p.1291-1299- Abstract
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... (More)
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.
(Less)
- author
- Elffers, Jan LU and Nordström, Jakob LU
- publishing date
- 2018
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
- series title
- IJCAI International Joint Conference on Artificial Intelligence
- editor
- Lang, Jerome
- volume
- 2018-July
- pages
- 9 pages
- publisher
- International Joint Conferences on Artificial Intelligence
- conference name
- 27th International Joint Conference on Artificial Intelligence, IJCAI 2018
- conference location
- Stockholm, Sweden
- conference dates
- 2018-07-13 - 2018-07-19
- external identifiers
-
- scopus:85049675778
- ISSN
- 1045-0823
- ISBN
- 9780999241127
- DOI
- 10.24963/ijcai.2018/180
- language
- English
- LU publication?
- no
- id
- d1fe22e4-309b-4911-ab6b-7af5eadb8fb4
- date added to LUP
- 2020-12-18 22:18:18
- date last changed
- 2022-04-26 22:42:12
@inproceedings{d1fe22e4-309b-4911-ab6b-7af5eadb8fb4,
abstract = {{<p>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.</p>}},
author = {{Elffers, Jan and Nordström, Jakob}},
booktitle = {{Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018}},
editor = {{Lang, Jerome}},
isbn = {{9780999241127}},
issn = {{1045-0823}},
language = {{eng}},
pages = {{1291--1299}},
publisher = {{International Joint Conferences on Artificial Intelligence}},
series = {{IJCAI International Joint Conference on Artificial Intelligence}},
title = {{Divide and conquer : Towards faster pseudo-boolean solving}},
url = {{http://dx.doi.org/10.24963/ijcai.2018/180}},
doi = {{10.24963/ijcai.2018/180}},
volume = {{2018-July}},
year = {{2018}},
}