Paper Info
Title
Heuristic Search Algorithms Based on Symbolic Data Structures
Abstract
Search algorithms in formal verification invariably suffer from combinational explosions in the number of states as complexity increases. One approach to alleviate this problem is to use symbolic data structures called BDDs (Binary Decision Diagrams). BDDs represent sets of states as Boolean expressions, which makes them ideal data structures for problems in AI and verification with large state spaces. In this paper we demonstrate a BDD-based A*algorithm, and compare the performance of X with this algorithm using heuristics that have varying levels of informedness. We find that contrary to expectation, the BDD-based algorithm is not faster in certain circumstances, namely if the heuristic is strong. In this case, X can be faster and will use a lot less memory. Only if the heuristic is weak will the BDD-based algorithm be faster, but even in this case, it will require substantially more memory than X. In short, a symbolic approach only pays dividends if the heuristic is weak, and this will have an associated memory penalty. We base our performance comparisons on the well-known sliding tile puzzle benchmark.
Year
DOI
Venue
2003
10.1007/978-3-540-24581-0_83
AI 2003: ADVANCES IN ARTIFICIAL INTELLIGENCE
Keywords
Field
DocType
heuristic search,shortest path,binary decision diagrams
Data structure,Heuristic,Search algorithm,Computer science,Binary decision diagram,Symbolic computation,Algorithm,Heuristics,Boolean expression,Formal verification
Conference
Volume
ISSN
Citations 
2903
0302-9743
10
PageRank 
References 
Authors
0.54
20
2
Name
Order
Citations
PageRank
Albert Nymeyer11069.98
Kairong Qian2633.38