MiFuMax—a Literate MaxSAT Solver

The main motivation behind the MaxSAT solver MiFuMax is twofold. It provides a baseline implementation of core-based algorithms for both weighted and unweighted MaxSAT. Such baseline implementation may serve for evaluation of evolving solvers. MiFuMax is written in literate programming and as such is instructive for anyone interested in learning about the implementation of modern core-based MaxSAT solvers. Despite its educative background, the solver has placed 1^st in the Unweighted Max-SAT-Industrial track of the 2013 MaxSAT Evaluation and it has been successfully applied in other research.