zeta1999 / maxhs Goto Github PK

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
================================================================================