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:
- -r: if no reset state is specified, any state might be a reset state (otherwise, the first state is assumed to be the reset state)
- -np: do not include the 'partial solution' in the SAT problem
- -nl: like -np, but does also not use the size of the 'partial solution' as a lower bound (i.e., does not need the partial solution at all)
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.