MiFuMaX

MiFuMaX is an open-source unsat-based MaxSAT solver (both unweighted and weighted). Based on the algorithms by Fu and Malik [FM06] and Manquinho et al. [MSP09]. Minisat is used as the underlying SAT solver [ES03].

The solver is implemented using literate programming so it will hopefully be useful for people who wish to learn about unsatisfiability-based MaxSAT solving. The current implementation does not use any fancy techniques so its performance should be seen as a baseline for the above-mentioned algorithms.

Download

Program+documentation as PDF

weighted-0.9, windows binary
weighted-0.9, mac binary
weighted-0.9, linux 64-bit binary
partial-0.9, linux 64-bit binary
sources-0.9

Results

The unweighted version of the solver placed 1st in the track "Unweighted Max-SAT-Industrial" of the 2013 MaxSAT Evaluation.

COPYRIGHT NOTICE

(C) 2013 Mikolas Janota

MiFuMaX is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

MiFuMaX is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with MiFuMaX. If not, see GNU Licence.

References
[ES03] An extensible SAT-solver
Niklas Eén and Niklas Sörensson. SAT 2003
[FM06] On solving the partial MAX-SAT problem.
Zhaohui Fu and Sharad Malik. SAT 2006
[MSP09] Algorithms for weighted boolean optimization.
Vasco M. Manquinho, Joao P. Marques Silva, and Jordi Planes. SAT 2009

Valid XHTML 1.0 Strict VI Improved Last updated: Oct 11, 2017 14:51:45 PM