使用 IBM CPLEX 编译 MAX_HS 求解器

Compilation of MAX_HS solver with IBM CPLEX

我正在尝试开始使用名为:MAX_HS.

的 max-sat 求解器

该文档只是一个自述文件,内容不多,但很清楚您必须做什么: https://github.com/fbacchus/MaxHS

我已经从 IBM 安装了 CPLEX 库并按照文档中的指示配置了文件,但是当我编译时出现错误,这是我的终端日志:

\install -d /usr/local/include/maxhs
install -d /usr/local/include/minisat
for dir in maxhs/core maxhs/ifaces maxhs/ds maxhs/utils; do \
  install -d /usr/local/include/$dir ; \
        done
for dir in minisat/mtl minisat/utils minisat/core minisat/simp; do \
  install -d /usr/local/include/$dir ; \
done
for h in minisat/mtl/Alg.h minisat/mtl/Map.h minisat/mtl/Alloc.h minisat/mtl/Vec.h minisat/mtl/Rnd.h minisat/mtl/Sort.h minisat/mtl/IntMap.h minisat/mtl/Queue.h minisat/mtl/IntTypes.h minisat/mtl/Heap.h minisat/mtl/XAlloc.h minisat/core/SolverTypes.h minisat/core/Dimacs.h minisat/core/Solver.h minisat/utils/System.h minisat/utils/ParseUtils.h 
minisat/utils/Options.h minisat/simp/SimpSolver.h  ;
    do \
     install -m 644 $h /usr/local/include/$h ; \
done
for h in maxhs/core/Bvars.h maxhs/core/Dimacs.h maxhs/core/MaxSolverTypes.h maxhs/core/Assumptions.h maxhs/core/Wcnf.h maxhs/core/MaxSolver.h maxhs/ifaces/miniSatSolver.h maxhs/ifaces/GreedySolver.h maxhs/ifaces/Cplex.h maxhs/ifaces/greedySatSolver.h maxhs/ifaces/muser.h maxhs/ifaces/SatSolver.h maxhs/ds/Packed.h maxhs/utils/io.h maxhs/utils/Params.h maxhs/utils/hash.h  ; 
   do \
      install -m 644 $h /usr/local/include/$h ; \
done
install -d /usr/local/lib
install -m 644 build/release/lib/libmaxhs.a /usr/local/lib
Linking Binary: build/release/bin/maxhs
/opt/ibm/ILOG/CPLEX_Studio128/cplex/lib/x86-64_linux/static_pic/libcplex.a(mkl_memory_patched.o): In function `mkl_serv_set_memory_limit':
mkl_memory.c:(.text+0x5a9): undefined reference to `dlopen'
mkl_memory.c:(.text+0x5ca): undefined reference to `dlsym'
mkl_memory.c:(.text+0x618): undefined reference to `dlsym'
mkl_memory.c:(.text+0x62e): undefined reference to `dlsym'
mkl_memory.c:(.text+0x644): undefined reference to `dlsym'
mkl_memory.c:(.text+0x739): undefined reference to `dlerror'
mkl_memory.c:(.text+0x78c): undefined reference to `dlopen'
mkl_memory.c:(.text+0x840): undefined reference to `dlopen'
mkl_memory.c:(.text+0x856): undefined reference to `dlerror'
mkl_memory.c:(.text+0x91a): undefined reference to `dlopen'
mkl_memory.c:(.text+0x922): undefined reference to `dlerror'
mkl_memory.c:(.text+0x937): undefined reference to `dlsym'
mkl_memory.c:(.text+0x95a): undefined reference to `dlopen'
mkl_memory.c:(.text+0x962): undefined reference to `dlerror'
mkl_memory.c:(.text+0x972): undefined reference to `dlsym'
mkl_memory.c:(.text+0x98d): undefined reference to `dlerror'
...
...
...
64_linux/static_pic/libcplex.a(mkl_semaphore.o): In function `_Init_MKL_Loader':
mkl_semaphore.c:(.text+0x4ed): undefined reference to `dladdr'
/opt/ibm/ILOG/CPLEX_Studio128/cplex/lib/x86-64_linux/static_pic/libcplex.a(libc_is_static_interface.o): In function `mkl_serv_libc_is_static':
libc_is_static_interface.c:(.text+0x10): undefined reference to `dladdr'
/opt/ibm/ILOG/CPLEX_Studio128/cplex/lib/x86-64_linux/static_pic/libcplex.a(load_library_HOST.o): In function `mkl_ueaa_prv_load_backend_lib':
load_library.c:(.text+0x1cd): undefined reference to `dlopen'
load_library.c:(.text+0x1ef): undefined reference to `dlvsym'
load_library.c:(.text+0x218): undefined reference to `dlvsym'
load_library.c:(.text+0x241): undefined reference to `dlvsym'
load_library.c:(.text+0x26a): undefined reference to `dlvsym'
load_library.c:(.text+0x293): undefined reference to `dlvsym'
/opt/ibm/ILOG/CPLEX_Studio128/cplex/lib/x86-64_linux/static_pic/libcplex.a(load_library_HOST.o):load_library.c:(.text+0x2bc): more undefined references to `dlvsym' follow
/opt/ibm/ILOG/CPLEX_Studio128/cplex/lib/x86-64_linux/static_pic/libcplex.a(mkl_aa_fw_load_orsl_lite_lib_HOST.o): In function `mkl_aa_fw_load_orsl_lite_lib':
mkl_aa_fw_load_orsl_lite_lib.c:(.text+0xb9): undefined reference to `dlopen'
mkl_aa_fw_load_orsl_lite_lib.c:(.text+0xd4): undefined reference to `dlsym'
mkl_aa_fw_load_orsl_lite_lib.c:(.text+0xf2): undefined reference to `dlsym'
mkl_aa_fw_load_orsl_lite_lib.c:(.text+0x110): undefined reference to `dlsym'
mkl_aa_fw_load_orsl_lite_lib.c:(.text+0x12e): undefined reference to `dlsym'
collect2: error: ld returned 1 exit status
Makefile:155: recipe for target 'build/release/bin/maxhs' failed
make: *** [build/release/bin/maxhs] Error 1

真的不知道什么会导致错误,因为库是官方许可的 IBM cplex 库,唯一的设置是为 IBM 库分配正确路径的设置。我想我已经正确地完成了这一步,因为当路径错误并且没有找到 IBM 库时我又遇到了另一个错误。

有什么想法吗?

谢谢!

对于 CPLEX 12.8,您必须 link 使用动态 linker 库。您可以在 CPLEX 附带的示例联编文件中看到这一点。查看 MaxHS git 存储库中的 Makefile,您可以尝试更改以下行(尚未测试):

MAXHS_LDFLAGS  = -Wall -lz -L$(CPLEXLIBDIR) -lcplex -lpthread

至:

MAXHS_LDFLAGS  = -Wall -lz -L$(CPLEXLIBDIR) -lcplex -lpthread -ldl

如果可行,您应该考虑为 MaxHS 的维护者创建一个问题。

或者,您可以安装旧版本的 CPLEX(例如 12.7.1)。