On division versus saturation in pseudo-boolean solving
(2019) 28th International Joint Conference on Artificial Intelligence, IJCAI 2019 In IJCAI International Joint Conference on Artificial Intelligence 2019-August. p.1711-1718- Abstract
The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al.,'87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with... (More)
The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al.,'87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with division instead of saturation can be exponentially stronger. In the other direction, we prove that simulating a single saturation step can require an exponential number of divisions. We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes.
(Less)
- author
- Gocht, Stephan LU ; Nordström, Jakob LU and Yehudayoff, Amir
- publishing date
- 2019
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019
- series title
- IJCAI International Joint Conference on Artificial Intelligence
- editor
- Kraus, Sarit
- volume
- 2019-August
- pages
- 8 pages
- publisher
- International Joint Conferences on Artificial Intelligence
- conference name
- 28th International Joint Conference on Artificial Intelligence, IJCAI 2019
- conference location
- Macao, China
- conference dates
- 2019-08-10 - 2019-08-16
- external identifiers
-
- scopus:85074915020
- ISSN
- 1045-0823
- ISBN
- 9780999241141
- DOI
- 10.24963/ijcai.2019/237
- language
- English
- LU publication?
- no
- id
- 5136d1d9-dfe8-47c2-8b21-2316074d1957
- date added to LUP
- 2020-12-18 22:15:21
- date last changed
- 2022-04-26 22:42:12
@inproceedings{5136d1d9-dfe8-47c2-8b21-2316074d1957,
abstract = {{<p>The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al.,'87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with division instead of saturation can be exponentially stronger. In the other direction, we prove that simulating a single saturation step can require an exponential number of divisions. We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes.</p>}},
author = {{Gocht, Stephan and Nordström, Jakob and Yehudayoff, Amir}},
booktitle = {{Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019}},
editor = {{Kraus, Sarit}},
isbn = {{9780999241141}},
issn = {{1045-0823}},
language = {{eng}},
pages = {{1711--1718}},
publisher = {{International Joint Conferences on Artificial Intelligence}},
series = {{IJCAI International Joint Conference on Artificial Intelligence}},
title = {{On division versus saturation in pseudo-boolean solving}},
url = {{http://dx.doi.org/10.24963/ijcai.2019/237}},
doi = {{10.24963/ijcai.2019/237}},
volume = {{2019-August}},
year = {{2019}},
}