Skip to content

UWrMaxSat is a relatively new MiniSat+-based solver participating in MaxSAT Evaluation 2019, where it ranked second places in both main tracks (weighted and unweighted). In MaxSAT Evaluation 2020 it won the weighted main track. It has been created recently at the University of Wrocław. It is a complete solver for partial weighted MaxSAT instanc…

License

Notifications You must be signed in to change notification settings

marekpiotrow/UWrMaxSat

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

UWrMaxSat is a quite new solver for MaxSAT and pseudo-Boolean problems. It has been created at the University of Wroclaw and can be characterized as a complete solver for partial weighted MaxSAT instances, and, independently, for linear pseudo-Boolean optimizing and decision ones.

When citing, always reference my ICTAI 2020 conference paper, bibtex record is here.

Since the version 1.3 you can merge the power of this solver with the SCIP solver, if you have a licence to use it (see: https://scipopt.org/index.php#license). The SCIP solver will be run in a separate thread, if a MaxSAT instance is not too big (less than 100000 variables and clauses). Using parameters, you can force the solver to ran in the same thread as UWrMaxSat for a given number of seconds and UWrMaxSat will be started afterwards.

Since the version 1.4 you can use the solver as a library with the IPAMIR interface (see IPAMIR). Some UWrMaxSat parameters can be set in the environment variable UWRFLAGS, for example, UWRFLAGS="-v1 -scip-cpu=120". It works both with the library and with the standalone application.

Since version 1.6.1 the IPAMIR library runs the SCIP solver in a separate thread in the similar way as the standalone application. This default behaviour can be changed by setting UWRFLAGS="-no-par".

================================================================================

Quick Install

  1. clone the repository into uwrmaxsat:
    git clone https://github.com/marekpiotrow/UWrMaxSat uwrmaxsat

  2. build the SAT solver:

    • 2.1 get COMiniSatPS by cloning its repository (with modifications used in UWrMaxSat):
      git clone https://github.com/marekpiotrow/cominisatps
    • 2.2 compile the SAT solver library:
      cd cominisatps
      rm core simp mtl utils && ln -s minisat/core minisat/simp minisat/mtl minisat/utils .
      make lr
      cd ..
  3. build the MaxPre preprocessor (if you want to use it - see Comments below):

    • 3.1 clone the MaxPre repository:
      git clone https://github.com/Laakeri/maxpre
    • 3.2 compile it as a static library:
      cd maxpre
      sed -i 's/-g/-D NDEBUG/' src/Makefile
      make lib
      cd ..
  4. build the SCIP solver library (if you want to use it)

    • 4.1 get sources of scipoptsuite from https://scipopt.org/index.php#download
    • 4.2 untar and build a static library it:
      tar zxvf scipoptsuite-8.1.0.tgz
      cd scipoptsuite-8.1.0
      mkdir build && cd build
      cmake -DSHARED=off -DNO_EXTERNAL_CODE=on -DSOPLEX=on -DTPI=tny ..
      cmake --build . --config Release --target libscip libsoplex-pic
      cd ../..
  5. build the UWrMaxSat solver (release version, statically linked):
    cd uwrmaxsat
    make config
    make r

    • 5.1 replace the last command with the following one if you do not want to use MAXPRE and SCIP libraries:
      MAXPRE= USESCIP= make r
    • 5.2 or with the one below if you do not want to use the MAXPRE library only:
      MAXPRE= make r
    • 5.3 or with the one below if you do not want to use the SCIP library only:
      USESCIP= make r

Comments:

  • the executable file is: build/release/bin/uwrmaxsat

  • if you want to use unbounded weights in MaxSAT instances, remove # in config.mk in the first line containing BIGWEIGHTS before running the last command

  • The program can be compiled with mingw64 g++ compiler in MSYS2 environment (https://www.msys2.org).

  • To build a dynamic library you have to compile the static libraries above with the compiler option -fPIC
    and, in the last step, replace 'make r' with 'make lsh'. The compiler option can be added to the steps above
    as follows:
    (2) The SAT solver library should be made with the command: CXXFLAGS=-fPIC make lr
    (3) The MaxPre Makefile should be modified with: sed -i 's/-g/-fPIC -D NDEBUG/' src/Makefile
    (4) Add the following option to the first line starting with cmake:
    -DSCIP_COMP_OPTIONS=-fPIC

Other SAT solvers

You can replace COMiniSatPS SAT solver with (A) CaDiCaL by Armin Biere or (B) Glucose 4.1 by Gilles Audemard and Laurent Simon or (C) mergesat by Norbert Manthey - see steps 5(A) or 5(B) or 5(C) below.

  • 5(A) clone CaDiCaL and build UWrMaxSat with this SAT solver:
    cd ..
    git clone https://github.com/arminbiere/cadical
    cd cadical
    patch -p1 <../uwrmaxsat/cadical.patch
    ./configure
    make
    cd ../uwrmaxsat
    cp config.cadical config.mk
    make clean
    make r

  • 5(B) clone Glucose 4.1 and build UWrMaxSat with this SAT solver:
    cd ..
    wget https://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup-4.1.tgz
    tar zxvf glucose-syrup-4.1.tgz
    cd glucose-syrup-4.1
    patch -p1 <../uwrmaxsat/glucose4.1.patch
    cd simp
    MROOT=.. make libr
    cd ..
    mkdir minisat ; cd minisat ; ln -s ../core ../simp ../mtl ../utils . ; cd ../..
    cd uwrmaxsat
    cp config.glucose4 config.mk
    make r

  • 5(C) clone mergesat and build UWrMaxSat with this SAT solver:
    cd ..
    git clone https://github.com/conp-solutions/mergesat
    cd mergesat
    make lr
    cd ../uwrmaxsat
    cp config.mergesat config.mk
    make clean
    make r

About

UWrMaxSat is a relatively new MiniSat+-based solver participating in MaxSAT Evaluation 2019, where it ranked second places in both main tracks (weighted and unweighted). In MaxSAT Evaluation 2020 it won the weighted main track. It has been created recently at the University of Wrocław. It is a complete solver for partial weighted MaxSAT instanc…

Topics

Resources

License

Stars

Watchers

Forks

Languages

  • C++ 93.3%
  • C 4.1%
  • Makefile 1.9%
  • Other 0.7%