HgMUS - Efficient Horn group MUS enumerator


HgMus [1] is a high-performance group-MUS enumerator for Horn formulas. It is based on implicit hitting set dualization, so it enumerates both Minimal Unsatisfiable Subformulas (MUSes) and Minimal Correction Subsets (MCSes).


A Linux (64-bit) executable can be downloaded here: hgmus.tar.gz (~1.3Mbyte)

Detailed Results

Detailed results (from [1]) can be downloaded here: supplementary-material-hgmus.tar.gz (~6.3Mbyte)

Information on how to generate the axiom pinpointing instances of [1] for HgMUS can be found at EL2MUS website.


[1] M. Fareed Arif, Carlos Mencia, and Joao Marques-Silva. “Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing”. SAT 2015