Differences

This shows you the differences between two versions of the page.

Link to this comparison view

muser [2016/11/17 13:44] (current)
ajrm created
Line 1: Line 1:
 +====== MUSer2 (MUS extractor v2) - (V/​G)MUS/​MES extraction tool ======
  
 +==== Description ====
 +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:
 +  - J. Marques-Silva and I. Lynce: {{:​papers:​msl-sat11.pdf| On Improving MUS Extraction Algorithms}}. SAT 2011. LNCS 6695, pp. 159-173
 +  - A. Belov and J. Marques-Silva:​ {{:​papers:​bms-fmcad11.pdf| Accelerating MUS Extraction with Recursive Model Rotation}}. FMCAD 2011.
 +  - A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva:​ {{:​papers:​bimms-sat12.pdf| On Efficient Computation of Variable MUSes}}. SAT 2012. LNCS 7317, pp. 296-309
 +  - A. Belov, M. Janota, I. Lynce and J. Marques-Silva:​ On Computing Minimal Equivalent Subformulas. CP 2012 (to appear).
 +  - A. Belov and J. Marques-Silva:​ {{:​papers:​bms-pos12.pdf| MUSer2: An Efficient MUS Extractor}}. POS 2012.
 +  - A. Belov, I. Lynce and J. Marques-Silva:​ Towards Efficient MUS Extraction. AI Communications,​ 2012 (In Press) {{:​papers:​blms-aicomm12.pdf|[preprint]}}
 +
 +==== News ====
 +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.
 +
 +
 +
 +==== Distribution ====
 +
 +MUSer2 is currently available from [[https://​bitbucket.org/​anton_belov/​muser2|bitbucket]].
 +
 +Public release for teaching and research use only.
 +
 +Please contact [[anton.belov|Anton]] in case of any questions or problems. ​  
 +
 +Download binaries (Linux 32/64bit, MacOSX 64 bit) {{:​tools:​muser2-20120821.tgz|here}}. Please contact us if you need a binary for a different UNIX-based platform.
 +
 +Download source distribution {{:​tools:​muser2-src-20120821.tgz|here}}. The source distribution is under GPLv3, and lacks some of the features in the binary. ​
 +==== Documentation ====
 +The instructions for using ''​MUSer2''​ are available {{:​docs:​readme-muser2.txt|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
 +
 +==== Benchmarks ====
 +
 +The set of 500 benchmark CNF instances used in the experiments reported in the SAT 2011 and FMCAD 2011 papers are available in {{:​benchmarks:​satcomp11-submitted-trimmed.tgz|this archive}}. The CNF and group-CNF benchmarks used in the MUS track of SAT Competition 2011 are available from the [[http://​www.cril.univ-artois.fr/​SAT11/​|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.
 +
 +{{:​images:​muser-2-satcomp11-benchmarks-cactus.png?​|}}
 +
 +==== Contributors ====
 +  * Anton Belov
 +  * [[joao.marques-silva| Joao Marques-Silva]] (Principal Investigator)
 +
 +==== Funding ====
 +The research on MUS extraction and the devlopement of MUSer2 were partially supported by [[http://​www.sfi.ie/​ | Science Foundation Ireland]]
 +
 +{{:​images:​sfi.jpeg?​nolink&​200|}}
Print/export