Skip to content

Latest commit

 

History

History
113 lines (92 loc) · 5.45 KB

README.md

File metadata and controls

113 lines (92 loc) · 5.45 KB
Raw

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:

  3. build the MaxPre preprocessor (if you want to use it - see Comments below):

  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.