It is a natural question to find a DFA or NFA for which a given set of words should be accepted and another given set should not be accepted.

In this presentation we investigate how to find a smallest automaton for both types by means of SMT solving, and compare the results.