1. Anton Belov
  2. muser2-para


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

[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.

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

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

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)


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


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.


[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