Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
Repository files navigation
This is an updated version of the original MaxHS solver (https://github.com/fbacchus/MaxHS) developed by Jessica Davies, Fahiem Bacchus, and Randy Hickey. This update is developed and maintained by Edgar Justus, Mathias Fleury, Tobias Paxian, and Andre Schidler. We are happy for any contributions. Compared to the original version, we have: - Fixed several bugs using fuzzing. - Updated the used SAT solver to CaDiCaL 3. - Updated to MaxPre 2.2 - Implemented the possibility of switching between different MIP solvers. Implementations for CPLEX, SCIP, and SCIP in exact mode exist. - Switched to CMake Known Issues: - There is a rare case where SCIP returns the wrong result, in our tests setting -no-lp-harden-reduced avoid the issue. - The LNS component is not yet built. ================================================================================ MaxHS---a maxsat solver expoiting a hybrid approach between SAT and MIPS. --------------------------------------------------------------------- Building and installing: ----------------------- 0) Get CPLEX or SCIP. ------------- You can obtain CPLEX from https://www.ibm.com/academic and the SCIP OptSuite from https://www.scipopt.org. Make sure that SCIP builds with exact mode enabled if you want to use the optimizer scip_exact. 1) clone maxhs from https://github.com/aschidler/MaxHS 2) Move into the MaxHS directory. 3) Create a directory build and initialize cmake: mkdir build cd build cmake -DCMAKE_BUILD_TYPE=Release .. 4) Add the desired parameters for cmake, possible parameters can be listed using: cmake -LH At least one optimizer must be used (USE_SCIP=Enabled or USE_CPLEX=Enabled). 5) Build maxhs: make -j 6) Run --------- The executable is built in the created 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