Abstract
Symbolic search solves state space problems consisting of an initial state, a set of goal states, and a set of actions using a succinct representation for state sets. The approach lessens the costs associated with the exponential memory requirements for the state sets involved as problem sizes get bigger. Symbolic search has been associated with the term planning via model checking (Giunchiglia and Traverso 1999). While initially applied to model check hardware verification problems (McMillan 1993), symbolic search features many modern action planning systems (Ghallab et al. 2000). Symbolic search algorithms explore the underlying problem graph by using functional expressions to represent sets of states and actions. Compared with the space requirements induced by standard explicit-state search algorithms, symbolic representations additionally save space by sharing parts of the state vector. Algorithm designs change, as not all search algorithms adapt to the exploration of state sets.
TopBackground
Binary decision diagrams or BDDs are one option for a space-efficient representation for state sets.
A BDD (Bryant 1992; see Figure 1), is a data structure to manipulate Boolean functions efficiently. BDDs are finite state machines over the alphabet {0,1} with a 1-sink that operates as an accepting state. Each internal node is labelled with the variable (index) for selecting the outgoing transition (either 1 or 0, see figure) for a given variable assignment. For evaluating a BDD, a path is traced from the root to the sinks (all paths obey the same variable ordering). What distinguishes BDDs from decision trees is the use of reduction rules, detecting unnecessary variable tests and repeating subgraphs. This leads to a unique representation, polynomial in the number of input variables for many interesting functions. The reduced and ordered BDD representation is unique; a clear benefit to the satisfiability test for Boolean formulas, which by the virtue of Cook’s Theorem (1971) is an NP-hard problem
In symbolic search, BDDs accept the state vector representation. According functions are satisfied, if the state vector for the input assignment is a member of the represented set. The characteristic function can be identified with the state set it represents.
The transition relation Trans represents the actions (see Figure 2). It refers to current state variables x and next state variables x’ and is satisfied, if there is an action that transforms a state vector into one of its successors. The transition relation for the entire problem decomposes in the disjunction of the transition relations for singleton actions. The order of variables in the state vector is crucially influencing the size of the BDD. Unfortunately, the problem of finding the ordering that minimizes the BDD size is NP-hard (Wegener 2000). The interleaved representation for the Trans(x,x’) that alternates between x and x’ variables often leads to small BDDs.
Key Terms in this Chapter
Action Planning: Refers to a world description in logic, where a number of atomic propositions describe what can be true or false in each state of the world. By applying operators to a world, one arrives at another world, where different atoms might be true or false. Usually, only few atoms are affected by an action, and most of them remain the same.
Duplicate Elimination Scope: The number of layers that a back edge in a breath-first (or best-first) search graph can cross. It is an important parameter for the design of memory-limited frontier search algorithms and has application to improve the efficiency of both symbolic and disk-based search.
Model Checking: For a system model together with a formal description of a property, model checking is a push-button decision procedure. In case the desired property is not satisfied by the model, it returns a counter-example in form of a trace. Among the options for the specification of the model, there are Kripke structures and labelled transition systems. Valid choices for property specifications are linear and branching time logics, or the propositional µ-calculus.
Relational Product: Specialized procedure that combines conjunction and variable quantification in one specialized BDD operation.
Pattern Database: Given that state in a search problem is described as a vector of state variables, pattern variables denote a subset of them. They define an abstraction such that any path in the concrete state space induces a path in the abstract one. A pattern is a specific assignment of values to the pattern variables. A pattern database completely evaluates the abstract search space prior to the base level search in form of a lookup table indexed by the abstract containing the shortest goal distance.
Pattern Packing: Solves the pattern selection problem for constructing pattern database search heuristics. One bin represents a container for the abstract state space and approximates the memory usage for pattern database construction. Multiple bins apply for disjoint pattern database construction. In difference to standard bin packing, the effect of the selection of patterns is multiplicative.