MIN2SMT - A MINION to SMT-LIB2 Compiler

Constraint satisfaction solvers are fundamental tools for addressing diverse real-world challenges however, different solvers often require models written in distinct programming or modeling languages making interoperability and performance comparison difficult. To partially solve this challenge, we11 introduce a compiler that takes input models written for the MINION constraint solver and converts them to equivalent SMT-LIB2 representations. Our compiler is publicly available. Furthermore, we present a testing methodology to verify the correctness of our translations and empirically evaluate our compiler using the solver Z3. In this experiment, we not only tested the conversions of basic MINION language elements but also considered complex MINION models used for diagnosis.