Article

A Compressed Breadth-First Search for Satisfiability

Authors:

DoRon B. Motter,

Igor L. MarkovAuthors Info & Claims

ALENEX '02: Revised Papers from the 4th International Workshop on Algorithm Engineering and Experiments

Pages 29 - 42

Published: 04 January 2002 Publication History

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 thiswork 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 ⁴) runtime for holen instances, on which DLL solvers require exponential time.

References

[1]

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.

[2]

F. A. Aloul, M. Mneimneh, and K. A. Sakallah. Backtrack Search Using ZBDDs. Intl. Workshop on Logic and Synthesis, (IWLS) , 2001.

[3]

P. Beame and R. Karp. The efficiency of resolution and Davis-Putnam procedures . submitted for publication.

[4]

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.

[5]

P. Chatalic and L. Simon. ZRes: the old DP meets ZBDDs. Proc. of the 17th Conf. of Autom. Deduction (CADE) , 2000.

[6]

M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem Proving. Comm. ACM , 5:394-397, 1962.

[7]

M. Davis and H. Putnam. A computing procedure for quantification theory. Jounal of the ACM , 7:201-215, 1960.

[8]

P. Ferragina and G. Manzini. An experimental study of a compressed index. Proc. 12th ACM-SIAM Symposium on Discrete Algorithms (SODA) , 2001.

[9]

R. Gasser. Harnessing Computational Resources for Efficient Exhaustive Search . PhD thesis, Swiss Fed Inst Tech, Zurich, 1994.

[10]

R. L. Graham, M. Grötschel, and L. Lovász, editors. Handbook of Combinatorics . MIT Press, January 1996.

[11]

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.

[12]

A. San Miguel. Random 3-SAT and BDDs: The Plot Thickens Further. CP , 2001.

[13]

S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems. 30th ACM/IEEE DAC , 1993.

[14]

A. Mishchenko. An Introduction to Zero-Suppressed Binary Decision Diagrams. http://www.ee.pdx.edu/~alanmi/research/.

[15]

A. Mishchenko. EXTRA v. 1.3: Software Library Extending CUDD Package: Release 2.3.x. http://www.ee.pdx.edu/~alanmi/research/extra.htm.

[16]

M. Moskewicz et al. Chaff: Engineering an Efficient SAT Solver. Proc. of IEEE/ACM DAC , pages 530-535, 2001.

[17]

J. P. Marques Silva and K. A. Sakallah. GRASP: A new search algorithm for satisfiability. ICCAD , 1996.

[18]

F. Somenzi. CUDD: CU Decision Diagram Package Release 2.3.1. http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html.

[19]

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.

[20]

A. Urquhart. Hard examples for resolution. Journal of the ACM , 34, 1987.

Cited By

Sabharwal A(2009)SymChaffConstraints10.1007/s10601-008-9060-114:4(478-505)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.1007/s10601-008-9060-1
Sinz CBiere A(2006)Extended resolution proofs for conjoining BDDsProceedings of the First international computer science conference on Theory and Applications10.1007/11753728_60(600-611)Online publication date: 8-Jun-2006
https://dl.acm.org/doi/10.1007/11753728_60
Sabharwal A(2005)SymChaffProceedings of the 20th national conference on Artificial intelligence - Volume 110.5555/1619332.1619408(467-474)Online publication date: 9-Jul-2005
https://dl.acm.org/doi/10.5555/1619332.1619408
Show More Cited By

Recommendations

Breadth-first heuristic search

Recent work shows that the memory requirements of A* and related graph-search algorithms can be reduced substantially by only storing nodes that are on or near the search frontier, using special techniques to prevent node regeneration, and recovering ...
Lifted search engines for satisfiability
Breadth-first heuristic search
KR'04: Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning

Recent work shows that the memory requirements of best-first heuristic search can be reduced substantially by using a divide-and-conquer method of solution reconstruction. We show that memory requirements can be reduced even further by using a breadth-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ALENEX '02: Revised Papers from the 4th International Workshop on Algorithm Engineering and Experiments

January 2002

205 pages

ISBN:3540439773

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 04 January 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sabharwal A(2009)SymChaffConstraints10.1007/s10601-008-9060-114:4(478-505)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.1007/s10601-008-9060-1
Sinz CBiere A(2006)Extended resolution proofs for conjoining BDDsProceedings of the First international computer science conference on Theory and Applications10.1007/11753728_60(600-611)Online publication date: 8-Jun-2006
https://dl.acm.org/doi/10.1007/11753728_60
Sabharwal A(2005)SymChaffProceedings of the 20th national conference on Artificial intelligence - Volume 110.5555/1619332.1619408(467-474)Online publication date: 9-Jul-2005
https://dl.acm.org/doi/10.5555/1619332.1619408
Motter DRoy JMarkov I(2005)Resolution cannot polynomially simulate compressed-BFSAnnals of Mathematics and Artificial Intelligence10.1007/s10472-004-8427-244:1-2(121-156)Online publication date: 1-May-2005
https://dl.acm.org/doi/10.1007/s10472-004-8427-2
Pan GVardi M(2004)Search vs. symbolic techniques in satisfiability solvingProceedings of the 7th international conference on Theory and Applications of Satisfiability Testing10.1007/11527695_19(235-250)Online publication date: 10-May-2004
https://dl.acm.org/doi/10.1007/11527695_19

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents