A model checker verifies a property by building a graph of all
of the states in the model. In SMV, the number of states in the model
is 
, where n is the number of state variables in the cone of
the property. In fact, it is only necessary for the model checker to consider
the states that are ``reachable'' from an initial state. However, as you might
expect, the amount of computational effort required to verify a property still
tends to grow very rapidly with the number of state variables. This is known as
the ``state explosion problem''.
To address this problem, SMV uses a structure called a ``Binary Decision Diagram'' (BDD) to implicitly represent the state graph of the model, and sets of states satisfying given properties. For some models and properties, the use of BDD's (implicit enumeration) allows SMV to handle models with many orders of magnitude more states than could be handled by considering individual states (explicit enumeration). First, we see a simple example of a circuit with a very large number of states that can still be handled efficiently using BDD's. Later we'll consider what to do when a direct approach using BDD's doesn't work.