-
Notifications
You must be signed in to change notification settings - Fork 7
MaxHS: a hybrid Maxsat solver developed by Jessica Davies and Fahiem Bacchus
License
fbacchus/MaxHS
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
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 ================================================================================
About
MaxHS: a hybrid Maxsat solver developed by Jessica Davies and Fahiem Bacchus
Resources
License
Stars
Watchers
Forks
Packages 0
No packages published