MaxHS---a maxsat solver expoiting a hybrid approach between SAT and MIPS. The code uses minisat as the SAT solver and CPLEX from IBM as the MIPS solver. The Makefile setup is a modification of the minisat Makefile.

---

Building and installing:

0. Get CPLEX.

---

You need the CPLEX static libraries to link against. CPLEX is available from IBM under their academic Initiative program. It is free to faculty members and graduate students in academia.

try https://www.ibm.com/academic

If that fails aa google search of 'IBM academic initiative' should find the right site. You apply for their academic initiative program and then then you can download CPLEX and other IBM software.

Note. CPLEX is very useful for many tasks and well worth having access to irrespective of MaxHS.

1. clone maxhs from https://github.com/fbacchus/MaxHS

2. Move into the MaxHS directory and edit the Makefile to properly set the following Makefile variables

REQUIRED VARIABLE SETTINGS:

LINUX_CPLEXLIBDIR=<path to CPLEX library> #the directory on your linux system that contains libcplex.a #and libilocplex.a LINUX_CPLEXINCDIR=<path to CPLEX headers>

and if you want to build on macos

DARWIN_CPLEXLIBDIR=<path to CPLEX library> #the directory on your MAC system that contains libcplex.a #and libilocplex.a DARWIN_CPLEXINCDIR=<path to CPLEX headers>

NOTE: you do not have to set both the LINUX_ and DARWIN_ variables, just the ones for the operating system you are using.

3. Build

---

In the MaxHS directory execute

make

4. Run

---

The executable is built in MaxHS/build/release/bin/ if you change to that directory you should be able to execute

./maxhs -no-printSoln <maxsat instance file>

use ./maxhs --help or ./maxhs --help-verb

to obtain a listing of the available parameter settings

================================================================================ Directory Overview:

maxhs/ MaxHs code minisat/ Minisat SAT solver with changes to make assumptions more efficient glucose/ Glucose SAT solver README LICENSE