CMP.1:5.3 - A small description can create an expensive search

An input describes b Boolean state variables. A conversion that explicitly constructs every possible state may produce 2^b vertices. Even a solver linear in the resulting graph size then gives an exponential dependence on b.

The construction may still be effective and useful for small b. For a larger budget-constrained use, keep the original answer condition and seek a representation or method that avoids explicit expansion, or derive a suitable restriction of reachable states. Calling the target solver efficient does not settle the cost of the whole reduction.