1. Anton Belov
  2. muser2-para

Overview

HTTPS SSH
********************************************************************************
MUSer2-PARA: a parallel MUS extractor
--------------------------------------

This is an experimental version of MUSer2 that takes advantage of thread-based
parallelism to speed up MUS extraction. See the webpage for MUSer2 [2] for
details of what a scalar version of MUSer2 tries to achieve.

The detailed description of the parallel extractor is available in the following
publication:

[1] A. Belov, N. Manthey, J. Marques-Silva. Parallel MUS Extraction. SAT 2013

Please cite [1] if you user MUSer2-PARA in your research work.

MUSer2-PARA is (c) 2012-2014 Anton Belov, Norbert Manthey, Joao Marques-Silva

This source code release is under the GNU General Public License Version 3. See 
COPYING for more details. In essence you are only allowed to distribute a 
modified version of MUSer2-PARA (resp. a program that uses MUSer2-PARA) if you 
make the sources of your modifications (resp. the program that uses MUSer2-PARA) 
under GPL as well. If you need another license please contact us.

IMPORTANT: the modified version of SAT solver Minisat [3] included in this source 
release is under open-source license. If you use MUSer2-PARA, you are indirectly 
using this SAT solver and it is YOUR responsibility to ensure that your use 
abides by their licensing terms.
       
********************************************************************************
DEPENDENCIES

(1) As some of the code is written in C++11 gcc 4.7 or later is required to 
    compile the tool.
    
********************************************************************************
COMPILATION

This source code release is a snapshot of a subset of a large research framework
called BOLT, developed by J. Marques-Silva and collaborators. As such the 
directory structure and the compilation process is more involved than required 
for MUSer2. Its also a bit fragile, and will, hopefully be fixed.

To compile:

cd ./src/tools/muser2
make

To clean up all directories:

cd ./src/tools/muser2
make allclean

To rebuild dependencies:

cd into directory you want to rebuild for
make deps

The key file for compilation tweaks is ./src/mkcfg/makefile-common-defs

Compilation options:

make mkm=prof -- profiling build
make mkm=val  -- optimized, with debug symbols
make mkm=ass  -- optimized, with assertions enabled
make mkm=chk  -- checked build (code inside CHK(x) macros is compiled in)
make mkm=dbg  -- non-optimized debug build (code in DBG(x) macros is compiled in)

make xm=xp    -- compile all the experimental code, i.e. anything under
                 #ifdef XPMODE in the source (use at your own risk)

********************************************************************************
USAGE

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

Some examples:

1. parallel computation of a MUS:

muser2 -threads 4 bitops0.cnf  

2. computation of a group-MUS:

muser2 -grp -threads 4 ../examples/bitops0.gcnf

********************************************************************************
AUTHORS

Anton Belov (anton@belov-mcdowell.com)          -- MUSer2 + parallel algorithms  
Norbert Manthey (norbert.manthey@tu-dresden.de) -- parallelization + parallel algorithms
Joao Marques-Silva (joao.marques-silva@ucd.ie)  -- BOLT, initial version of MUSer.

********************************************************************************
REFERENCES

[1] A. Belov, N. Manthey, J. Marques-Silva. Parallel MUS Extraction. SAT 2013

[2] http://bitbucket.org/anton_belov/muser2

[3] Minisat 2.2 by Niklas Een and Niklas Sorensson
    http://http://minisat.se/