Symbolic search is based on checking the satisfiability of Boolean functions. 
The idea is to lessen the costs associated with the exponential memory requirements 
for the state sets involved as problem sizes get bigger. While invented for 
model checking, symbolic search features many successful AI planning systems. 

Symbolic state space search algorithms execute a functional exploration of the 
problem graph and apply Boolean expressions to represent sets of states. According 
to the space requirements of ordinary search algorithms, they save space mainly 
by sharing parts of the state vector such that the symbolic representation of a 
state set is often considerably smaller than the enumeration of all satisfying 
assignments. 

The functional representation has a drastic impact on the design of algorithms, 
as not all algorithms adapt to the exploration of state sets.
~