License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.16
URN: urn:nbn:de:0030-drops-184789
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18478/
Mengel, Stefan
Bounds on BDD-Based Bucket Elimination
Abstract
We study BDD-based bucket elimination, an approach to satisfiability testing using variable elimination which has seen several practical implementations in the past. We prove that it allows solving the standard pigeonhole principle formulas efficiently, when allowing different orders for variable elimination and BDD-representations, a variant of bucket elimination that was recently introduced. Furthermore, we show that this upper bound is somewhat brittle as for formulas which we get from the pigeonhole principle by restriction, i.e., fixing some of the variables, the same approach with the same variable orders has exponential runtime. We also show that the more common implementation of bucket elimination using the same order for variable elimination and the BDDs has exponential runtime for the pigeonhole principle when using either of the two orders from our upper bound, which suggests that the combination of both is the key to efficiency in the setting.
BibTeX - Entry
@InProceedings{mengel:LIPIcs.SAT.2023.16,
author = {Mengel, Stefan},
title = {{Bounds on BDD-Based Bucket Elimination}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {16:1--16:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18478},
URN = {urn:nbn:de:0030-drops-184789},
doi = {10.4230/LIPIcs.SAT.2023.16},
annote = {Keywords: Bucket Elimination, Binary Decision Diagrams, Satisfiability, Complexity}
}
Keywords: |
|
Bucket Elimination, Binary Decision Diagrams, Satisfiability, Complexity |
Collection: |
|
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) |
Issue Date: |
|
2023 |
Date of publication: |
|
09.08.2023 |