mikolas DOT janota AT gmail DOT com
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.
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
The unweighted version of the solver placed 1st in the track "Unweighted Max-SAT-Industrial" of the 2013 MaxSAT Evaluation.
(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.
[ES03] An extensible SAT-solver SAT 2003 |
[FM06] On solving the partial MAX-SAT problem. SAT 2006 |
[MSP09] Algorithms for weighted boolean optimization. SAT 2009 |
Last updated: Oct 11, 2017 14:51:45 PM |