Exact Searching for the Smallest Deterministic Automaton

We propose an approach to minimum-state deterministic finite automaton (DFA) inductive synthesis that is based on using satisfiability modulo theories (SMT) solvers. To that end, we explain how DFAs and their response to input samples can be encoded as logic formulas with integer variables, equations, and uninterpreted functions. An SMT solver is then tasked with finding an assignment for such a formula, from which we can extract the automaton of a required size. We provide an implementation of this approach, which we use to conduct experiments on a series of benchmarks. The results showed that our method outperforms in terms of CPU time other SAT and SMT approaches and other exact algorithms on prepared benchmarks.