Abstract
Leading algorithms for Boolean satisfiability (SAT) are based on either a depth-first tree traversal of the search space (the DLL procedure [6]) or resolution (the DP procedure [7]). In this work we introduce a variant of Breadth-First Search (BFS) based on the ability of Zero-Suppressed Binary Decision Diagrams (ZDDs) to compactly represent sparse or structured collections of subsets. While a BFS may require an exponential amount of memory, our new algorithm performs BFS directly with an implicit representation and achieves unconventional reductions in the search space.
We empirically evaluate our implementation on classical SAT instances difficult for DLL/DP solvers. Our main result is the empirical Θ(n 4) runtime for hole-n instances, on which DLL solvers require exponential time.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
F. A. Aloul, I. L. Markov, and K. A. Sakallah. Faster SAT and Smaller BDDs via Common Function Structure. Proc. Intl. Conf. Computer-Aided Design, 2001.
F. A. Aloul, M. Mneimneh, and K. A. Sakallah. Backtrack Search Using ZBDDs. Intl. Workshop on Logic and Synthesis, (IWLS), 2001.
P. Beame and R. Karp. The efficiency of resolution and Davis-Putnam procedures. submitted for publication.
P. Chatalic and L. Simon. Multi-Resolution on Compressed Sets of Clauses. Proc. of 12th International Conference on Tools with Artificial Intelligence (ICTAI-2000), November 2000.
P. Chatalic and L. Simon. ZRes: the old DP meets ZBDDs. Proc. of the 17th Conf. of Autom. Deduction (CADE), 2000.
M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. Comm. ACM, 5:394–397, 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. Jounal of the ACM, 7:201–215, 1960.
P. Ferragina and G. Manzini. An experimental study of a compressed index. Proc. 12th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2001.
R. Gasser. Harnessing Computational Resources for Efficient Exhaustive Search. PhD thesis, Swiss Fed Inst Tech, Zurich, 1994.
R. L. Graham, M. Grötschel, and L. Lovász, editors. Handbook of Combinatorics. MIT Press, January 1996.
J. F. Groote and H. Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Technical Report UU-CS-2000-14, Utrecht University, 2000.
A. San Miguel. Random 3-SAT and BDDs: The Plot Thickens Further. CP, 2001.
S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems. 30th ACM/IEEE DAC, 1993.
A. Mishchenko. An Introduction to Zero-Suppressed Binary Decision Diagrams. http://www.ee.pdx.edu/~alanmi/research/.
A. Mishchenko. EXTRA v. 1.3: Software Library Extending CUDD Package: Release 2.3.x. http://www.ee.pdx.edu/~alanmi/research/extra.htm.
M. Moskewicz et al. Chaff: Engineering an Efficient SAT Solver. Proc. of IEEE/ACM DAC, pages 530–535, 2001.
J. P. Marques Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. ICCAD, 1996.
F Somenzi. CUDD: CU Decision Diagram Package Release 2.3.1. http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html.
T. E. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In J. P. Jouannaud, editor, 1st Intl. Conf. on Constraints in Comp. Logics, volume 845 of LNCS, pages 34–49. Springer, September 1994.
Urquhart. Hard examples for resolution. Journal of the ACM, 34, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Motter, D.B., Markov, I.L. (2002). A Compressed Breadth-First Search for Satisfiability. In: Mount, D.M., Stein, C. (eds) Algorithm Engineering and Experiments. ALENEX 2002. Lecture Notes in Computer Science, vol 2409. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45643-0_3
Download citation
DOI: https://doi.org/10.1007/3-540-45643-0_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43977-6
Online ISBN: 978-3-540-45643-8
eBook Packages: Springer Book Archive