MUSer2 is an MUS, group-MUS, variable-MUS, interesting-VMUS/GVMUS  and MES (minimal equivalent subformula) extraction tool that implements hybrid extraction algorithm HYB  and its extensions [2,3,4]. The MUS functionality of MUSer2 is summarized in . The theory behind the MUS part is summarized in .
The relevant publications are:
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.
1. computation of a MUS:
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.
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