MUSer2 (MUS extractor v2) - (V/G)MUS/MES extraction tool


MUSer2 is an MUS, group-MUS, variable-MUS, interesting-VMUS/GVMUS [4] and MES (minimal equivalent subformula) extraction tool that implements hybrid extraction algorithm HYB [1] and its extensions [2,3,4]. The MUS functionality of MUSer2 is summarized in [5]. The theory behind the MUS part is summarized in [6].

The relevant publications are:

  1. J. Marques-Silva and I. Lynce: On Improving MUS Extraction Algorithms. SAT 2011. LNCS 6695, pp. 159-173
  2. A. Belov and J. Marques-Silva: Accelerating MUS Extraction with Recursive Model Rotation. FMCAD 2011.
  3. A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva: On Efficient Computation of Variable MUSes. SAT 2012. LNCS 7317, pp. 296-309
  4. A. Belov, M. Janota, I. Lynce and J. Marques-Silva: On Computing Minimal Equivalent Subformulas. CP 2012 (to appear).
  5. A. Belov and J. Marques-Silva: MUSer2: An Efficient MUS Extractor. POS 2012.
  6. A. Belov, I. Lynce and J. Marques-Silva: Towards Efficient MUS Extraction. AI Communications, 2012 (In Press) [preprint]


Aug 21, 2012: new source (muser2-src-20120821) and binary (muser2-20120821) distributions: bug fixes (group-mode output; finalization in source distro, might have performance impact).

Jul 7, 2012: new source distribution (muser2-src-20120706): propagated bug fixes from the binary distro.

Jul 6, 2012: new binary distribution (muser2-20120706): bug fixes (trimming; group-mode).

Jul 3, 2012: new binary distribution (muser2-20120703): bug fixes and functionality to get over-approximation on timeout/interrupt.

Jun 28, 2012: new source distribution, includes everything discussed in POS12 paper.

Jun 27, 2012: new binary distribution, includes MES computation functionality.


MUSer2 is currently available from bitbucket.

Public release for teaching and research use only.

Please contact Anton in case of any questions or problems.

Download binaries (Linux 32/64bit, MacOSX 64 bit) here. Please contact us if you need a binary for a different UNIX-based platform.

Download source distribution here. The source distribution is under GPLv3, and lacks some of the features in the binary.


The instructions for using MUSer2 are available here.

Example Usage

1. computation of a MUS:

 run-muser2 ../examples/bitops0.cnf  

2. computation of a group-MUS:

 run-muser2 -grp ../examples/bitops0.gcnf

3. computation of a variable-MUS:

 run-muser2 -var ../examples/c499_gr_2pin_w5.shuffled.cnf.gz

4. computation of an interesting-VMUS:

 run-muser2 -var -grp ../examples/b21_242.vgcnf.gz

5. computation of an MES using chunking mode and specialized model rotation

 run-muser2 -irr -chunk 1000 -imr ../examples/bw_large.a.cnf


The set of 500 benchmark CNF instances used in the experiments reported in the SAT 2011 and FMCAD 2011 papers are available in this archive. The CNF and group-CNF benchmarks used in the MUS track of SAT Competition 2011 are available from the competition page.

Current Results

Comparison with the MUS extractors that took the top 3 places in the MUS track of SAT Competition 2011. Same set of benchmarks as in the competition, and the same time limit. Note that the memory limit here is 4 GB, vs 7.8 GB at the competition.



The research on MUS extraction and the devlopement of MUSer2 were partially supported by Science Foundation Ireland