1. Anton Belov
  2. DMUSer


DMUSer: a DRUP-based MUS extractor

DMUSer is a Python-based pipeline for the computation of Minimal Unsatisfiable 
Subformulas (MUSes) of CNF formulas. Given an input CNF formula, DMUSer applies
a number of powerful DRUP-based formula trimming techniques described in [1], 
and kicks off a back-end MUS extractor, either on the trimmed formula, or on 
its resolution proof in TRACECHECK format.

This source code release of DMUSer is under the MIT license, i.e. you can do 
whatever you like with it. However, DMUSer uses a number of tools (listed 
below), which are included in the binary form in this release --- thus, if you 
use DMUSer you are indirectly using at least one of these tools and it is YOUR 
responsibility to ensure that your use abides by their licensing terms.

DMUSer is (c) 2014 Anton Belov and Marijn Heule. 

If you use DMUSer in your research, please cite

[1] A. Belov, M. Heule, J. Marques-Silva. "MUS Extraction using Clausal Proofs", 
    Proc. SAT 2014, 2014.

Please contact Anton Belov or Marijn Heule in case of bugs or questions.

DMUSer is written in Python (tested with version 2.7). 

DMUSer uses the following tools:

(1) DRUPtrim by Marijn Heule

(2) Glucose 3.0 by Gilles Audemard and Laurent Simon

(3) Haifa-MUC by Vadim Ryvchin

(4) MUSer2 by Anton Belov and Joao Marques-Silva


Simply clone the repository by running

       git clone https://anton_belov@bitbucket.org/anton_belov/dmuser.git

and create a symlink bin/tools that points to either bin/tools.linux or 
bin/tools.mac, depending on your platform.

The benchmark set used for the experimental evaluation of DMUSer in SAT 2014
paper is available for download here: 



dmuser.py -h -- display all available options and parameters. Please read the 
          output carefully. If something is unclear send us an email.

Some examples:

1. standard trimming, with Haifa-MUC (Tr-HM in the paper [1])

dmuser.py -pre=none -mt ./tests/3pipe_3_ooo.cnf

2. layred trimming, with Haifa-MUC or MUSer2 (LTr-HM/LTr-M in the paper [1])

dmuser.py -mt ./tests/3pipe_3_ooo.cnf
dmuser.py -mc ./tests/3pipe_3_ooo.cnf

3. iterative trimming, with Haifa-MUC (ITr0-HM-A in the paper [1])

dmuser.py -mi=0 -mt -ctime=10 -atime -preonce ./tests/3pipe_3_ooo.cnf