MEMIN: SAT-based exact minimization of incompletely specified Mealy machines

In this paper, we take a fresh look at a well-known NP-complete problem-the exact minimization of incompletely specified Mealy machines. Most existing exact techniques in this area are based on the enumeration of sets of compatible states, and the solution of a covering problem. We propose a different approach. In our approach, first, a polynomial-time algorithm is used to compute a partial solution. This partial solution is then extended to a minimum-size complete solution by solving a series of boolean satisfiability (SAT) problems. We evaluate our implementation on the same set of benchmarks used previously in the literature. On a number of hard benchmarks, our approach outperforms existing exact minimization techniques by several orders of magnitude; it is even competitive with state-of-the-art heuristic approaches on most benchmarks.