LIPIcs.SAT.2023.16.pdf
- Filesize: 0.59 MB
- 11 pages
Document
Bounds on BDD-Based Bucket Elimination
Author
-
Part of:
Volume:
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Theory and Applications of Satisfiability Testing (SAT) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-08-09
Cite As Get BibTex
Stefan Mengel. Bounds on BDD-Based Bucket Elimination. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.16
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Proof complexity
- Theory of computation → Constraint and logic programming
Keywords
- Bucket Elimination
- Binary Decision Diagrams
- Satisfiability
- Complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Antoine Amarilli, Florent Capelli, Mikaël Monet, and Pierre Senellart. Connecting knowledge compilation classes and width parameters. Theory Comput. Syst., 64(5):861-914, 2020. URL: https://doi.org/10.1007/s00224-019-09930-2.
- Albert Atserias, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint propagation as a proof system. In 10th International Conference Principles and Practice of Constraint Programming,CP 2004,, volume 3258 of Lecture Notes in Computer Science, pages 77-91. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30201-8_9.
- Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
- Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
- Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
- Randal E. Bryant and Marijn J. H. Heule. Generating extended resolution proofs with a bdd-based SAT solver. In 27th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, volume 12651 of Lecture Notes in Computer Science, pages 76-93. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_5.
- Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov. Lower bounds on OBDD proofs with several orders. ACM Trans. Comput. Log., 22(4):26:1-26:30, 2021. URL: https://doi.org/10.1145/3468855.
- Wei Chen and Wenhui Zhang. A direct construction of polynomial-size OBDD proof of pigeon hole problem. Inf. Process. Lett., 109(10):472-477, 2009. URL: https://doi.org/10.1016/j.ipl.2009.01.006.
- Cayden R. Codel, Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. Bipartite perfect matching benchmarks. http://www.pragmaticsofsat.org/2021/BiPartGen-slides.pdf, 2021. presentation at Pragmatics of SAT 2021 workshop.
- Cayden R. Codel, Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. Bipartite perfect matching benchmarks. unpublished report available at https://www.cs.cmu.edu/~jereeves/research/bipart-paper.pdf, 2021.
-
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201-215, 1960.
- Rina Dechter. Bucket elimination: A unifying framework for reasoning. Artif. Intell., 113(1-2):41-85, 1999. URL: https://doi.org/10.1016/S0004-3702(99)00059-4.
- Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
- Toni Jussila, Carsten Sinz, and Armin Biere. Extended resolution proofs for symbolic SAT solving with quantification. In International Conference on Theory and Applications of Satisfiability Testing, SAT 2006, volume 4121 of Lecture Notes in Computer Science, pages 54-60. Springer, 2006. URL: https://doi.org/10.1007/11814948_8.
- Guoqiang Pan and Moshe Y. Vardi. Symbolic techniques in satisfiability solving. J. Autom. Reason., 35(1-3):25-50, 2005. URL: https://doi.org/10.1007/s10817-005-9009-7.
- Alexander A. Razborov. Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci., 69(1):3-27, 2004. URL: https://doi.org/10.1016/j.jcss.2004.01.004.
- Irina Rish and Rina Dechter. Resolution versus search: Two strategies for SAT. J. Autom. Reason., 24(1/2):225-275, 2000. URL: https://doi.org/10.1023/A:1006303512524.