MeMin - SAT-based Exact Minimization of Incompletely Specified Mealy Machines

Introduction

MeMin is a tool for minimizing incompletely specified Mealy machines, i.e., Mealy machines where one or more outputs or next states might not be specified. Minimization of a machine M in this context means finding a machine M' with the minimal number of states that has the same input/output behavior on all input sequences, on which the behavior of M is defined (but M' might be defined on additional input sequences on which M is not defined). While the problem of minimizing Mealy machines is efficiently solvable for fully specified machines, it is NP-complete for incompletely specified machines.

Most existing exact minimization tools are based on the enumeration of sets of compatible states, and the solution of a covering problem. MeMin uses a different 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.

MeMin is written in C++, and it uses MiniSat as SAT solver. Like many existing tools, MeMin accepts inputs in the widely used KISS2 input format. In this format, Mealy machines are essentially described by a set of 4-tuples of the form (input; currentState; nextState; output).

Download and Installation

You can download a 64-bit binary Linux version of MeMin here. This is the same binary that was used for the evaluation in [1].

After downloading, make MeMin executable, e.g., by executing the following command:
  chmod u+x MeMin

Source Code

The source code of MeMin is available at https://github.com/andreas-abel/MeMin.

How to use MeMin

Simply run ./MeMin [Options] <input.kiss>. The output is written to a file named result.kiss in the same folder.

The following options can be specified:

Evaluation Results

We have compared the performance of our implementation to two other exact approaches: BICA is based on Angluin’s learning algorithm, and STAMINA (exact mode) is a popular implementation of the explicit version of the two-step standard approach. Furthermore, we have also compared our tool with STAMINA (heuristic mode), and COSME, which is another, recently proposed, heuristic technique.

We used the same sets of benchmarks that were used previously in the literature. These benchmarks come from several sources, e.g., logic synthesis, learning problems, and networks of interacting FSMs. On a number of hard benchmarks, our approach outperforms the other exact minimization techniques by several orders of magnitude; it is even competitive with state-of-the-art heuristic approaches on most benchmarks.

A table with all benchmark results can be found here.

References

Please see the following paper if you are interested in how MeMin works:
  1. MeMin: SAT-based Exact Minimization of Incompletely Specified Mealy Machines
    A. Abel and J. Reineke
    ICCAD, 2015. [doi]  [pdf]  [bib]