zbMATH — the first resource for mathematics

A compressed breadth-first search for satisfiability. (English) Zbl 1014.68560
Mount, David M. (ed.) et al., Algorithm engineering and experiments. 4th international workshop, ALENEX 2002, San Francisco, CA, USA, January 4-5, 2002. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2409, 29-42 (2002).
Summary: Leading algorithms for Boolean satisfiability (SAT) are based on either a depth-first tree traversal of the search space (the DLL procedure) or resolution (the DP procedure). 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 \(\Theta(n^4)\) runtime for hole-n instances, on which DLL solvers require exponential time.
For the entire collection see [Zbl 1008.68692].

68U99 Computing methodologies and applications
68W05 Nonnumerical algorithms
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Chaff; CUDD
Full Text: Link