2002 | OriginalPaper | Buchkapitel
A Compressed Breadth-First Search for Satisfiability
verfasst von : DoRon B. Motter, Igor L. Markov
Erschienen in: Algorithm Engineering and Experiments
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 Θ(n4) runtime for hole-n instances, on which DLL solvers require exponential time.