Execution Error when change the SATSolver from SAT

Question

In my Java code, when i change the SATSolver from SAT4J to MiniSatJNI or MiniSatProverJNI in:

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

For instance, to:

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

And then call:

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

I receive the following execution error:

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)

Any help?

Answer 1

Alloy invokes native solvers (such as MiniSAT) by using JNDI/JNI. That means that the native libraries must be correctly configured before. If you do not have the library correclty configured, Java will produce a "java.lang.UnsatisfiedLinkError" exception.

The Alloy distributable jar includes correctly configured libraries for Windows "x86" and for Linux and Mac in "x86" and "x64". That means that the jar will work in Windows, without any additional configuration, if you are using the Java 32 bits, but not with Java 64 bits. In the other operating systems you can use both Java versions (32 and 64 bits).

You may check other questions in StackOverflow for the same explanation.

Answer 2

The solution pointed by @Aleksandar in: Alloy API resulting in java.lang.UnsatisfiedLinkError

worked for me on linux!!! But it does not work on windows.

Thank you for all the help !