将SATSolver从SAT4J更改为MiniSAT时出现执行错误

Question

在我的Java代码中，当我将SATSolver从SAT4J更改为MiniSatJNI或MiniSatProverJNI时：

A4Options options = new A4Options();
options.solver = A4Options.SatSolver.SAT4J;

例如，执行以下操作：

A4Options options = new A4Options();
options.solver = A4Options.SatSolver.MiniSatProverJNI;

然后打电话给：

A4Solution currentAns = TranslateAlloyToKodkod.execute_command(null,
                        javaMetamodel.getAllReachableSigs(), command, options);

我收到以下执行错误：

Fatal error:
The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)
    at ejdolly.JDollyImp.initializeAlloyAnalyzer(JDollyImp.java:128)
    at ejdolly.JDolly.hasNext(JDolly.java:181)
    at org.testorrery.ForLoopIterator.hasNext(ForLoopIterator.java:40)
    at refactoringTest.RefactoringTest.runTests(RefactoringTest.java:145)
    at refactoringTest.MainRunner.main(MainRunner.java:83)
Caused by: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path
    at java.lang.ClassLoader.loadLibrary(Unknown Source)
    at java.lang.Runtime.loadLibrary0(Unknown Source)
    at java.lang.System.loadLibrary(Unknown Source)
    at kodkod.engine.satlab.NativeSolver.loadLibrary(NativeSolver.java:73)
    at kodkod.engine.satlab.MiniSatProver.<clinit>(MiniSatProver.java:148)
    at kodkod.engine.satlab.SATFactory$5.instance(SATFactory.java:106)
    at kodkod.engine.fol2sat.Bool2CNFTranslator.translate(Bool2CNFTranslator.java:55)
    at kodkod.engine.fol2sat.Translator.toCNF(Translator.java:426)
    at kodkod.engine.fol2sat.Translator.generateSBP(Translator.java:365)
    at kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:343)
    at kodkod.engine.fol2sat.Translator.translate(Translator.java:189)
    at kodkod.engine.fol2sat.Translator.translate(Translator.java:143)
    at kodkod.engine.Solver$SolutionIterator.next(Solver.java:495)
    at kodkod.engine.Solver$SolutionIterator.next(Solver.java:1)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.<init>(A4Solution.java:719)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.<init>(A4Solution.java:709)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:941)
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:388)
    ... 5 more
java.lang.NullPointerException
    at ejdolly.JDolly.hasNext(JDolly.java:182)
    at org.testorrery.ForLoopIterator.hasNext(ForLoopIterator.java:40)
    at refactoringTest.RefactoringTest.runTests(RefactoringTest.java:145)
    at refactoringTest.MainRunner.main(MainRunner.java:83)

有什么帮助吗？

Answer 1

@Aleksandar在：Alloy API resulting in java.lang.UnsatisfiedLinkError中指出的解决方案

在linux上为我工作！但它在windows上不起作用。

谢谢你的帮助！

Answer 2

合金通过使用JNDI/JNI调用本机求解器(如MiniSAT)。这意味着在此之前必须正确配置本机库。如果你没有正确配置这个库，Java会产生一个"java.lang.UnsatisfiedLinkError“异常。

合金可分发jar包括Windows "x86“以及"x86”和"x64“中针对Linux和Mac的正确配置的库。这意味着，如果您使用的是Java32位，那么jar将在Windows中工作，而不需要任何额外的配置，但不能使用Java64位。在其他操作系统中，您可以使用这两个Java版本(32位和64位)。

你可以在other questions in StackOverflow上找到同样的解释。