从命令行选择SAT解算器

edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler类提供了一个如何从命令行执行Alloy命令的示例。本例中使用的后端求解器是Sat4J。我很乐意将求解器改为其中一个更快的求解器，如Plingeling。不幸的是我无法解决如何实现这一目标。简单地改变行从命令行选择SAT解算器

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

的合金GUI似乎被一些文件（包括plingeling可执行文件）复制到合适的位置，然后再运行来解决这个问题。

来源

2016-04-26 John Wickerson

感谢从Tarciana's answer链接的问题，我成功地在我的机器上（Mac）得到了这个工作。

为了使用求解像Plingeling被分布可执行文件，应该运行java之前运行
```
export PATH=<path_to_solver_binaries_and_libraries>:$PATH 
```
。
为了使用求解像MINISAT被分布动态库，应运行java时添加参数
```
-Djava.library.path=<path_to_solver_binaries_and_libraries> 
```
。

来源

2016-05-01 21:14:03

我是比你同样的问题，如图我的问题： 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中：在任何的java.library.path zchaffx5 “

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

来源

2016-04-30 21:10:06 Tarciana

从命令行选择SAT解算器

回答

相关问题