-
Notifications
You must be signed in to change notification settings - Fork 7
/
README
79 lines (58 loc) · 2.31 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
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
================================================================================