Classic results in the theory of regular languages show that the problem of converting an NFA (nondeterministic finite automaton) into a minimal equivalent NFA is NP-hard, even for NFAs over a unary alphabet. This paper describes work on fast search techniques for finding minimal NFAs. The foundation of our approach is a characterization theorem for NFAs: we prove that a language is recognized by an nstate NFA iff it has what we call an inductive basis of size n. Using this characterization, we develop a fast incremental search for minimal NFAs for unary languages. We study the performance of our search algorithm experimentally, showing that, as compared with exhaustive search, it cuts the search space dramatically.