MCSMUS is a state-of-the-art tool to extract MUSes from CNF formulas
MCSMUS can extract minimal unsatisfiable or maximally satisfiable sets of clauses from CNF formulas. It has facilities for extracting either a single, several, or all such subsets. It has can use several SAT solvers as backend and comes with minisat, glucose, and lingeling backends.
Mots clés
Lien vers l'élément du SI MIA
mcsmus Informations générales
Informations spécifiques
Langage(s) de développement
N° de version courante
V1.0 Date de la version courante
OS supporté
Type de licence
Etat
Développement suivi Auteur(s)
George Katsirelos
Contact
georgios.katsirelos@inra.fr
Publication de référence
