CODEWITHSUNDEEP
alloy
John Wickerson
John Wickerson

Reputation: 1232

Selecting SAT solver from command line

The class edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler provides an example of how to execute Alloy commands from the command-line. The backend solver used in this example is Sat4J. I would love to change the solver to one of the faster ones like Plingeling. Unfortunately I can't work out how to achieve this. Simply changing the line

options.solver = A4Options.SatSolver.SAT4J;

into

options.solver = A4Options.SatSolver.PLingelingJNI;

doesn't work; I get the following error message:

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

The Alloy GUI seems to get around this problem by copying some files (including the plingeling executable) into the right place before it runs.

Upvotes: 1

Views: 573

Answers (2)

John Wickerson
John Wickerson

Reputation: 1232

Thanks to the questions linked from Tarciana's answer, I successfully got this working on my machine (a Mac).

  • In order to use solvers like Plingeling that are distributed as executables, one should run

    export PATH=<path_to_solver_binaries_and_libraries>:$PATH

    before running java.

  • In order to use solvers like MiniSat that are distributed as dynamic libraries, one should add the argument

    -Djava.library.path=<path_to_solver_binaries_and_libraries>

    when running java.

Upvotes: 2

Tarciana
Tarciana

Reputation: 123

I was with the same problem than yours as shown in my question: Execution Error when change the SATSolver from SAT4J to MiniSAT

The solution pointed by @Aleksandar in a previous question, see Alloy API resulting in java.lang.UnsatisfiedLinkError

, works for me in an older ubuntu version (10.0.0) but it does not work in earlier ubuntu versions (such as 14.04 or 16.04).

When choosing another solvers such as zchaff or minisatprover i observe that the error changes, for instance:

"The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no zchaffx5 in java.library.path"

and for all the other solvers it seems that the library it is looking for (ex.: zchaffx5) is more updated than the existing one in the x86-linux folder (inside the alloy-4.2.jar): zchaffx1. I think the existing libraries for the other solvers are outdated. If you achieve to find a solution for this problem, please let us know.

Upvotes: 1

Related Questions