Mint is a Python prototype implementation of the minimum satisfying assignment solver proposed in [*]. Given an SMT formula in the SMTLIB format (version 2), it computes a model of the formula that assigns the smallest possible number of variables of the formula leaving all the other variables unassigned. The underlying algorithm is based on implicit hitting set approach and the minimal hitting set duality between "minimal existential subsets" and "minimal falsifying subsets" of a formula. The minimal hitting set engine is implemented as an incremental core-guided MaxSAT solver.

[*] A. Ignatiev, A. Previti, and J. Marques-Silva. On Finding Minimum Satisfying Assignments. In: Proc. CP 2016, pp. 287–297.

Authors: Alexey Ignatiev, Alessandro Previti
Contributor: Joao Marques-Silva

Download: Gzipped TAR archive