从命令行选择 SAT 求解器

Question

edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler 类提供了如何从命令行执行 Alloy 命令的示例。此示例中使用的后端求解器是 Sat4J。我很想将求解器更改为速度更快的求解器之一，例如 Plingeling。不幸的是，我无法弄清楚如何实现这一目标。只需换行

options.solver = A4Options.SatSolver.SAT4J;

进入

options.solver = A4Options.SatSolver.PLingelingJNI;

不起作用；我收到以下错误消息：

Exception in thread "main" Fatal error:
Unknown exception occurred: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1079)
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1065)
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:381)
    at edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler.main(ExampleUsingTheCompiler.java:72)
Caused by: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory
    at kodkod.engine.Solver.solve(Solver.java:147)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:1058)
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1070)
    ... 3 more
Caused by: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory
    at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:255)
    at kodkod.engine.Solver.solve(Solver.java:140)
    ... 5 more
Caused by: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:1048)
    at java.lang.Runtime.exec(Runtime.java:620)
    at java.lang.Runtime.exec(Runtime.java:485)
    at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:221)
    ... 6 more
Caused by: java.io.IOException: error=2, No such file or directory
    at java.lang.UNIXProcess.forkAndExec(Native Method)
    at java.lang.UNIXProcess.<init>(UNIXProcess.java:248)
    at java.lang.ProcessImpl.start(ProcessImpl.java:134)
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:1029)
    ... 9 more

Alloy GUI 似乎通过在运行之前将一些文件（包括 plingeling 可执行文件）复制到正确的位置来解决这个问题。

Answer 1

感谢Tarciana's answer 链接的问题，我成功地在我的机器（Mac）上运行了这个。

• 为了使用像 Plingeling 这样的求解器，分布为 可执行文件，一个应该运行

  export PATH=<path_to_solver_binaries_and_libraries>:$PATH
  

  在运行java之前。

• 为了使用像 MiniSat 这样的求解器，分布为 动态库，应该添加参数

  -Djava.library.path=<path_to_solver_binaries_and_libraries>
  

  运行java时。

Answer 2

我遇到的问题与您的问题相同，如我的问题所示： Execution Error when change the SATSolver from SAT4J to MiniSAT

@Aleksandar 在上一个问题中指出的解决方案，请参阅 Alloy API resulting in java.lang.UnsatisfiedLinkError

，在较旧的 ubuntu 版本 (10.0.0) 中适用于我，但在较早的 ubuntu 版本（例如 14.04 或 16.04）中不起作用。

选择其他求解器（例如Zchaff或MinisatProver）时，我会观察到错误会发生变化：

“找不到所需的JNI库：java.lang.UnsatisfiedLinkError: no zchaffx5 in java.library.path”

对于所有其他求解器，它正在寻找的库（例如：zchaffx5）似乎比 x86-linux 文件夹（alloy-4.2.jar 内）中的现有库更新得更多：zchaffx1。我认为其他求解器的现有库已经过时。如果您找到解决此问题的方法，请告诉我们。