Выбор SAT Solver из командной строки

Класс 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 исполняется) в нужном месте, прежде чем он запускается.

Источник

2 ответа

Решение

Благодаря вопросам, связанным с ответом Tarciana, я успешно получил эту работу на моей машине (Mac).

  • Чтобы использовать такие решатели, как Plingeling, которые распространяются как исполняемые файлы, нужно запустить

    export PATH=<path_to_solver_binaries_and_libraries>:$PATH

    перед запуском java,

  • Чтобы использовать решатели типа MiniSat, которые распространяются в виде динамических библиотек, необходимо добавить аргумент

    -Djava.library.path=<path_to_solver_binaries_and_libraries>

    при беге java,

Источник

У меня была та же проблема, что и у вас, как показано в моем вопросе: Ошибка выполнения при изменении SATSolver с SAT4J на MiniSAT

Решение, на которое указывал @Aleksandar в предыдущем вопросе, см. Alloy API, приводящий к java.lang.UnsatisfiedLinkError

, работает для меня в более старой версии Ubuntu (10.0.0), но не работает в более ранних версиях Ubuntu (например, 14.04 или 16.04).

При выборе других решателей, таких как zchaff или minisatprover, я замечаю, что ошибка меняется, например:

"Не удается найти требуемую библиотеку JNI: java.lang.UnsatisfiedLinkError: нет zchaffx5 в java.library.path"

и для всех других решателей кажется, что библиотека, которую она ищет (например, zchaffx5), более обновлена, чем существующая в папке x86-linux (внутри сплава-4.2.jar): zchaffx1. Я думаю, что существующие библиотеки для других решателей устарели. Если вам удастся найти решение этой проблемы, сообщите нам об этом.

Источник
Другие вопросы по тегам